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	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dvhbase.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
	dvhbase.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dvhbase.f	⊢ 𝐹 = ( Scalar ‘ 𝑈 )
	dvhbase.c	⊢ 𝐶 = ( Base ‘ 𝐹 )
Assertion	dvhbase	⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) → 𝐶 = 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		dvhbase.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dvhbase.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
3		dvhbase.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		dvhbase.f	⊢ 𝐹 = ( Scalar ‘ 𝑈 )
5		dvhbase.c	⊢ 𝐶 = ( Base ‘ 𝐹 )
6		eqid	⊢ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
7	1 6 3 4	dvhsca	⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) → 𝐹 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
8	7	fveq2d	⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝐹 ) = ( Base ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) )
9	5 8	syl5eq	⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) → 𝐶 = ( Base ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) )
10		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
11		eqid	⊢ ( Base ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
12	1 10 2 6 11	erngbase	⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝐸 )
13	9 12	eqtrd	⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) → 𝐶 = 𝐸 )