Metamath Proof Explorer

Theorem issdrg2

Description: Property of a division subring (closure version). (Contributed by Mario Carneiro, 3-Oct-2015)

Ref Expression
Hypotheses issdrg2.i 
|- I = ( invr ` R )
issdrg2.z 
|- .0. = ( 0g ` R )
Assertion issdrg2 
|- ( S e. ( SubDRing ` R ) <-> ( R e. DivRing /\ S e. ( SubRing ` R ) /\ A. x e. ( S \ { .0. } ) ( I ` x ) e. S ) )

Proof

Step Hyp Ref Expression
1 issdrg2.i 
 |-  I = ( invr ` R )
2 issdrg2.z 
 |-  .0. = ( 0g ` R )
3 issdrg 
 |-  ( S e. ( SubDRing ` R ) <-> ( R e. DivRing /\ S e. ( SubRing ` R ) /\ ( R |`s S ) e. DivRing ) )
4 eqid 
 |-  ( R |`s S ) = ( R |`s S )
5 4 2 1 issubdrg 
 |-  ( ( R e. DivRing /\ S e. ( SubRing ` R ) ) -> ( ( R |`s S ) e. DivRing <-> A. x e. ( S \ { .0. } ) ( I ` x ) e. S ) )
6 5 pm5.32i 
 |-  ( ( ( R e. DivRing /\ S e. ( SubRing ` R ) ) /\ ( R |`s S ) e. DivRing ) <-> ( ( R e. DivRing /\ S e. ( SubRing ` R ) ) /\ A. x e. ( S \ { .0. } ) ( I ` x ) e. S ) )
7 df-3an 
 |-  ( ( R e. DivRing /\ S e. ( SubRing ` R ) /\ ( R |`s S ) e. DivRing ) <-> ( ( R e. DivRing /\ S e. ( SubRing ` R ) ) /\ ( R |`s S ) e. DivRing ) )
8 df-3an 
 |-  ( ( R e. DivRing /\ S e. ( SubRing ` R ) /\ A. x e. ( S \ { .0. } ) ( I ` x ) e. S ) <-> ( ( R e. DivRing /\ S e. ( SubRing ` R ) ) /\ A. x e. ( S \ { .0. } ) ( I ` x ) e. S ) )
9 6 7 8 3bitr4i 
 |-  ( ( R e. DivRing /\ S e. ( SubRing ` R ) /\ ( R |`s S ) e. DivRing ) <-> ( R e. DivRing /\ S e. ( SubRing ` R ) /\ A. x e. ( S \ { .0. } ) ( I ` x ) e. S ) )
10 3 9 bitri 
 |-  ( S e. ( SubDRing ` R ) <-> ( R e. DivRing /\ S e. ( SubRing ` R ) /\ A. x e. ( S \ { .0. } ) ( I ` x ) e. S ) )