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=BasendxLTrn⁡K⁡W+ndxf∈LTrn⁡K⁡W,g∈LTrn⁡K⁡W⟼f∘gScalar⁡ndxD∪⋅ndxs∈TEndo⁡K⁡W,f∈LTrn⁡K⁡W⟼s⁡f
8 7 fveq2d ⊢K∈X∧W∈H→Scalar⁡U=Scalar⁡BasendxLTrn⁡K⁡W+ndxf∈LTrn⁡K⁡W,g∈LTrn⁡K⁡W⟼f∘gScalar⁡ndxD∪⋅ndxs∈TEndo⁡K⁡W,f∈LTrn⁡K⁡W⟼s⁡f
9 2 fvexi ⊢D∈V
10 eqid ⊢BasendxLTrn⁡K⁡W+ndxf∈LTrn⁡K⁡W,g∈LTrn⁡K⁡W⟼f∘gScalar⁡ndxD∪⋅ndxs∈TEndo⁡K⁡W,f∈LTrn⁡K⁡W⟼s⁡f=BasendxLTrn⁡K⁡W+ndxf∈LTrn⁡K⁡W,g∈LTrn⁡K⁡W⟼f∘gScalar⁡ndxD∪⋅ndxs∈TEndo⁡K⁡W,f∈LTrn⁡K⁡W⟼s⁡f
11 10 lmodsca ⊢D∈V→D=Scalar⁡BasendxLTrn⁡K⁡W+ndxf∈LTrn⁡K⁡W,g∈LTrn⁡K⁡W⟼f∘gScalar⁡ndxD∪⋅ndxs∈TEndo⁡K⁡W,f∈LTrn⁡K⁡W⟼s⁡f
12 9 11 ax-mp ⊢D=Scalar⁡BasendxLTrn⁡K⁡W+ndxf∈LTrn⁡K⁡W,g∈LTrn⁡K⁡W⟼f∘gScalar⁡ndxD∪⋅ndxs∈TEndo⁡K⁡W,f∈LTrn⁡K⁡W⟼s⁡f
13 8 4 12 3eqtr4g ⊢K∈X∧W∈H→F=D