Theorem hlhilsrng

Description: The star division ring for the final constructed Hilbert space is a division ring. (Contributed by NM, 21-Jun-2015)

	Ref	Expression
Hypotheses	hlhillvec.h	|- H = ( LHyp ` K )
	hlhillvec.u	|- U = ( ( HLHil ` K ) ` W )
	hlhillvec.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hlhildrng.r	|- R = ( Scalar ` U )
Assertion	hlhilsrng	|- ( ph -> R e. *Ring )

Proof

Step	Hyp	Ref	Expression
1		hlhillvec.h	|- H = ( LHyp ` K )
2		hlhillvec.u	|- U = ( ( HLHil ` K ) ` W )
3		hlhillvec.k	|- ( ph -> ( K e. HL /\ W e. H ) )
4		hlhildrng.r	|- R = ( Scalar ` U )
5		eqid	|- ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W )
6		eqid	|- ( Scalar ` ( ( DVecH ` K ) ` W ) ) = ( Scalar ` ( ( DVecH ` K ) ` W ) )
7		eqid	|- ( Base ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) ) = ( Base ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) )
8		eqid	|- ( +g ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) ) = ( +g ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) )
9		eqid	|- ( .r ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) ) = ( .r ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) )
10		eqid	|- ( ( HGMap ` K ) ` W ) = ( ( HGMap ` K ) ` W )
11	1 2 3 4 5 6 7 8 9 10	hlhilsrnglem	|- ( ph -> R e. *Ring )