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=BaseU
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=BaseU
6 eqid ⊢EDRing⁡K⁡W=EDRing⁡K⁡W
7 1 2 3 6 4 dvhset ⊢K∈X∧W∈H→U=BasendxT×E+ndxf∈T×E,g∈T×E⟼1st⁡f∘1st⁡gh∈T⟼2nd⁡f⁡h∘2nd⁡g⁡hScalar⁡ndxEDRing⁡K⁡W∪⋅ndxs∈E,f∈T×E⟼s⁡1st⁡fs∘2nd⁡f
8 7 fveq2d ⊢K∈X∧W∈H→BaseU=BaseBasendxT×E+ndxf∈T×E,g∈T×E⟼1st⁡f∘1st⁡gh∈T⟼2nd⁡f⁡h∘2nd⁡g⁡hScalar⁡ndxEDRing⁡K⁡W∪⋅ndxs∈E,f∈T×E⟼s⁡1st⁡fs∘2nd⁡f
9 2 fvexi ⊢T∈V
10 3 fvexi ⊢E∈V
11 9 10 xpex ⊢T×E∈V
12 eqid ⊢BasendxT×E+ndxf∈T×E,g∈T×E⟼1st⁡f∘1st⁡gh∈T⟼2nd⁡f⁡h∘2nd⁡g⁡hScalar⁡ndxEDRing⁡K⁡W∪⋅ndxs∈E,f∈T×E⟼s⁡1st⁡fs∘2nd⁡f=BasendxT×E+ndxf∈T×E,g∈T×E⟼1st⁡f∘1st⁡gh∈T⟼2nd⁡f⁡h∘2nd⁡g⁡hScalar⁡ndxEDRing⁡K⁡W∪⋅ndxs∈E,f∈T×E⟼s⁡1st⁡fs∘2nd⁡f
13 12 lmodbase ⊢T×E∈V→T×E=BaseBasendxT×E+ndxf∈T×E,g∈T×E⟼1st⁡f∘1st⁡gh∈T⟼2nd⁡f⁡h∘2nd⁡g⁡hScalar⁡ndxEDRing⁡K⁡W∪⋅ndxs∈E,f∈T×E⟼s⁡1st⁡fs∘2nd⁡f
14 11 13 ax-mp ⊢T×E=BaseBasendxT×E+ndxf∈T×E,g∈T×E⟼1st⁡f∘1st⁡gh∈T⟼2nd⁡f⁡h∘2nd⁡g⁡hScalar⁡ndxEDRing⁡K⁡W∪⋅ndxs∈E,f∈T×E⟼s⁡1st⁡fs∘2nd⁡f
15 8 5 14 3eqtr4g ⊢K∈X∧W∈H→V=T×E