Metamath Proof Explorer

Theorem dvaplusg

Description: Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013)

Ref Expression
Hypotheses dvafplus.h ⊢ H = LHyp ⁡ K
dvafplus.t ⊢ T = LTrn ⁡ K ⁡ W
dvafplus.e ⊢ E = TEndo ⁡ K ⁡ W
dvafplus.u ⊢ U = DVecA ⁡ K ⁡ W
dvafplus.f ⊢ F = Scalar ⁡ U
dvafplus.p ⊢ + ˙ = + F
Assertion dvaplusg ⊢ K ∈ V ∧ W ∈ H ∧ R ∈ E ∧ S ∈ E → R + ˙ S = f ∈ T ⟼ R ⁡ f ∘ S ⁡ f

Proof

Step Hyp Ref Expression
1 dvafplus.h ⊢ H = LHyp ⁡ K
2 dvafplus.t ⊢ T = LTrn ⁡ K ⁡ W
3 dvafplus.e ⊢ E = TEndo ⁡ K ⁡ W
4 dvafplus.u ⊢ U = DVecA ⁡ K ⁡ W
5 dvafplus.f ⊢ F = Scalar ⁡ U
6 dvafplus.p ⊢ + ˙ = + F
7 1 2 3 4 5 6 dvafplusg ⊢ K ∈ V ∧ W ∈ H → + ˙ = s ∈ E , t ∈ E ⟼ g ∈ T ⟼ s ⁡ g ∘ t ⁡ g
8 7 oveqd ⊢ K ∈ V ∧ W ∈ H → R + ˙ S = R s ∈ E , t ∈ E ⟼ g ∈ T ⟼ s ⁡ g ∘ t ⁡ g S
9 eqid ⊢ s ∈ E , t ∈ E ⟼ g ∈ T ⟼ s ⁡ g ∘ t ⁡ g = s ∈ E , t ∈ E ⟼ g ∈ T ⟼ s ⁡ g ∘ t ⁡ g
10 9 2 tendopl ⊢ R ∈ E ∧ S ∈ E → R s ∈ E , t ∈ E ⟼ g ∈ T ⟼ s ⁡ g ∘ t ⁡ g S = f ∈ T ⟼ R ⁡ f ∘ S ⁡ f
11 8 10 sylan9eq ⊢ K ∈ V ∧ W ∈ H ∧ R ∈ E ∧ S ∈ E → R + ˙ S = f ∈ T ⟼ R ⁡ f ∘ S ⁡ f