Metamath Proof Explorer

Theorem dvabase

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

Ref Expression
Hypotheses dvabase.h ⊢ H = LHyp ⁡ K
dvabase.e ⊢ E = TEndo ⁡ K ⁡ W
dvabase.u ⊢ U = DVecA ⁡ K ⁡ W
dvabase.f ⊢ F = Scalar ⁡ U
dvabase.c ⊢ C = Base F
Assertion dvabase ⊢ K ∈ X ∧ W ∈ H → C = E

Proof

Step Hyp Ref Expression
1 dvabase.h ⊢ H = LHyp ⁡ K
2 dvabase.e ⊢ E = TEndo ⁡ K ⁡ W
3 dvabase.u ⊢ U = DVecA ⁡ K ⁡ W
4 dvabase.f ⊢ F = Scalar ⁡ U
5 dvabase.c ⊢ C = Base F
6 eqid ⊢ EDRing ⁡ K ⁡ W = EDRing ⁡ K ⁡ W
7 1 6 3 4 dvasca ⊢ K ∈ X ∧ W ∈ H → F = EDRing ⁡ K ⁡ W
8 7 fveq2d ⊢ K ∈ X ∧ W ∈ H → Base F = Base EDRing ⁡ K ⁡ W
9 5 8 syl5eq ⊢ K ∈ X ∧ W ∈ H → C = Base EDRing ⁡ K ⁡ W
10 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
11 eqid ⊢ Base EDRing ⁡ K ⁡ W = Base EDRing ⁡ K ⁡ W
12 1 10 2 6 11 erngbase ⊢ K ∈ X ∧ W ∈ H → Base EDRing ⁡ K ⁡ W = E
13 9 12 eqtrd ⊢ K ∈ X ∧ W ∈ H → C = E