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 
|- ( ph -> ( K e. HL /\ W e. H ) )
hlhildrng.r 
|- R = ( Scalar ` U )
Assertion hlhildrng 
|- ( ph -> R e. DivRing )

Proof

Step Hyp Ref Expression
1 hlhillvec.h 
 |-  H = ( LHyp ` K )
2 hlhillvec.u 
 |-  U = ( ( HLHil ` K ) ` W )
3 hlhillvec.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
4 hlhildrng.r 
 |-  R = ( Scalar ` U )
5 eqid 
 |-  ( ( EDRing ` K ) ` W ) = ( ( EDRing ` K ) ` W )
6 1 5 erngdv 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( EDRing ` K ) ` W ) e. DivRing )
7 3 6 syl 
 |-  ( ph -> ( ( EDRing ` K ) ` W ) e. DivRing )
8 eqidd 
 |-  ( ph -> ( 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 
 |-  ( ph -> ( Base ` ( ( EDRing ` K ) ` W ) ) = ( Base ` R ) )
11 eqid 
 |-  ( +g ` ( ( EDRing ` K ) ` W ) ) = ( +g ` ( ( EDRing ` K ) ` W ) )
12 1 5 2 4 3 11 hlhilsplus 
 |-  ( ph -> ( +g ` ( ( EDRing ` K ) ` W ) ) = ( +g ` R ) )
13 12 oveqdr 
 |-  ( ( ph /\ ( x e. ( Base ` ( ( EDRing ` K ) ` W ) ) /\ y e. ( Base ` ( ( EDRing ` K ) ` W ) ) ) ) -> ( x ( +g ` ( ( EDRing ` K ) ` W ) ) y ) = ( x ( +g ` R ) y ) )
14 eqid 
 |-  ( .r ` ( ( EDRing ` K ) ` W ) ) = ( .r ` ( ( EDRing ` K ) ` W ) )
15 1 5 2 4 3 14 hlhilsmul 
 |-  ( ph -> ( .r ` ( ( EDRing ` K ) ` W ) ) = ( .r ` R ) )
16 15 oveqdr 
 |-  ( ( ph /\ ( x e. ( Base ` ( ( EDRing ` K ) ` W ) ) /\ y e. ( Base ` ( ( EDRing ` K ) ` W ) ) ) ) -> ( x ( .r ` ( ( EDRing ` K ) ` W ) ) y ) = ( x ( .r ` R ) y ) )
17 8 10 13 16 drngpropd 
 |-  ( ph -> ( ( ( EDRing ` K ) ` W ) e. DivRing <-> R e. DivRing ) )
18 7 17 mpbid 
 |-  ( ph -> R e. DivRing )