This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

Step	Hyp	Ref	Expression
1		dvabase.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dvabase.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
3		dvabase.u	⊢ 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
4		dvabase.f	⊢ 𝐹 = ( Scalar ‘ 𝑈 )
5		dvabase.c	⊢ 𝐶 = ( Base ‘ 𝐹 )
6		eqid	⊢ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
7	1 6 3 4	dvasca	⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) → 𝐹 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
8	7	fveq2d	⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝐹 ) = ( Base ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) )
9	5 8	eqtrid	⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) → 𝐶 = ( 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	⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) → 𝐶 = 𝐸 )