Metamath Proof Explorer

Theorem sdrgacs

Description: Closure property of division subrings. (Contributed by Mario Carneiro, 3-Oct-2015)

Ref Expression
Hypothesis subrgacs.b 
|- B = ( Base ` R )
Assertion sdrgacs 
|- ( R e. DivRing -> ( SubDRing ` R ) e. ( ACS ` B ) )

Proof

Step Hyp Ref Expression
1 subrgacs.b 
 |-  B = ( Base ` R )
2 eqid 
 |-  ( invr ` R ) = ( invr ` R )
3 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
4 2 3 issdrg2 
 |-  ( s e. ( SubDRing ` R ) <-> ( R e. DivRing /\ s e. ( SubRing ` R ) /\ A. x e. ( s \ { ( 0g ` R ) } ) ( ( invr ` R ) ` x ) e. s ) )
5 3anass 
 |-  ( ( R e. DivRing /\ s e. ( SubRing ` R ) /\ A. x e. ( s \ { ( 0g ` R ) } ) ( ( invr ` R ) ` x ) e. s ) <-> ( R e. DivRing /\ ( s e. ( SubRing ` R ) /\ A. x e. ( s \ { ( 0g ` R ) } ) ( ( invr ` R ) ` x ) e. s ) ) )
6 4 5 bitri 
 |-  ( s e. ( SubDRing ` R ) <-> ( R e. DivRing /\ ( s e. ( SubRing ` R ) /\ A. x e. ( s \ { ( 0g ` R ) } ) ( ( invr ` R ) ` x ) e. s ) ) )
7 6 baib 
 |-  ( R e. DivRing -> ( s e. ( SubDRing ` R ) <-> ( s e. ( SubRing ` R ) /\ A. x e. ( s \ { ( 0g ` R ) } ) ( ( invr ` R ) ` x ) e. s ) ) )
8 1 subrgss 
 |-  ( s e. ( SubRing ` R ) -> s C_ B )
9 velpw 
 |-  ( s e. ~P B <-> s C_ B )
10 8 9 sylibr 
 |-  ( s e. ( SubRing ` R ) -> s e. ~P B )
11 10 adantl 
 |-  ( ( R e. DivRing /\ s e. ( SubRing ` R ) ) -> s e. ~P B )
12 iftrue 
 |-  ( x = ( 0g ` R ) -> if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) = x )
13 12 eleq1d 
 |-  ( x = ( 0g ` R ) -> ( if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y <-> x e. y ) )
14 13 biimprd 
 |-  ( x = ( 0g ` R ) -> ( x e. y -> if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y ) )
15 eldifsni 
 |-  ( x e. ( y \ { ( 0g ` R ) } ) -> x =/= ( 0g ` R ) )
16 15 necon2bi 
 |-  ( x = ( 0g ` R ) -> -. x e. ( y \ { ( 0g ` R ) } ) )
17 16 pm2.21d 
 |-  ( x = ( 0g ` R ) -> ( x e. ( y \ { ( 0g ` R ) } ) -> ( ( invr ` R ) ` x ) e. y ) )
18 14 17 2thd 
 |-  ( x = ( 0g ` R ) -> ( ( x e. y -> if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y ) <-> ( x e. ( y \ { ( 0g ` R ) } ) -> ( ( invr ` R ) ` x ) e. y ) ) )
19 eldifsn 
 |-  ( x e. ( y \ { ( 0g ` R ) } ) <-> ( x e. y /\ x =/= ( 0g ` R ) ) )
20 19 rbaibr 
 |-  ( x =/= ( 0g ` R ) -> ( x e. y <-> x e. ( y \ { ( 0g ` R ) } ) ) )
21 ifnefalse 
 |-  ( x =/= ( 0g ` R ) -> if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) = ( ( invr ` R ) ` x ) )
22 21 eleq1d 
 |-  ( x =/= ( 0g ` R ) -> ( if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y <-> ( ( invr ` R ) ` x ) e. y ) )
23 20 22 imbi12d 
 |-  ( x =/= ( 0g ` R ) -> ( ( x e. y -> if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y ) <-> ( x e. ( y \ { ( 0g ` R ) } ) -> ( ( invr ` R ) ` x ) e. y ) ) )
24 18 23 pm2.61ine 
 |-  ( ( x e. y -> if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y ) <-> ( x e. ( y \ { ( 0g ` R ) } ) -> ( ( invr ` R ) ` x ) e. y ) )
25 24 ralbii2 
 |-  ( A. x e. y if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y <-> A. x e. ( y \ { ( 0g ` R ) } ) ( ( invr ` R ) ` x ) e. y )
26 difeq1 
 |-  ( y = s -> ( y \ { ( 0g ` R ) } ) = ( s \ { ( 0g ` R ) } ) )
27 eleq2w 
 |-  ( y = s -> ( ( ( invr ` R ) ` x ) e. y <-> ( ( invr ` R ) ` x ) e. s ) )
28 26 27 raleqbidv 
 |-  ( y = s -> ( A. x e. ( y \ { ( 0g ` R ) } ) ( ( invr ` R ) ` x ) e. y <-> A. x e. ( s \ { ( 0g ` R ) } ) ( ( invr ` R ) ` x ) e. s ) )
29 25 28 syl5bb 
 |-  ( y = s -> ( A. x e. y if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y <-> A. x e. ( s \ { ( 0g ` R ) } ) ( ( invr ` R ) ` x ) e. s ) )
30 29 elrab3 
 |-  ( s e. ~P B -> ( s e. { y e. ~P B | A. x e. y if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y } <-> A. x e. ( s \ { ( 0g ` R ) } ) ( ( invr ` R ) ` x ) e. s ) )
31 11 30 syl 
 |-  ( ( R e. DivRing /\ s e. ( SubRing ` R ) ) -> ( s e. { y e. ~P B | A. x e. y if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y } <-> A. x e. ( s \ { ( 0g ` R ) } ) ( ( invr ` R ) ` x ) e. s ) )
32 31 pm5.32da 
 |-  ( R e. DivRing -> ( ( s e. ( SubRing ` R ) /\ s e. { y e. ~P B | A. x e. y if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y } ) <-> ( s e. ( SubRing ` R ) /\ A. x e. ( s \ { ( 0g ` R ) } ) ( ( invr ` R ) ` x ) e. s ) ) )
33 7 32 bitr4d 
 |-  ( R e. DivRing -> ( s e. ( SubDRing ` R ) <-> ( s e. ( SubRing ` R ) /\ s e. { y e. ~P B | A. x e. y if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y } ) ) )
34 elin 
 |-  ( s e. ( ( SubRing ` R ) i^i { y e. ~P B | A. x e. y if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y } ) <-> ( s e. ( SubRing ` R ) /\ s e. { y e. ~P B | A. x e. y if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y } ) )
35 33 34 bitr4di 
 |-  ( R e. DivRing -> ( s e. ( SubDRing ` R ) <-> s e. ( ( SubRing ` R ) i^i { y e. ~P B | A. x e. y if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y } ) ) )
36 35 eqrdv 
 |-  ( R e. DivRing -> ( SubDRing ` R ) = ( ( SubRing ` R ) i^i { y e. ~P B | A. x e. y if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y } ) )
37 1 fvexi 
 |-  B e. _V
38 mreacs 
 |-  ( B e. _V -> ( ACS ` B ) e. ( Moore ` ~P B ) )
39 37 38 mp1i 
 |-  ( R e. DivRing -> ( ACS ` B ) e. ( Moore ` ~P B ) )
40 drngring 
 |-  ( R e. DivRing -> R e. Ring )
41 1 subrgacs 
 |-  ( R e. Ring -> ( SubRing ` R ) e. ( ACS ` B ) )
42 40 41 syl 
 |-  ( R e. DivRing -> ( SubRing ` R ) e. ( ACS ` B ) )
43 simplr 
 |-  ( ( ( R e. DivRing /\ x e. B ) /\ x = ( 0g ` R ) ) -> x e. B )
44 df-ne 
 |-  ( x =/= ( 0g ` R ) <-> -. x = ( 0g ` R ) )
45 1 3 2 drnginvrcl 
 |-  ( ( R e. DivRing /\ x e. B /\ x =/= ( 0g ` R ) ) -> ( ( invr ` R ) ` x ) e. B )
46 45 3expa 
 |-  ( ( ( R e. DivRing /\ x e. B ) /\ x =/= ( 0g ` R ) ) -> ( ( invr ` R ) ` x ) e. B )
47 44 46 sylan2br 
 |-  ( ( ( R e. DivRing /\ x e. B ) /\ -. x = ( 0g ` R ) ) -> ( ( invr ` R ) ` x ) e. B )
48 43 47 ifclda 
 |-  ( ( R e. DivRing /\ x e. B ) -> if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. B )
49 48 ralrimiva 
 |-  ( R e. DivRing -> A. x e. B if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. B )
50 acsfn1 
 |-  ( ( B e. _V /\ A. x e. B if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. B ) -> { y e. ~P B | A. x e. y if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y } e. ( ACS ` B ) )
51 37 49 50 sylancr 
 |-  ( R e. DivRing -> { y e. ~P B | A. x e. y if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y } e. ( ACS ` B ) )
52 mreincl 
 |-  ( ( ( ACS ` B ) e. ( Moore ` ~P B ) /\ ( SubRing ` R ) e. ( ACS ` B ) /\ { y e. ~P B | A. x e. y if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y } e. ( ACS ` B ) ) -> ( ( SubRing ` R ) i^i { y e. ~P B | A. x e. y if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y } ) e. ( ACS ` B ) )
53 39 42 51 52 syl3anc 
 |-  ( R e. DivRing -> ( ( SubRing ` R ) i^i { y e. ~P B | A. x e. y if ( x = ( 0g ` R ) , x , ( ( invr ` R ) ` x ) ) e. y } ) e. ( ACS ` B ) )
54 36 53 eqeltrd 
 |-  ( R e. DivRing -> ( SubDRing ` R ) e. ( ACS ` B ) )