Metamath Proof Explorer

Theorem cntzsdrg

Description: Centralizers in division rings/fields are subfields. (Contributed by Mario Carneiro, 3-Oct-2015)

Ref Expression
Hypotheses cntzsdrg.b 
|- B = ( Base ` R )
cntzsdrg.m 
|- M = ( mulGrp ` R )
cntzsdrg.z 
|- Z = ( Cntz ` M )
Assertion cntzsdrg 
|- ( ( R e. DivRing /\ S C_ B ) -> ( Z ` S ) e. ( SubDRing ` R ) )

Proof

Step Hyp Ref Expression
1 cntzsdrg.b 
 |-  B = ( Base ` R )
2 cntzsdrg.m 
 |-  M = ( mulGrp ` R )
3 cntzsdrg.z 
 |-  Z = ( Cntz ` M )
4 simpl 
 |-  ( ( R e. DivRing /\ S C_ B ) -> R e. DivRing )
5 drngring 
 |-  ( R e. DivRing -> R e. Ring )
6 1 2 3 cntzsubr 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( Z ` S ) e. ( SubRing ` R ) )
7 5 6 sylan 
 |-  ( ( R e. DivRing /\ S C_ B ) -> ( Z ` S ) e. ( SubRing ` R ) )
8 oveq2 
 |-  ( y = ( 0g ` R ) -> ( ( ( invr ` R ) ` x ) ( .r ` R ) y ) = ( ( ( invr ` R ) ` x ) ( .r ` R ) ( 0g ` R ) ) )
9 oveq1 
 |-  ( y = ( 0g ` R ) -> ( y ( .r ` R ) ( ( invr ` R ) ` x ) ) = ( ( 0g ` R ) ( .r ` R ) ( ( invr ` R ) ` x ) ) )
10 8 9 eqeq12d 
 |-  ( y = ( 0g ` R ) -> ( ( ( ( invr ` R ) ` x ) ( .r ` R ) y ) = ( y ( .r ` R ) ( ( invr ` R ) ` x ) ) <-> ( ( ( invr ` R ) ` x ) ( .r ` R ) ( 0g ` R ) ) = ( ( 0g ` R ) ( .r ` R ) ( ( invr ` R ) ` x ) ) ) )
11 eldifsn 
 |-  ( y e. ( S \ { ( 0g ` R ) } ) <-> ( y e. S /\ y =/= ( 0g ` R ) ) )
12 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
13 2 oveq1i 
 |-  ( M |`s ( Unit ` R ) ) = ( ( mulGrp ` R ) |`s ( Unit ` R ) )
14 eqid 
 |-  ( invr ` R ) = ( invr ` R )
15 12 13 14 invrfval 
 |-  ( invr ` R ) = ( invg ` ( M |`s ( Unit ` R ) ) )
16 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
17 1 12 16 isdrng 
 |-  ( R e. DivRing <-> ( R e. Ring /\ ( Unit ` R ) = ( B \ { ( 0g ` R ) } ) ) )
18 17 simprbi 
 |-  ( R e. DivRing -> ( Unit ` R ) = ( B \ { ( 0g ` R ) } ) )
19 18 oveq2d 
 |-  ( R e. DivRing -> ( M |`s ( Unit ` R ) ) = ( M |`s ( B \ { ( 0g ` R ) } ) ) )
