Metamath Proof Explorer

Theorem issdrg

Description: Property of a division subring. (Contributed by Stefan O'Rear, 3-Oct-2015)

Ref Expression
Assertion issdrg 
|- ( S e. ( SubDRing ` R ) <-> ( R e. DivRing /\ S e. ( SubRing ` R ) /\ ( R |`s S ) e. DivRing ) )

Proof

Step Hyp Ref Expression
1 df-sdrg 
 |-  SubDRing = ( w e. DivRing |-> { s e. ( SubRing ` w ) | ( w |`s s ) e. DivRing } )
2 1 mptrcl 
 |-  ( S e. ( SubDRing ` R ) -> R e. DivRing )
3 fveq2 
 |-  ( w = R -> ( SubRing ` w ) = ( SubRing ` R ) )
4 oveq1 
 |-  ( w = R -> ( w |`s s ) = ( R |`s s ) )
5 4 eleq1d 
 |-  ( w = R -> ( ( w |`s s ) e. DivRing <-> ( R |`s s ) e. DivRing ) )
6 3 5 rabeqbidv 
 |-  ( w = R -> { s e. ( SubRing ` w ) | ( w |`s s ) e. DivRing } = { s e. ( SubRing ` R ) | ( R |`s s ) e. DivRing } )
7 fvex 
 |-  ( SubRing ` R ) e. _V
8 7 rabex 
 |-  { s e. ( SubRing ` R ) | ( R |`s s ) e. DivRing } e. _V
9 6 1 8 fvmpt 
 |-  ( R e. DivRing -> ( SubDRing ` R ) = { s e. ( SubRing ` R ) | ( R |`s s ) e. DivRing } )
10 9 eleq2d 
 |-  ( R e. DivRing -> ( S e. ( SubDRing ` R ) <-> S e. { s e. ( SubRing ` R ) | ( R |`s s ) e. DivRing } ) )
11 oveq2 
 |-  ( s = S -> ( R |`s s ) = ( R |`s S ) )
12 11 eleq1d 
 |-  ( s = S -> ( ( R |`s s ) e. DivRing <-> ( R |`s S ) e. DivRing ) )
13 12 elrab 
 |-  ( S e. { s e. ( SubRing ` R ) | ( R |`s s ) e. DivRing } <-> ( S e. ( SubRing ` R ) /\ ( R |`s S ) e. DivRing ) )
14 10 13 bitrdi 
 |-  ( R e. DivRing -> ( S e. ( SubDRing ` R ) <-> ( S e. ( SubRing ` R ) /\ ( R |`s S ) e. DivRing ) ) )
15 2 14 biadanii 
 |-  ( S e. ( SubDRing ` R ) <-> ( R e. DivRing /\ ( S e. ( SubRing ` R ) /\ ( R |`s S ) e. DivRing ) ) )
16 3anass 
 |-  ( ( R e. DivRing /\ S e. ( SubRing ` R ) /\ ( R |`s S ) e. DivRing ) <-> ( R e. DivRing /\ ( S e. ( SubRing ` R ) /\ ( R |`s S ) e. DivRing ) ) )
17 15 16 bitr4i 
 |-  ( S e. ( SubDRing ` R ) <-> ( R e. DivRing /\ S e. ( SubRing ` R ) /\ ( R |`s S ) e. DivRing ) )