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=\mathrm{LHyp}\left(K\right)$$
	hlhillvec.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
	hlhillvec.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hlhildrng.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
Assertion	hlhilsrng	$$⊢\phi \to R\in \mathrm{*-Ring}$$

Proof

Step	Hyp	Ref	Expression
1		hlhillvec.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hlhillvec.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
3		hlhillvec.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
4		hlhildrng.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
5		eqid	$$⊢\mathrm{DVecH}\left(K\right)\left(W\right)=\mathrm{DVecH}\left(K\right)\left(W\right)$$
6		eqid	$$⊢\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)=\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)$$
7		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}$$
8		eqid	$$⊢{+}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}={+}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}$$
9		eqid	$$⊢{\cdot }_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}={\cdot }_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}$$
10		eqid	$$⊢\mathrm{HGMap}\left(K\right)\left(W\right)=\mathrm{HGMap}\left(K\right)\left(W\right)$$
11	1 2 3 4 5 6 7 8 9 10	hlhilsrnglem	$$⊢\phi \to R\in \mathrm{*-Ring}$$