20 19 fveq2d 
 |-  ( R e. DivRing -> ( invg ` ( M |`s ( Unit ` R ) ) ) = ( invg ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) )
21 15 20 syl5eq 
 |-  ( R e. DivRing -> ( invr ` R ) = ( invg ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) )
22 21 ad2antrr 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> ( invr ` R ) = ( invg ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) )
23 22 fveq1d 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> ( ( invr ` R ) ` x ) = ( ( invg ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) ` x ) )
24 2 oveq1i 
 |-  ( M |`s ( B \ { ( 0g ` R ) } ) ) = ( ( mulGrp ` R ) |`s ( B \ { ( 0g ` R ) } ) )
25 1 16 24 drngmgp 
 |-  ( R e. DivRing -> ( M |`s ( B \ { ( 0g ` R ) } ) ) e. Grp )
26 25 ad2antrr 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> ( M |`s ( B \ { ( 0g ` R ) } ) ) e. Grp )
27 ssdif 
 |-  ( S C_ B -> ( S \ { ( 0g ` R ) } ) C_ ( B \ { ( 0g ` R ) } ) )
28 27 ad2antlr 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> ( S \ { ( 0g ` R ) } ) C_ ( B \ { ( 0g ` R ) } ) )
29 difss 
 |-  ( B \ { ( 0g ` R ) } ) C_ B
30 eqid 
 |-  ( M |`s ( B \ { ( 0g ` R ) } ) ) = ( M |`s ( B \ { ( 0g ` R ) } ) )
31 2 1 mgpbas 
 |-  B = ( Base ` M )
32 30 31 ressbas2 
 |-  ( ( B \ { ( 0g ` R ) } ) C_ B -> ( B \ { ( 0g ` R ) } ) = ( Base ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) )
33 29 32 ax-mp 
 |-  ( B \ { ( 0g ` R ) } ) = ( Base ` ( M |`s ( B \ { ( 0g ` R ) } ) ) )
34 eqid 
 |-  ( Cntz ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) = ( Cntz ` ( M |`s ( B \ { ( 0g ` R ) } ) ) )
35 33 34 cntzsubg 
 |-  ( ( ( M |`s ( B \ { ( 0g ` R ) } ) ) e. Grp /\ ( S \ { ( 0g ` R ) } ) C_ ( B \ { ( 0g ` R ) } ) ) -> ( ( Cntz ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) ` ( S \ { ( 0g ` R ) } ) ) e. ( SubGrp ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) )
36 26 28 35 syl2anc 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> ( ( Cntz ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) ` ( S \ { ( 0g ` R ) } ) ) e. ( SubGrp ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) )
37 simpr 
 |-  ( ( R e. DivRing /\ S C_ B ) -> S C_ B )
38 difss 
 |-  ( S \ { ( 0g ` R ) } ) C_ S
39 31 3 cntz2ss 
 |-  ( ( S C_ B /\ ( S \ { ( 0g ` R ) } ) C_ S ) -> ( Z ` S ) C_ ( Z ` ( S \ { ( 0g ` R ) } ) ) )
40 37 38 39 sylancl 
 |-  ( ( R e. DivRing /\ S C_ B ) -> ( Z ` S ) C_ ( Z ` ( S \ { ( 0g ` R ) } ) ) )
41 40 ssdifssd 
 |-  ( ( R e. DivRing /\ S C_ B ) -> ( ( Z ` S ) \ { ( 0g ` R ) } ) C_ ( Z ` ( S \ { ( 0g ` R ) } ) ) )
42 41 sselda 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> x e. ( Z ` ( S \ { ( 0g ` R ) } ) ) )
43 31 3 cntzssv 
 |-  ( Z ` S ) C_ B
44 ssdif 
 |-  ( ( Z ` S ) C_ B -> ( ( Z ` S ) \ { ( 0g ` R ) } ) C_ ( B \ { ( 0g ` R ) } ) )
45 43 44 mp1i 
 |-  ( ( R e. DivRing /\ S C_ B ) -> ( ( Z ` S ) \ { ( 0g ` R ) } ) C_ ( B \ { ( 0g ` R ) } ) )
