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 eqtrid
 |-  ( 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 sselid
 |-  ( ( ( 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 ) )