Metamath Proof Explorer

Theorem issubdrg

Description: Characterize the subfields of a division ring. (Contributed by Mario Carneiro, 3-Dec-2014)

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

Proof

Step Hyp Ref Expression
1 issubdrg.s 
 |-  S = ( R |`s A )
2 issubdrg.z 
 |-  .0. = ( 0g ` R )
3 issubdrg.i 
 |-  I = ( invr ` R )
4 simpllr 
 |-  ( ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ S e. DivRing ) /\ x e. ( A \ { .0. } ) ) -> A e. ( SubRing ` R ) )
5 1 subrgring 
 |-  ( A e. ( SubRing ` R ) -> S e. Ring )
6 4 5 syl 
 |-  ( ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ S e. DivRing ) /\ x e. ( A \ { .0. } ) ) -> S e. Ring )
7 eldifsn 
 |-  ( x e. ( A \ { .0. } ) <-> ( x e. A /\ x =/= .0. ) )
8 7 bilani 
 |-  ( ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ S e. DivRing ) /\ x e. ( A \ { .0. } ) ) -> ( x e. A /\ x =/= .0. ) )
9 8 simpld 
 |-  ( ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ S e. DivRing ) /\ x e. ( A \ { .0. } ) ) -> x e. A )
10 1 subrgbas 
 |-  ( A e. ( SubRing ` R ) -> A = ( Base ` S ) )
11 4 10 syl 
 |-  ( ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ S e. DivRing ) /\ x e. ( A \ { .0. } ) ) -> A = ( Base ` S ) )
12 9 11 eleqtrd 
 |-  ( ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ S e. DivRing ) /\ x e. ( A \ { .0. } ) ) -> x e. ( Base ` S ) )
13 8 simprd 
 |-  ( ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ S e. DivRing ) /\ x e. ( A \ { .0. } ) ) -> x =/= .0. )
14 1 2 subrg0 
 |-  ( A e. ( SubRing ` R ) -> .0. = ( 0g ` S ) )
15 4 14 syl 
 |-  ( ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ S e. DivRing ) /\ x e. ( A \ { .0. } ) ) -> .0. = ( 0g ` S ) )
16 13 15 neeqtrd 
 |-  ( ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ S e. DivRing ) /\ x e. ( A \ { .0. } ) ) -> x =/= ( 0g ` S ) )
17 eqid 
 |-  ( Base ` S ) = ( Base ` S )
18 eqid 
 |-  ( Unit ` S ) = ( Unit ` S )
19 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
20 17 18 19 drngunit 
 |-  ( S e. DivRing -> ( x e. ( Unit ` S ) <-> ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) )
21 20 ad2antlr 
 |-  ( ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ S e. DivRing ) /\ x e. ( A \ { .0. } ) ) -> ( x e. ( Unit ` S ) <-> ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) )
22 12 16 21 mpbir2and 
 |-  ( ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ S e. DivRing ) /\ x e. ( A \ { .0. } ) ) -> x e. ( Unit ` S ) )
23 eqid 
 |-  ( invr ` S ) = ( invr ` S )
24 18 23 17 ringinvcl 
 |-  ( ( S e. Ring /\ x e. ( Unit ` S ) ) -> ( ( invr ` S ) ` x ) e. ( Base ` S ) )
25 6 22 24 syl2anc 
 |-  ( ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ S e. DivRing ) /\ x e. ( A \ { .0. } ) ) -> ( ( invr ` S ) ` x ) e. ( Base ` S ) )
26 1 3 18 23 subrginv 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. ( Unit ` S ) ) -> ( I ` x ) = ( ( invr ` S ) ` x ) )
27 4 22 26 syl2anc 
 |-  ( ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ S e. DivRing ) /\ x e. ( A \ { .0. } ) ) -> ( I ` x ) = ( ( invr ` S ) ` x ) )