46 45 sselda 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> x e. ( B \ { ( 0g ` R ) } ) )
47 42 46 elind 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> x e. ( ( Z ` ( S \ { ( 0g ` R ) } ) ) i^i ( B \ { ( 0g ` R ) } ) ) )
48 1 fvexi 
 |-  B e. _V
49 48 difexi 
 |-  ( B \ { ( 0g ` R ) } ) e. _V
50 30 3 34 resscntz 
 |-  ( ( ( B \ { ( 0g ` R ) } ) e. _V /\ ( S \ { ( 0g ` R ) } ) C_ ( B \ { ( 0g ` R ) } ) ) -> ( ( Cntz ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) ` ( S \ { ( 0g ` R ) } ) ) = ( ( Z ` ( S \ { ( 0g ` R ) } ) ) i^i ( B \ { ( 0g ` R ) } ) ) )
51 49 28 50 sylancr 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> ( ( Cntz ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) ` ( S \ { ( 0g ` R ) } ) ) = ( ( Z ` ( S \ { ( 0g ` R ) } ) ) i^i ( B \ { ( 0g ` R ) } ) ) )
52 47 51 eleqtrrd 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> x e. ( ( Cntz ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) ` ( S \ { ( 0g ` R ) } ) ) )
53 eqid 
 |-  ( invg ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) = ( invg ` ( M |`s ( B \ { ( 0g ` R ) } ) ) )
54 53 subginvcl 
 |-  ( ( ( ( Cntz ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) ` ( S \ { ( 0g ` R ) } ) ) e. ( SubGrp ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) /\ x e. ( ( Cntz ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) ` ( S \ { ( 0g ` R ) } ) ) ) -> ( ( invg ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) ` x ) e. ( ( Cntz ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) ` ( S \ { ( 0g ` R ) } ) ) )
55 36 52 54 syl2anc 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> ( ( invg ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) ` x ) e. ( ( Cntz ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) ` ( S \ { ( 0g ` R ) } ) ) )
56 23 55 eqeltrd 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> ( ( invr ` R ) ` x ) e. ( ( Cntz ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) ` ( S \ { ( 0g ` R ) } ) ) )
57 eqid 
 |-  ( .r ` R ) = ( .r ` R )
58 2 57 mgpplusg 
 |-  ( .r ` R ) = ( +g ` M )
59 30 58 ressplusg 
 |-  ( ( B \ { ( 0g ` R ) } ) e. _V -> ( .r ` R ) = ( +g ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) )
60 49 59 ax-mp 
 |-  ( .r ` R ) = ( +g ` ( M |`s ( B \ { ( 0g ` R ) } ) ) )
61 60 34 cntzi 
 |-  ( ( ( ( invr ` R ) ` x ) e. ( ( Cntz ` ( M |`s ( B \ { ( 0g ` R ) } ) ) ) ` ( S \ { ( 0g ` R ) } ) ) /\ y e. ( S \ { ( 0g ` R ) } ) ) -> ( ( ( invr ` R ) ` x ) ( .r ` R ) y ) = ( y ( .r ` R ) ( ( invr ` R ) ` x ) ) )
62 56 61 sylan 
 |-  ( ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) /\ y e. ( S \ { ( 0g ` R ) } ) ) -> ( ( ( invr ` R ) ` x ) ( .r ` R ) y ) = ( y ( .r ` R ) ( ( invr ` R ) ` x ) ) )
63 11 62 sylan2br 
 |-  ( ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) /\ ( y e. S /\ y =/= ( 0g ` R ) ) ) -> ( ( ( invr ` R ) ` x ) ( .r ` R ) y ) = ( y ( .r ` R ) ( ( invr ` R ) ` x ) ) )
64 63 anassrs 
 |-  ( ( ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) /\ y e. S ) /\ y =/= ( 0g ` R ) ) -> ( ( ( invr ` R ) ` x ) ( .r ` R ) y ) = ( y ( .r ` R ) ( ( invr ` R ) ` x ) ) )
65 5 ad3antrrr 
 |-  ( ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) /\ y e. S ) -> R e. Ring )
