[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃⁱ[𝕜] P₂
⊢ f.linear = (AffineIsometry.linearIsometry f).toLinearMap
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃⁱ[𝕜] P₂
x✝ : V
⊢ ↑f.linear x✝ = ↑(AffineIsometry.linearIsometry f).toLinearMap x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f✝ f g : P →ᵃⁱ[𝕜] P₂
⊢ (fun f => f.toFun) f = (fun f => f.toFun) g → f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f g : P →ᵃⁱ[𝕜] P₂
toAffineMap✝ : P →ᵃ[𝕜] P₂
norm_map✝ : ∀ (x : V), ‖↑toAffineMap✝.linear x‖ = ‖x‖
⊢ (fun f => f.toFun) { toAffineMap := toAffineMap✝, norm_map := norm_map✝ } = (fun f => f.toFun) g →
    { toAffineMap := toAffineMap✝, norm_map := norm_map✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃⁱ[𝕜] P₂
toAffineMap✝¹ : P →ᵃ[𝕜] P₂
norm_map✝¹ : ∀ (x : V), ‖↑toAffineMap✝¹.linear x‖ = ‖x‖
toAffineMap✝ : P →ᵃ[𝕜] P₂
norm_map✝ : ∀ (x : V), ‖↑toAffineMap✝.linear x‖ = ‖x‖
⊢ (fun f => f.toFun) { toAffineMap := toAffineMap✝¹, norm_map := norm_map✝¹ } =
      (fun f => f.toFun) { toAffineMap := toAffineMap✝, norm_map := norm_map✝ } →
    { toAffineMap := toAffineMap✝¹, norm_map := norm_map✝¹ } = { toAffineMap := toAffineMap✝, norm_map := norm_map✝ }
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃⁱ[𝕜] P₂
⊢ ↑f.toAffineMap = ↑f
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃⁱ[𝕜] P₂
⊢ Injective toAffineMap
[PROOFSTEP]
rintro ⟨f, _⟩ ⟨g, _⟩ rfl
[GOAL]
case mk.mk
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f✝ : P →ᵃⁱ[𝕜] P₂
f : P →ᵃ[𝕜] P₂
norm_map✝¹ : ∀ (x : V), ‖↑f.linear x‖ = ‖x‖
norm_map✝ : ∀ (x : V), ‖↑{ toAffineMap := f, norm_map := norm_map✝¹ }.toAffineMap.linear x‖ = ‖x‖
⊢ { toAffineMap := f, norm_map := norm_map✝¹ } =
    { toAffineMap := { toAffineMap := f, norm_map := norm_map✝¹ }.toAffineMap, norm_map := norm_map✝ }
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : V →ₗᵢ[𝕜] V₂
⊢ AffineIsometry.linearIsometry (toAffineIsometry f) = f
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : V →ₗᵢ[𝕜] V₂
x✝ : V
⊢ ↑(AffineIsometry.linearIsometry (toAffineIsometry f)) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃⁱ[𝕜] P₂
f₁ : P₁ →ᵃⁱ[𝕜] P₂
x y : P
⊢ dist (↑f x) (↑f y) = dist x y
[PROOFSTEP]
rw [dist_eq_norm_vsub V₂, dist_eq_norm_vsub V, ← map_vsub, f.linearIsometry.norm_map]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃⁱ[𝕜] P₂
f₁ : P₁ →ᵃⁱ[𝕜] P₂
x y : P
⊢ nndist (↑f x) (↑f y) = nndist x y
[PROOFSTEP]
simp [nndist_dist, (dist_map)]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃⁱ[𝕜] P₂
f₁ : P₁ →ᵃⁱ[𝕜] P₂
x y : P
⊢ edist (↑f x) (↑f y) = edist x y
[PROOFSTEP]
simp [edist_dist, (dist_map)]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
⊢ e.linear = (AffineIsometryEquiv.linearIsometryEquiv e).toLinearEquiv
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
x✝ : V
⊢ ↑e.linear x✝ = ↑(AffineIsometryEquiv.linearIsometryEquiv e).toLinearEquiv x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e f g : P ≃ᵃⁱ[𝕜] P₂
h : (fun f => f.toFun) f = (fun f => f.toFun) g
x✝ : (fun f => f.invFun) f = (fun f => f.invFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e g : P ≃ᵃⁱ[𝕜] P₂
toAffineEquiv✝ : P ≃ᵃ[𝕜] P₂
norm_map✝ : ∀ (x : V), ‖↑toAffineEquiv✝.linear x‖ = ‖x‖
h : (fun f => f.toFun) { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ } = (fun f => f.toFun) g
x✝ : (fun f => f.invFun) { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ } = (fun f => f.invFun) g
⊢ { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
toAffineEquiv✝¹ : P ≃ᵃ[𝕜] P₂
norm_map✝¹ : ∀ (x : V), ‖↑toAffineEquiv✝¹.linear x‖ = ‖x‖
toAffineEquiv✝ : P ≃ᵃ[𝕜] P₂
norm_map✝ : ∀ (x : V), ‖↑toAffineEquiv✝.linear x‖ = ‖x‖
h :
  (fun f => f.toFun) { toAffineEquiv := toAffineEquiv✝¹, norm_map := norm_map✝¹ } =
    (fun f => f.toFun) { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ }
x✝ :
  (fun f => f.invFun) { toAffineEquiv := toAffineEquiv✝¹, norm_map := norm_map✝¹ } =
    (fun f => f.invFun) { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ }
⊢ { toAffineEquiv := toAffineEquiv✝¹, norm_map := norm_map✝¹ } =
    { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toAffineEquiv
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
toAffineEquiv✝¹ : P ≃ᵃ[𝕜] P₂
norm_map✝¹ : ∀ (x : V), ‖↑toAffineEquiv✝¹.linear x‖ = ‖x‖
toAffineEquiv✝ : P ≃ᵃ[𝕜] P₂
norm_map✝ : ∀ (x : V), ‖↑toAffineEquiv✝.linear x‖ = ‖x‖
h :
  (fun f => f.toFun) { toAffineEquiv := toAffineEquiv✝¹, norm_map := norm_map✝¹ } =
    (fun f => f.toFun) { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ }
x✝ :
  (fun f => f.invFun) { toAffineEquiv := toAffineEquiv✝¹, norm_map := norm_map✝¹ } =
    (fun f => f.invFun) { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ }
⊢ toAffineEquiv✝¹ = toAffineEquiv✝
[PROOFSTEP]
simpa [FunLike.coe_injective.eq_iff] using h
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e✝ : P ≃ᵃⁱ[𝕜] P₂
e : P₁ → P₂
e' : V₁ ≃ₗᵢ[𝕜] V₂
p : P₁
h : ∀ (p' : P₁), e p' = ↑e' (p' -ᵥ p) +ᵥ e p
⊢ AffineIsometryEquiv.linearIsometryEquiv (mk' e e' p h) = e'
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e✝ : P ≃ᵃⁱ[𝕜] P₂
e : P₁ → P₂
e' : V₁ ≃ₗᵢ[𝕜] V₂
p : P₁
h : ∀ (p' : P₁), e p' = ↑e' (p' -ᵥ p) +ᵥ e p
x✝ : V₁
⊢ ↑(AffineIsometryEquiv.linearIsometryEquiv (mk' e e' p h)) x✝ = ↑e' x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e : V ≃ₗᵢ[𝕜] V₂
⊢ ↑(toAffineIsometryEquiv e) = ↑e
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e : V ≃ₗᵢ[𝕜] V₂
⊢ AffineIsometryEquiv.linearIsometryEquiv (toAffineIsometryEquiv e) = e
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e : V ≃ₗᵢ[𝕜] V₂
x✝ : V
⊢ ↑(AffineIsometryEquiv.linearIsometryEquiv (toAffineIsometryEquiv e)) x✝ = ↑e x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e✝ e : P ≃ᵃⁱ[𝕜] P₂
⊢ range ↑e = univ
[PROOFSTEP]
rw [← coe_toIsometryEquiv]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e✝ e : P ≃ᵃⁱ[𝕜] P₂
⊢ range ↑(toIsometryEquiv e) = univ
[PROOFSTEP]
exact IsometryEquiv.range_eq_univ _
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²¹ : NormedField 𝕜
inst✝²⁰ : SeminormedAddCommGroup V
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : SeminormedAddCommGroup V₂
inst✝¹⁷ : SeminormedAddCommGroup V₃
inst✝¹⁶ : SeminormedAddCommGroup V₄
inst✝¹⁵ : NormedSpace 𝕜 V
inst✝¹⁴ : NormedSpace 𝕜 V₁
inst✝¹³ : NormedSpace 𝕜 V₂
inst✝¹² : NormedSpace 𝕜 V₃
inst✝¹¹ : NormedSpace 𝕜 V₄
inst✝¹⁰ : PseudoMetricSpace P
inst✝⁹ : MetricSpace P₁
inst✝⁸ : PseudoMetricSpace P₂
inst✝⁷ : PseudoMetricSpace P₃
inst✝⁶ : PseudoMetricSpace P₄
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : NormedAddTorsor V₂ P₂
inst✝² : NormedAddTorsor V₃ P₃
inst✝¹ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type u_12
inst✝ : TopologicalSpace α
p : P
⊢ symm (constVSub 𝕜 p) = trans (LinearIsometryEquiv.toAffineIsometryEquiv (LinearIsometryEquiv.neg 𝕜)) (vaddConst 𝕜 p)
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²¹ : NormedField 𝕜
inst✝²⁰ : SeminormedAddCommGroup V
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : SeminormedAddCommGroup V₂
inst✝¹⁷ : SeminormedAddCommGroup V₃
inst✝¹⁶ : SeminormedAddCommGroup V₄
inst✝¹⁵ : NormedSpace 𝕜 V
inst✝¹⁴ : NormedSpace 𝕜 V₁
inst✝¹³ : NormedSpace 𝕜 V₂
inst✝¹² : NormedSpace 𝕜 V₃
inst✝¹¹ : NormedSpace 𝕜 V₄
inst✝¹⁰ : PseudoMetricSpace P
inst✝⁹ : MetricSpace P₁
inst✝⁸ : PseudoMetricSpace P₂
inst✝⁷ : PseudoMetricSpace P₃
inst✝⁶ : PseudoMetricSpace P₄
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : NormedAddTorsor V₂ P₂
inst✝² : NormedAddTorsor V₃ P₃
inst✝¹ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type u_12
inst✝ : TopologicalSpace α
p : P
x✝ : V
⊢ ↑(symm (constVSub 𝕜 p)) x✝ =
    ↑(trans (LinearIsometryEquiv.toAffineIsometryEquiv (LinearIsometryEquiv.neg 𝕜)) (vaddConst 𝕜 p)) x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²¹ : NormedField 𝕜
inst✝²⁰ : SeminormedAddCommGroup V
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : SeminormedAddCommGroup V₂
inst✝¹⁷ : SeminormedAddCommGroup V₃
inst✝¹⁶ : SeminormedAddCommGroup V₄
inst✝¹⁵ : NormedSpace 𝕜 V
inst✝¹⁴ : NormedSpace 𝕜 V₁
inst✝¹³ : NormedSpace 𝕜 V₂
inst✝¹² : NormedSpace 𝕜 V₃
inst✝¹¹ : NormedSpace 𝕜 V₄
inst✝¹⁰ : PseudoMetricSpace P
inst✝⁹ : MetricSpace P₁
inst✝⁸ : PseudoMetricSpace P₂
inst✝⁷ : PseudoMetricSpace P₃
inst✝⁶ : PseudoMetricSpace P₄
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : NormedAddTorsor V₂ P₂
inst✝² : NormedAddTorsor V₃ P₃
inst✝¹ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type u_12
inst✝ : TopologicalSpace α
f : P → P₂
hf : Isometry f
p : P
g : V → V₂
hg : ∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p
⊢ Isometry g
[PROOFSTEP]
convert (vaddConst 𝕜 (f p)).symm.isometry.comp (hf.comp (vaddConst 𝕜 p).isometry)
[GOAL]
case h.e'_5
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²¹ : NormedField 𝕜
inst✝²⁰ : SeminormedAddCommGroup V
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : SeminormedAddCommGroup V₂
inst✝¹⁷ : SeminormedAddCommGroup V₃
inst✝¹⁶ : SeminormedAddCommGroup V₄
inst✝¹⁵ : NormedSpace 𝕜 V
inst✝¹⁴ : NormedSpace 𝕜 V₁
inst✝¹³ : NormedSpace 𝕜 V₂
inst✝¹² : NormedSpace 𝕜 V₃
inst✝¹¹ : NormedSpace 𝕜 V₄
inst✝¹⁰ : PseudoMetricSpace P
inst✝⁹ : MetricSpace P₁
inst✝⁸ : PseudoMetricSpace P₂
inst✝⁷ : PseudoMetricSpace P₃
inst✝⁶ : PseudoMetricSpace P₄
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : NormedAddTorsor V₂ P₂
inst✝² : NormedAddTorsor V₃ P₃
inst✝¹ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type u_12
inst✝ : TopologicalSpace α
f : P → P₂
hf : Isometry f
p : P
g : V → V₂
hg : ∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p
⊢ g = ↑(symm (vaddConst 𝕜 (f p))) ∘ f ∘ ↑(vaddConst 𝕜 p)
[PROOFSTEP]
exact funext hg
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²¹ : NormedField 𝕜
inst✝²⁰ : SeminormedAddCommGroup V
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : SeminormedAddCommGroup V₂
inst✝¹⁷ : SeminormedAddCommGroup V₃
inst✝¹⁶ : SeminormedAddCommGroup V₄
inst✝¹⁵ : NormedSpace 𝕜 V
inst✝¹⁴ : NormedSpace 𝕜 V₁
inst✝¹³ : NormedSpace 𝕜 V₂
inst✝¹² : NormedSpace 𝕜 V₃
inst✝¹¹ : NormedSpace 𝕜 V₄
inst✝¹⁰ : PseudoMetricSpace P
inst✝⁹ : MetricSpace P₁
inst✝⁸ : PseudoMetricSpace P₂
inst✝⁷ : PseudoMetricSpace P₃
inst✝⁶ : PseudoMetricSpace P₄
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : NormedAddTorsor V₂ P₂
inst✝² : NormedAddTorsor V₃ P₃
inst✝¹ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type u_12
inst✝ : TopologicalSpace α
x y : P
⊢ dist (↑(pointReflection 𝕜 x) y) x = dist y x
[PROOFSTEP]
rw [← (pointReflection 𝕜 x).dist_map y x, pointReflection_self]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²¹ : NormedField 𝕜
inst✝²⁰ : SeminormedAddCommGroup V
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : SeminormedAddCommGroup V₂
inst✝¹⁷ : SeminormedAddCommGroup V₃
inst✝¹⁶ : SeminormedAddCommGroup V₄
inst✝¹⁵ : NormedSpace 𝕜 V
inst✝¹⁴ : NormedSpace 𝕜 V₁
inst✝¹³ : NormedSpace 𝕜 V₂
inst✝¹² : NormedSpace 𝕜 V₃
inst✝¹¹ : NormedSpace 𝕜 V₄
inst✝¹⁰ : PseudoMetricSpace P
inst✝⁹ : MetricSpace P₁
inst✝⁸ : PseudoMetricSpace P₂
inst✝⁷ : PseudoMetricSpace P₃
inst✝⁶ : PseudoMetricSpace P₄
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : NormedAddTorsor V₂ P₂
inst✝² : NormedAddTorsor V₃ P₃
inst✝¹ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type u_12
inst✝ : TopologicalSpace α
x y : P
⊢ dist (↑(pointReflection 𝕜 x) y) y = ‖bit0 (x -ᵥ y)‖
[PROOFSTEP]
rw [pointReflection_apply, dist_eq_norm_vsub V, vadd_vsub_assoc, bit0]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²¹ : NormedField 𝕜
inst✝²⁰ : SeminormedAddCommGroup V
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : SeminormedAddCommGroup V₂
inst✝¹⁷ : SeminormedAddCommGroup V₃
inst✝¹⁶ : SeminormedAddCommGroup V₄
inst✝¹⁵ : NormedSpace 𝕜 V
inst✝¹⁴ : NormedSpace 𝕜 V₁
inst✝¹³ : NormedSpace 𝕜 V₂
inst✝¹² : NormedSpace 𝕜 V₃
inst✝¹¹ : NormedSpace 𝕜 V₄
inst✝¹⁰ : PseudoMetricSpace P
inst✝⁹ : MetricSpace P₁
inst✝⁸ : PseudoMetricSpace P₂
inst✝⁷ : PseudoMetricSpace P₃
inst✝⁶ : PseudoMetricSpace P₄
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : NormedAddTorsor V₂ P₂
inst✝² : NormedAddTorsor V₃ P₃
inst✝¹ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type u_12
inst✝ : TopologicalSpace α
x y : P
⊢ dist (↑(pointReflection 𝕜 x) y) y = ‖2‖ * dist x y
[PROOFSTEP]
rw [dist_pointReflection_self', ← two_smul' 𝕜 (x -ᵥ y), norm_smul, ← dist_eq_norm_vsub V]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²² : NormedField 𝕜
inst✝²¹ : SeminormedAddCommGroup V
inst✝²⁰ : SeminormedAddCommGroup V₁
inst✝¹⁹ : SeminormedAddCommGroup V₂
inst✝¹⁸ : SeminormedAddCommGroup V₃
inst✝¹⁷ : SeminormedAddCommGroup V₄
inst✝¹⁶ : NormedSpace 𝕜 V
inst✝¹⁵ : NormedSpace 𝕜 V₁
inst✝¹⁴ : NormedSpace 𝕜 V₂
inst✝¹³ : NormedSpace 𝕜 V₃
inst✝¹² : NormedSpace 𝕜 V₄
inst✝¹¹ : PseudoMetricSpace P
inst✝¹⁰ : MetricSpace P₁
inst✝⁹ : PseudoMetricSpace P₂
inst✝⁸ : PseudoMetricSpace P₃
inst✝⁷ : PseudoMetricSpace P₄
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddTorsor V₁ P₁
inst✝⁴ : NormedAddTorsor V₂ P₂
inst✝³ : NormedAddTorsor V₃ P₃
inst✝² : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type u_12
inst✝¹ : TopologicalSpace α
inst✝ : NormedSpace ℝ V
x y : P
⊢ dist (↑(pointReflection ℝ x) y) y = 2 * dist x y
[PROOFSTEP]
rw [dist_pointReflection_self, Real.norm_two]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
⊢ Continuous ↑f.linear ↔ Continuous ↑f
[PROOFSTEP]
inhabit P
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
⊢ Continuous ↑f.linear ↔ Continuous ↑f
[PROOFSTEP]
have :
  (f.linear : V → V₂) =
    (AffineIsometryEquiv.vaddConst 𝕜 <| f default).toHomeomorph.symm ∘
      f ∘ (AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph :=
  by
  ext v
  simp only [(AffineIsometryEquiv.coe_toHomeomorph), Function.comp_apply, (AffineMap.map_vadd), eq_self_iff_true,
    (AffineIsometryEquiv.toHomeomorph_symm), (AffineIsometryEquiv.coe_vaddConst), (vadd_vsub),
    (AffineIsometryEquiv.coe_vaddConst_symm)]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
⊢ ↑f.linear =
    ↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
      ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default))
[PROOFSTEP]
ext v
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
v : V
⊢ ↑f.linear v =
    (↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
        ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default)))
      v
[PROOFSTEP]
simp only [(AffineIsometryEquiv.coe_toHomeomorph), Function.comp_apply, (AffineMap.map_vadd), eq_self_iff_true,
  (AffineIsometryEquiv.toHomeomorph_symm), (AffineIsometryEquiv.coe_vaddConst), (vadd_vsub),
  (AffineIsometryEquiv.coe_vaddConst_symm)]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
this :
  ↑f.linear =
    ↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
      ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default))
