This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvafplusg

Description: Ring addition operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013) (Revised by Mario Carneiro, 22-Jun-2014)

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 dvafplusg ⊢ K ∈ V ∧ W ∈ H → + ˙ = s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ 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 eqid ⊢ EDRing ⁡ K ⁡ W = EDRing ⁡ K ⁡ W
8 1 7 4 5 dvasca ⊢ K ∈ V ∧ W ∈ H → F = EDRing ⁡ K ⁡ W
9 8 fveq2d ⊢ K ∈ V ∧ W ∈ H → + F = + EDRing ⁡ K ⁡ W
10 6 9 eqtrid ⊢ K ∈ V ∧ W ∈ H → + ˙ = + EDRing ⁡ K ⁡ W
11 eqid ⊢ + EDRing ⁡ K ⁡ W = + EDRing ⁡ K ⁡ W
12 1 2 3 7 11 erngfplus ⊢ K ∈ V ∧ W ∈ H → + EDRing ⁡ K ⁡ W = s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
13 10 12 eqtrd ⊢ K ∈ V ∧ W ∈ H → + ˙ = s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f