Metamath Proof Explorer


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 φ K HL W H
hlhildrng.r R = Scalar U
Assertion hlhilsrng φ R *-Ring

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 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 + Scalar DVecH K W = + Scalar DVecH K W
9 eqid Scalar DVecH K W = Scalar DVecH K W
10 eqid HGMap K W = HGMap K W
11 1 2 3 4 5 6 7 8 9 10 hlhilsrnglem φ R *-Ring