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

Metamath Proof Explorer

Theorem dvhvbase

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

Ref Expression
Hypotheses dvhvbase.h ⊢ H = LHyp ⁡ K
dvhvbase.t ⊢ T = LTrn ⁡ K ⁡ W
dvhvbase.e ⊢ E = TEndo ⁡ K ⁡ W
dvhvbase.u ⊢ U = DVecH ⁡ K ⁡ W
dvhvbase.v ⊢ V = Base U
Assertion dvhvbase ⊢ K ∈ X ∧ W ∈ H → V = T × E

Proof

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