28 25 27 11 3eltr4d 
 |-  ( ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ S e. DivRing ) /\ x e. ( A \ { .0. } ) ) -> ( I ` x ) e. A )
29 28 ralrimiva 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ S e. DivRing ) -> A. x e. ( A \ { .0. } ) ( I ` x ) e. A )
30 5 ad2antlr 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) -> S e. Ring )
31 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
32 1 31 18 subrguss 
 |-  ( A e. ( SubRing ` R ) -> ( Unit ` S ) C_ ( Unit ` R ) )
33 32 ad2antlr 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) -> ( Unit ` S ) C_ ( Unit ` R ) )
34 eqid 
 |-  ( Base ` R ) = ( Base ` R )
35 34 31 2 isdrng 
 |-  ( R e. DivRing <-> ( R e. Ring /\ ( Unit ` R ) = ( ( Base ` R ) \ { .0. } ) ) )
36 35 simprbi 
 |-  ( R e. DivRing -> ( Unit ` R ) = ( ( Base ` R ) \ { .0. } ) )
37 36 ad2antrr 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) -> ( Unit ` R ) = ( ( Base ` R ) \ { .0. } ) )
38 33 37 sseqtrd 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) -> ( Unit ` S ) C_ ( ( Base ` R ) \ { .0. } ) )
39 17 18 unitss 
 |-  ( Unit ` S ) C_ ( Base ` S )
40 10 ad2antlr 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) -> A = ( Base ` S ) )
41 39 40 sseqtrrid 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) -> ( Unit ` S ) C_ A )
42 38 41 ssind 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) -> ( Unit ` S ) C_ ( ( ( Base ` R ) \ { .0. } ) i^i A ) )
43 34 subrgss 
 |-  ( A e. ( SubRing ` R ) -> A C_ ( Base ` R ) )
44 43 ad2antlr 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) -> A C_ ( Base ` R ) )
45 difin2 
 |-  ( A C_ ( Base ` R ) -> ( A \ { .0. } ) = ( ( ( Base ` R ) \ { .0. } ) i^i A ) )
46 44 45 syl 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) -> ( A \ { .0. } ) = ( ( ( Base ` R ) \ { .0. } ) i^i A ) )
47 42 46 sseqtrrd 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) -> ( Unit ` S ) C_ ( A \ { .0. } ) )
48 43 ad2antlr 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ ( x e. ( A \ { .0. } ) /\ ( I ` x ) e. A ) ) -> A C_ ( Base ` R ) )
49 simprl 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ ( x e. ( A \ { .0. } ) /\ ( I ` x ) e. A ) ) -> x e. ( A \ { .0. } ) )
50 49 7 sylib 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ ( x e. ( A \ { .0. } ) /\ ( I ` x ) e. A ) ) -> ( x e. A /\ x =/= .0. ) )
51 50 simpld 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ ( x e. ( A \ { .0. } ) /\ ( I ` x ) e. A ) ) -> x e. A )
52 48 51 sseldd 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ ( x e. ( A \ { .0. } ) /\ ( I ` x ) e. A ) ) -> x e. ( Base ` R ) )
53 50 simprd 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ ( x e. ( A \ { .0. } ) /\ ( I ` x ) e. A ) ) -> x =/= .0. )
54 34 31 2 drngunit 
 |-  ( R e. DivRing -> ( x e. ( Unit ` R ) <-> ( x e. ( Base ` R ) /\ x =/= .0. ) ) )
55 54 ad2antrr 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ ( x e. ( A \ { .0. } ) /\ ( I ` x ) e. A ) ) -> ( x e. ( Unit ` R ) <-> ( x e. ( Base ` R ) /\ x =/= .0. ) ) )
56 52 53 55 mpbir2and 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ ( x e. ( A \ { .0. } ) /\ ( I ` x ) e. A ) ) -> x e. ( Unit ` R ) )
57 simprr 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ ( x e. ( A \ { .0. } ) /\ ( I ` x ) e. A ) ) -> ( I ` x ) e. A )
58 1 31 18 3 subrgunit 
 |-  ( A e. ( SubRing ` R ) -> ( x e. ( Unit ` S ) <-> ( x e. ( Unit ` R ) /\ x e. A /\ ( I ` x ) e. A ) ) )
59 58 ad2antlr 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ ( x e. ( A \ { .0. } ) /\ ( I ` x ) e. A ) ) -> ( x e. ( Unit ` S ) <-> ( x e. ( Unit ` R ) /\ x e. A /\ ( I ` x ) e. A ) ) )
60 56 51 57 59 mpbir3and 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ ( x e. ( A \ { .0. } ) /\ ( I ` x ) e. A ) ) -> x e. ( Unit ` S ) )
61 60 expr 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ x e. ( A \ { .0. } ) ) -> ( ( I ` x ) e. A -> x e. ( Unit ` S ) ) )
62 61 ralimdva 
 |-  ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) -> ( A. x e. ( A \ { .0. } ) ( I ` x ) e. A -> A. x e. ( A \ { .0. } ) x e. ( Unit ` S ) ) )
63 62 imp 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) -> A. x e. ( A \ { .0. } ) x e. ( Unit ` S ) )
64 dfss3 
 |-  ( ( A \ { .0. } ) C_ ( Unit ` S ) <-> A. x e. ( A \ { .0. } ) x e. ( Unit ` S ) )
65 63 64 sylibr 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) -> ( A \ { .0. } ) C_ ( Unit ` S ) )
66 47 65 eqssd 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) -> ( Unit ` S ) = ( A \ { .0. } ) )
67 14 ad2antlr 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) -> .0. = ( 0g ` S ) )
68 67 sneqd 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) -> { .0. } = { ( 0g ` S ) } )
69 40 68 difeq12d 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) -> ( A \ { .0. } ) = ( ( Base ` S ) \ { ( 0g ` S ) } ) )
70 66 69 eqtrd 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) -> ( Unit ` S ) = ( ( Base ` S ) \ { ( 0g ` S ) } ) )
71 17 18 19 isdrng 
 |-  ( S e. DivRing <-> ( S e. Ring /\ ( Unit ` S ) = ( ( Base ` S ) \ { ( 0g ` S ) } ) ) )
72 30 70 71 sylanbrc 
 |-  ( ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) /\ A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) -> S e. DivRing )
73 29 72 impbida 
 |-  ( ( R e. DivRing /\ A e. ( SubRing ` R ) ) -> ( S e. DivRing <-> A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) )