Theorem dvhbase

Description: The ring base set of the constructed full vector space H. (Contributed by NM, 29-Oct-2013) (Revised by Mario Carneiro, 22-Jun-2014)

	Ref	Expression
Hypotheses	dvhbase.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dvhbase.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
	dvhbase.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dvhbase.f	$$⊢F=\mathrm{Scalar}\left(U\right)$$
	dvhbase.c	$$⊢C={\mathrm{Base}}_F$$
Assertion	dvhbase	$$⊢\left(K\in X\wedge W\in H\right)\to C=E$$

Proof

Step	Hyp	Ref	Expression
1		dvhbase.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dvhbase.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
3		dvhbase.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		dvhbase.f	$$⊢F=\mathrm{Scalar}\left(U\right)$$
5		dvhbase.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	dvhsca	$$⊢\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	syl5eq	$$⊢\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$$