Metamath Proof Explorer


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=LHypK
hlhillvec.u U=HLHilKW
hlhillvec.k φKHLWH
hlhildrng.r R=ScalarU
Assertion hlhildrng φRDivRing

Proof

Step Hyp Ref Expression
1 hlhillvec.h H=LHypK
2 hlhillvec.u U=HLHilKW
3 hlhillvec.k φKHLWH
4 hlhildrng.r R=ScalarU
5 eqid EDRingKW=EDRingKW
6 1 5 erngdv KHLWHEDRingKWDivRing
7 3 6 syl φEDRingKWDivRing
8 eqidd φBaseEDRingKW=BaseEDRingKW
9 eqid BaseEDRingKW=BaseEDRingKW
10 1 5 2 4 3 9 hlhilsbase φBaseEDRingKW=BaseR
11 eqid +EDRingKW=+EDRingKW
12 1 5 2 4 3 11 hlhilsplus φ+EDRingKW=+R
13 12 oveqdr φxBaseEDRingKWyBaseEDRingKWx+EDRingKWy=x+Ry
14 eqid EDRingKW=EDRingKW
15 1 5 2 4 3 14 hlhilsmul φEDRingKW=R
16 15 oveqdr φxBaseEDRingKWyBaseEDRingKWxEDRingKWy=xRy
17 8 10 13 16 drngpropd φEDRingKWDivRingRDivRing
18 7 17 mpbid φRDivRing