Metamath Proof Explorer

Theorem issubrg

Description: The subring predicate. (Contributed by Stefan O'Rear, 27-Nov-2014) (Proof shortened by AV, 12-Oct-2020)

Ref Expression
Hypotheses issubrg.b 
|- B = ( Base ` R )
issubrg.i 
|- .1. = ( 1r ` R )
Assertion issubrg 
|- ( A e. ( SubRing ` R ) <-> ( ( R e. Ring /\ ( R |`s A ) e. Ring ) /\ ( A C_ B /\ .1. e. A ) ) )

Proof

Step Hyp Ref Expression
1 issubrg.b 
 |-  B = ( Base ` R )
2 issubrg.i 
 |-  .1. = ( 1r ` R )
3 df-subrg 
 |-  SubRing = ( r e. Ring |-> { s e. ~P ( Base ` r ) | ( ( r |`s s ) e. Ring /\ ( 1r ` r ) e. s ) } )
4 3 mptrcl 
 |-  ( A e. ( SubRing ` R ) -> R e. Ring )
5 simpll 
 |-  ( ( ( R e. Ring /\ ( R |`s A ) e. Ring ) /\ ( A C_ B /\ .1. e. A ) ) -> R e. Ring )
6 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
7 6 1 eqtr4di 
 |-  ( r = R -> ( Base ` r ) = B )
8 7 pweqd 
 |-  ( r = R -> ~P ( Base ` r ) = ~P B )
9 oveq1 
 |-  ( r = R -> ( r |`s s ) = ( R |`s s ) )
10 9 eleq1d 
 |-  ( r = R -> ( ( r |`s s ) e. Ring <-> ( R |`s s ) e. Ring ) )
11 fveq2 
 |-  ( r = R -> ( 1r ` r ) = ( 1r ` R ) )
12 11 2 eqtr4di 
 |-  ( r = R -> ( 1r ` r ) = .1. )
13 12 eleq1d 
 |-  ( r = R -> ( ( 1r ` r ) e. s <-> .1. e. s ) )
14 10 13 anbi12d 
 |-  ( r = R -> ( ( ( r |`s s ) e. Ring /\ ( 1r ` r ) e. s ) <-> ( ( R |`s s ) e. Ring /\ .1. e. s ) ) )
15 8 14 rabeqbidv 
 |-  ( r = R -> { s e. ~P ( Base ` r ) | ( ( r |`s s ) e. Ring /\ ( 1r ` r ) e. s ) } = { s e. ~P B | ( ( R |`s s ) e. Ring /\ .1. e. s ) } )
16 1 fvexi 
 |-  B e. _V
17 16 pwex 
 |-  ~P B e. _V
18 17 rabex 
 |-  { s e. ~P B | ( ( R |`s s ) e. Ring /\ .1. e. s ) } e. _V
19 15 3 18 fvmpt 
 |-  ( R e. Ring -> ( SubRing ` R ) = { s e. ~P B | ( ( R |`s s ) e. Ring /\ .1. e. s ) } )
20 19 eleq2d 
 |-  ( R e. Ring -> ( A e. ( SubRing ` R ) <-> A e. { s e. ~P B | ( ( R |`s s ) e. Ring /\ .1. e. s ) } ) )
21 oveq2 
 |-  ( s = A -> ( R |`s s ) = ( R |`s A ) )
22 21 eleq1d 
 |-  ( s = A -> ( ( R |`s s ) e. Ring <-> ( R |`s A ) e. Ring ) )
23 eleq2 
 |-  ( s = A -> ( .1. e. s <-> .1. e. A ) )
24 22 23 anbi12d 
 |-  ( s = A -> ( ( ( R |`s s ) e. Ring /\ .1. e. s ) <-> ( ( R |`s A ) e. Ring /\ .1. e. A ) ) )
25 24 elrab 
 |-  ( A e. { s e. ~P B | ( ( R |`s s ) e. Ring /\ .1. e. s ) } <-> ( A e. ~P B /\ ( ( R |`s A ) e. Ring /\ .1. e. A ) ) )
26 16 elpw2 
 |-  ( A e. ~P B <-> A C_ B )
27 26 anbi1i 
 |-  ( ( A e. ~P B /\ ( ( R |`s A ) e. Ring /\ .1. e. A ) ) <-> ( A C_ B /\ ( ( R |`s A ) e. Ring /\ .1. e. A ) ) )
28 an12 
 |-  ( ( A C_ B /\ ( ( R |`s A ) e. Ring /\ .1. e. A ) ) <-> ( ( R |`s A ) e. Ring /\ ( A C_ B /\ .1. e. A ) ) )
29 25 27 28 3bitri 
 |-  ( A e. { s e. ~P B | ( ( R |`s s ) e. Ring /\ .1. e. s ) } <-> ( ( R |`s A ) e. Ring /\ ( A C_ B /\ .1. e. A ) ) )
30 ibar 
 |-  ( R e. Ring -> ( ( R |`s A ) e. Ring <-> ( R e. Ring /\ ( R |`s A ) e. Ring ) ) )
31 30 anbi1d 
 |-  ( R e. Ring -> ( ( ( R |`s A ) e. Ring /\ ( A C_ B /\ .1. e. A ) ) <-> ( ( R e. Ring /\ ( R |`s A ) e. Ring ) /\ ( A C_ B /\ .1. e. A ) ) ) )
32 29 31 syl5bb 
 |-  ( R e. Ring -> ( A e. { s e. ~P B | ( ( R |`s s ) e. Ring /\ .1. e. s ) } <-> ( ( R e. Ring /\ ( R |`s A ) e. Ring ) /\ ( A C_ B /\ .1. e. A ) ) ) )
33 20 32 bitrd 
 |-  ( R e. Ring -> ( A e. ( SubRing ` R ) <-> ( ( R e. Ring /\ ( R |`s A ) e. Ring ) /\ ( A C_ B /\ .1. e. A ) ) ) )
34 4 5 33 pm5.21nii 
 |-  ( A e. ( SubRing ` R ) <-> ( ( R e. Ring /\ ( R |`s A ) e. Ring ) /\ ( A C_ B /\ .1. e. A ) ) )