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

Metamath Proof Explorer

Theorem dvavbase

Description: The vectors (vector base set) of the constructed partial vector space A are all translations (for a fiducial co-atom W ). (Contributed by NM, 9-Oct-2013) (Revised by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypotheses dvavbase.h ⊢ H = LHyp ⁡ K
dvavbase.t ⊢ T = LTrn ⁡ K ⁡ W
dvavbase.u ⊢ U = DVecA ⁡ K ⁡ W
dvavbase.v ⊢ V = Base U
Assertion dvavbase ⊢ K ∈ X ∧ W ∈ H → V = T

Proof

Step Hyp Ref Expression
1 dvavbase.h ⊢ H = LHyp ⁡ K
2 dvavbase.t ⊢ T = LTrn ⁡ K ⁡ W
3 dvavbase.u ⊢ U = DVecA ⁡ K ⁡ W
4 dvavbase.v ⊢ V = Base U
5 eqid ⊢ TEndo ⁡ K ⁡ W = TEndo ⁡ K ⁡ W
6 eqid ⊢ EDRing ⁡ K ⁡ W = EDRing ⁡ K ⁡ W
7 1 2 5 6 3 dvaset ⊢ K ∈ X ∧ W ∈ H → U = Base ndx T + ndx f ∈ T , g ∈ T ⟼ f ∘ g Scalar ⁡ ndx EDRing ⁡ K ⁡ W ∪ ⋅ ndx s ∈ TEndo ⁡ K ⁡ W , f ∈ T ⟼ s ⁡ f
8 7 fveq2d ⊢ K ∈ X ∧ W ∈ H → Base U = Base Base ndx T + ndx f ∈ T , g ∈ T ⟼ f ∘ g Scalar ⁡ ndx EDRing ⁡ K ⁡ W ∪ ⋅ ndx s ∈ TEndo ⁡ K ⁡ W , f ∈ T ⟼ s ⁡ f
9 2 fvexi ⊢ T ∈ V
10 eqid ⊢ Base ndx T + ndx f ∈ T , g ∈ T ⟼ f ∘ g Scalar ⁡ ndx EDRing ⁡ K ⁡ W ∪ ⋅ ndx s ∈ TEndo ⁡ K ⁡ W , f ∈ T ⟼ s ⁡ f = Base ndx T + ndx f ∈ T , g ∈ T ⟼ f ∘ g Scalar ⁡ ndx EDRing ⁡ K ⁡ W ∪ ⋅ ndx s ∈ TEndo ⁡ K ⁡ W , f ∈ T ⟼ s ⁡ f
11 10 lmodbase ⊢ T ∈ V → T = Base Base ndx T + ndx f ∈ T , g ∈ T ⟼ f ∘ g Scalar ⁡ ndx EDRing ⁡ K ⁡ W ∪ ⋅ ndx s ∈ TEndo ⁡ K ⁡ W , f ∈ T ⟼ s ⁡ f
12 9 11 ax-mp ⊢ T = Base Base ndx T + ndx f ∈ T , g ∈ T ⟼ f ∘ g Scalar ⁡ ndx EDRing ⁡ K ⁡ W ∪ ⋅ ndx s ∈ TEndo ⁡ K ⁡ W , f ∈ T ⟼ s ⁡ f
13 8 4 12 3eqtr4g ⊢ K ∈ X ∧ W ∈ H → V = T