66 4 adantr 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> R e. DivRing )
67 eldifi 
 |-  ( x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) -> x e. ( Z ` S ) )
68 67 adantl 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> x e. ( Z ` S ) )
69 43 68 sseldi 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> x e. B )
70 eldifsni 
 |-  ( x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) -> x =/= ( 0g ` R ) )
71 70 adantl 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> x =/= ( 0g ` R ) )
72 1 16 14 drnginvrcl 
 |-  ( ( R e. DivRing /\ x e. B /\ x =/= ( 0g ` R ) ) -> ( ( invr ` R ) ` x ) e. B )
73 66 69 71 72 syl3anc 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> ( ( invr ` R ) ` x ) e. B )
74 73 adantr 
 |-  ( ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) /\ y e. S ) -> ( ( invr ` R ) ` x ) e. B )
75 1 57 16 ringrz 
 |-  ( ( R e. Ring /\ ( ( invr ` R ) ` x ) e. B ) -> ( ( ( invr ` R ) ` x ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
76 65 74 75 syl2anc 
 |-  ( ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) /\ y e. S ) -> ( ( ( invr ` R ) ` x ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
77 1 57 16 ringlz 
 |-  ( ( R e. Ring /\ ( ( invr ` R ) ` x ) e. B ) -> ( ( 0g ` R ) ( .r ` R ) ( ( invr ` R ) ` x ) ) = ( 0g ` R ) )
78 65 74 77 syl2anc 
 |-  ( ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) /\ y e. S ) -> ( ( 0g ` R ) ( .r ` R ) ( ( invr ` R ) ` x ) ) = ( 0g ` R ) )
79 76 78 eqtr4d 
 |-  ( ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) /\ y e. S ) -> ( ( ( invr ` R ) ` x ) ( .r ` R ) ( 0g ` R ) ) = ( ( 0g ` R ) ( .r ` R ) ( ( invr ` R ) ` x ) ) )
80 10 64 79 pm2.61ne 
 |-  ( ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) /\ y e. S ) -> ( ( ( invr ` R ) ` x ) ( .r ` R ) y ) = ( y ( .r ` R ) ( ( invr ` R ) ` x ) ) )
81 80 ralrimiva 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> A. y e. S ( ( ( invr ` R ) ` x ) ( .r ` R ) y ) = ( y ( .r ` R ) ( ( invr ` R ) ` x ) ) )
82 simplr 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> S C_ B )
83 31 58 3 cntzel 
 |-  ( ( S C_ B /\ ( ( invr ` R ) ` x ) e. B ) -> ( ( ( invr ` R ) ` x ) e. ( Z ` S ) <-> A. y e. S ( ( ( invr ` R ) ` x ) ( .r ` R ) y ) = ( y ( .r ` R ) ( ( invr ` R ) ` x ) ) ) )
84 82 73 83 syl2anc 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> ( ( ( invr ` R ) ` x ) e. ( Z ` S ) <-> A. y e. S ( ( ( invr ` R ) ` x ) ( .r ` R ) y ) = ( y ( .r ` R ) ( ( invr ` R ) ` x ) ) ) )
85 81 84 mpbird 
 |-  ( ( ( R e. DivRing /\ S C_ B ) /\ x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ) -> ( ( invr ` R ) ` x ) e. ( Z ` S ) )
86 85 ralrimiva 
 |-  ( ( R e. DivRing /\ S C_ B ) -> A. x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ( ( invr ` R ) ` x ) e. ( Z ` S ) )
87 14 16 issdrg2 
 |-  ( ( Z ` S ) e. ( SubDRing ` R ) <-> ( R e. DivRing /\ ( Z ` S ) e. ( SubRing ` R ) /\ A. x e. ( ( Z ` S ) \ { ( 0g ` R ) } ) ( ( invr ` R ) ` x ) e. ( Z ` S ) ) )
88 4 7 86 87 syl3anbrc 
 |-  ( ( R e. DivRing /\ S C_ B ) -> ( Z ` S ) e. ( SubDRing ` R ) )