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=\mathrm{LHyp}\left(K\right)$$
	dvabase.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
	dvabase.u	$$⊢U=\mathrm{DVecA}\left(K\right)\left(W\right)$$
	dvabase.f	$$⊢F=\mathrm{Scalar}\left(U\right)$$
	dvabase.c	$$⊢C={\mathrm{Base}}_F$$
Assertion	dvabase	$$⊢\left(K\in X\wedge W\in H\right)\to C=E$$

Proof

Step	Hyp	Ref	Expression
1		dvabase.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dvabase.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
3		dvabase.u	$$⊢U=\mathrm{DVecA}\left(K\right)\left(W\right)$$
4		dvabase.f	$$⊢F=\mathrm{Scalar}\left(U\right)$$
5		dvabase.c	$$⊢C={\mathrm{Base}}_F$$
6		eqid	$$⊢\mathrm{EDRing}\left(K\right)\left(W\right)=\mathrm{EDRing}\left(K\right)\left(W\right)$$
7	1 6 3 4	dvasca	$$⊢\left(K\in X\wedge W\in H\right)\to F=\mathrm{EDRing}\left(K\right)\left(W\right)$$
8	7	fveq2d	$$⊢\left(K\in X\wedge W\in H\right)\to {\mathrm{Base}}_F={\mathrm{Base}}_{\mathrm{EDRing}\left(K\right)\left(W\right)}$$
9	5 8	eqtrid	$$⊢\left(K\in X\wedge W\in H\right)\to C={\mathrm{Base}}_{\mathrm{EDRing}\left(K\right)\left(W\right)}$$
10		eqid	$$⊢\mathrm{LTrn}\left(K\right)\left(W\right)=\mathrm{LTrn}\left(K\right)\left(W\right)$$
11		eqid	$$⊢{\mathrm{Base}}_{\mathrm{EDRing}\left(K\right)\left(W\right)}={\mathrm{Base}}_{\mathrm{EDRing}\left(K\right)\left(W\right)}$$
12	1 10 2 6 11	erngbase	$$⊢\left(K\in X\wedge W\in H\right)\to {\mathrm{Base}}_{\mathrm{EDRing}\left(K\right)\left(W\right)}=E$$
13	9 12	eqtrd	$$⊢\left(K\in X\wedge W\in H\right)\to C=E$$