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

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 DVecHKW=DVecHKW
6 eqid ScalarDVecHKW=ScalarDVecHKW
7 eqid BaseScalarDVecHKW=BaseScalarDVecHKW
8 eqid +ScalarDVecHKW=+ScalarDVecHKW
9 eqid ScalarDVecHKW=ScalarDVecHKW
10 eqid HGMapKW=HGMapKW
11 1 2 3 4 5 6 7 8 9 10 hlhilsrnglem φR*-Ring