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 = LHyp K
hlhillvec.u U = HLHil K W
hlhillvec.k φ K HL W H
hlhildrng.r R = Scalar U
Assertion hlhildrng φ R DivRing

Proof

Step Hyp Ref Expression
1 hlhillvec.h H = LHyp K
2 hlhillvec.u U = HLHil K W
3 hlhillvec.k φ K HL W H
4 hlhildrng.r R = Scalar U
5 eqid EDRing K W = EDRing K W
6 1 5 erngdv K HL W H EDRing K W DivRing
7 3 6 syl φ EDRing K W DivRing
8 eqidd φ Base EDRing K W = Base EDRing K W
9 eqid Base EDRing K W = Base EDRing K W
10 1 5 2 4 3 9 hlhilsbase φ Base EDRing K W = Base R
11 eqid + EDRing K W = + EDRing K W
12 1 5 2 4 3 11 hlhilsplus φ + EDRing K W = + R
13 12 oveqdr φ x Base EDRing K W y Base EDRing K W x + EDRing K W y = x + R y
14 eqid EDRing K W = EDRing K W
15 1 5 2 4 3 14 hlhilsmul φ EDRing K W = R
16 15 oveqdr φ x Base EDRing K W y Base EDRing K W x EDRing K W y = x R y
17 8 10 13 16 drngpropd φ EDRing K W DivRing R DivRing
18 7 17 mpbid φ R DivRing