k : Type u_3
V : Type u_5
P : Type u_6
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type ?u.403226
s₂ : Finset ι₂
V₂ : Type u_1
P₂ : Type u_2
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
w : ι → k
hw : Finset.sum s w = 1
f : P →ᵃ[k] P₂
b : P
⊢ ↑f (↑(affineCombination k s p) w) = ↑(affineCombination k s (↑f ∘ p)) w
k : Type u_3
V : Type u_5
P : Type u_6
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type ?u.403226
s₂ : Finset ι₂
V₂ : Type u_1
P₂ : Type u_2
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
w : ι → k
hw : Finset.sum s w = 1
f : P →ᵃ[k] P₂
⊢ ↑f (↑(affineCombination k s p) w) = ↑(affineCombination k s (↑f ∘ p)) w
have b := Classical.choice (inferInstance : AffineSpace V P).Nonempty
k : Type u_3
V : Type u_5
P : Type u_6
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type ?u.403226
s₂ : Finset ι₂
V₂ : Type u_1
P₂ : Type u_2
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
w : ι → k
hw : Finset.sum s w = 1
f : P →ᵃ[k] P₂
b : P
b₂ : P₂
⊢ ↑f (↑(affineCombination k s p) w) = ↑(affineCombination k s (↑f ∘ p)) w
k : Type u_3
V : Type u_5
P : Type u_6
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type ?u.403226
s₂ : Finset ι₂
V₂ : Type u_1
P₂ : Type u_2
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
w : ι → k
hw : Finset.sum s w = 1
f : P →ᵃ[k] P₂
b : P
⊢ ↑f (↑(affineCombination k s p) w) = ↑(affineCombination k s (↑f ∘ p)) w
have b₂ := Classical.choice (inferInstance : AffineSpace V₂ P₂).Nonempty
k : Type u_3
V : Type u_5
P : Type u_6
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type ?u.403226
s₂ : Finset ι₂
V₂ : Type u_1
P₂ : Type u_2
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
w : ι → k
hw : Finset.sum s w = 1
f : P →ᵃ[k] P₂
b : P
b₂ : P₂
⊢ ↑f (↑(weightedVSubOfPoint s p b) w +ᵥ b) = ↑(weightedVSubOfPoint s (↑f ∘ p) (↑f b)) w +ᵥ ↑f b
k : Type u_3
V : Type u_5
P : Type u_6
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type ?u.403226
s₂ : Finset ι₂
V₂ : Type u_1
P₂ : Type u_2
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
w : ι → k
hw : Finset.sum s w = 1
f : P →ᵃ[k] P₂
b : P
b₂ : P₂
⊢ ↑f (↑(affineCombination k s p) w) = ↑(affineCombination k s (↑f ∘ p)) w
rw [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p hw b,
  s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w (f ∘ p) hw b₂, ←
  s.weightedVSubOfPoint_vadd_eq_of_sum_eq_one w (f ∘ p) hw (f b) b₂]
no goals
k : Type u_3
V : Type u_5
P : Type u_6
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type ?u.403226
s₂ : Finset ι₂
V₂ : Type u_1
P₂ : Type u_2
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
w : ι → k
hw : Finset.sum s w = 1
f : P →ᵃ[k] P₂
b : P
b₂ : P₂
⊢ ↑f (↑(weightedVSubOfPoint s p b) w +ᵥ b) = ↑(weightedVSubOfPoint s (↑f ∘ p) (↑f b)) w +ᵥ ↑f b
simp only [weightedVSubOfPoint_apply, RingHom.id_apply, AffineMap.map_vadd,
  LinearMap.map_smulₛₗ, AffineMap.linearMap_vsub, LinearMap.map_sum, Function.comp_apply]