Metamath Proof Explorer

Theorem dvasca

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, 22-Jun-2014)

Ref Expression
Hypotheses dvasca.h ⊢ H = LHyp ⁡ K
dvasca.d ⊢ D = EDRing ⁡ K ⁡ W
dvasca.u ⊢ U = DVecA ⁡ K ⁡ W
dvasca.f ⊢ F = Scalar ⁡ U
Assertion dvasca ⊢ K ∈ X ∧ W ∈ H → F = D

Proof

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