⊢ Continuous ↑f.linear ↔ Continuous ↑f
[PROOFSTEP]
rw [this]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
this :
  ↑f.linear =
    ↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
      ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default))
⊢ Continuous
      (↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
        ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default))) ↔
    Continuous ↑f
[PROOFSTEP]
simp only [Homeomorph.comp_continuous_iff, Homeomorph.comp_continuous_iff']
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
⊢ IsOpenMap ↑f.linear ↔ IsOpenMap ↑f
[PROOFSTEP]
inhabit P
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
⊢ IsOpenMap ↑f.linear ↔ IsOpenMap ↑f
[PROOFSTEP]
have :
  (f.linear : V → V₂) =
    (AffineIsometryEquiv.vaddConst 𝕜 <| f default).toHomeomorph.symm ∘
      f ∘ (AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph :=
  by
  ext v
  simp only [(AffineIsometryEquiv.coe_toHomeomorph), Function.comp_apply, (AffineMap.map_vadd), eq_self_iff_true,
    (AffineIsometryEquiv.toHomeomorph_symm), (AffineIsometryEquiv.coe_vaddConst), (vadd_vsub),
    (AffineIsometryEquiv.coe_vaddConst_symm)]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
⊢ ↑f.linear =
    ↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
      ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default))
[PROOFSTEP]
ext v
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
v : V
⊢ ↑f.linear v =
    (↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
        ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default)))
      v
[PROOFSTEP]
simp only [(AffineIsometryEquiv.coe_toHomeomorph), Function.comp_apply, (AffineMap.map_vadd), eq_self_iff_true,
  (AffineIsometryEquiv.toHomeomorph_symm), (AffineIsometryEquiv.coe_vaddConst), (vadd_vsub),
  (AffineIsometryEquiv.coe_vaddConst_symm)]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
this :
  ↑f.linear =
    ↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
      ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default))
⊢ IsOpenMap ↑f.linear ↔ IsOpenMap ↑f
[PROOFSTEP]
rw [this]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
this :
  ↑f.linear =
    ↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
      ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default))
⊢ IsOpenMap
      (↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
        ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default))) ↔
    IsOpenMap ↑f
[PROOFSTEP]
simp only [Homeomorph.comp_isOpenMap_iff, Homeomorph.comp_isOpenMap_iff']
