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