Theorem hlhildrng

Description: The star division ring for the final constructed Hilbert space is a division ring. (Contributed by NM, 20-Jun-2015) (Revised by Mario Carneiro, 28-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	hlhildrng	$$⊢\phi \to R\in \mathrm{DivRing}$$

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{EDRing}\left(K\right)\left(W\right)=\mathrm{EDRing}\left(K\right)\left(W\right)$$
6	1 5	erngdv	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \mathrm{EDRing}\left(K\right)\left(W\right)\in \mathrm{DivRing}$$
7	3 6	syl	$$⊢\phi \to \mathrm{EDRing}\left(K\right)\left(W\right)\in \mathrm{DivRing}$$
8		eqidd	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{EDRing}\left(K\right)\left(W\right)}={\mathrm{Base}}_{\mathrm{EDRing}\left(K\right)\left(W\right)}$$
9		eqid	$$⊢{\mathrm{Base}}_{\mathrm{EDRing}\left(K\right)\left(W\right)}={\mathrm{Base}}_{\mathrm{EDRing}\left(K\right)\left(W\right)}$$
10	1 5 2 4 3 9	hlhilsbase	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{EDRing}\left(K\right)\left(W\right)}={\mathrm{Base}}_R$$
11		eqid	$$⊢{+}_{\mathrm{EDRing}\left(K\right)\left(W\right)}={+}_{\mathrm{EDRing}\left(K\right)\left(W\right)}$$
12	1 5 2 4 3 11	hlhilsplus	$$⊢\phi \to {+}_{\mathrm{EDRing}\left(K\right)\left(W\right)}={+}_R$$
13	12	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{EDRing}\left(K\right)\left(W\right)}\wedge y\in {\mathrm{Base}}_{\mathrm{EDRing}\left(K\right)\left(W\right)}\right)\right)\to x{+}_{\mathrm{EDRing}\left(K\right)\left(W\right)}y=x{+}_{R}y$$
14		eqid	$$⊢{\cdot }_{\mathrm{EDRing}\left(K\right)\left(W\right)}={\cdot }_{\mathrm{EDRing}\left(K\right)\left(W\right)}$$
15	1 5 2 4 3 14	hlhilsmul	$$⊢\phi \to {\cdot }_{\mathrm{EDRing}\left(K\right)\left(W\right)}={\cdot }_R$$
16	15	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{EDRing}\left(K\right)\left(W\right)}\wedge y\in {\mathrm{Base}}_{\mathrm{EDRing}\left(K\right)\left(W\right)}\right)\right)\to x{\cdot }_{\mathrm{EDRing}\left(K\right)\left(W\right)}y=x{\cdot }_{R}y$$
17	8 10 13 16	drngpropd	$$⊢\phi \to \left(\mathrm{EDRing}\left(K\right)\left(W\right)\in \mathrm{DivRing}\leftrightarrow R\in \mathrm{DivRing}\right)$$
18	7 17	mpbid	$$⊢\phi \to R\in \mathrm{DivRing}$$