Metamath Proof Explorer

Theorem cntzsubr

Description: Centralizers in a ring are subrings. (Contributed by Stefan O'Rear, 6-Sep-2015) (Revised by Mario Carneiro, 19-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 cntzsubr.b 
 |-  B = ( Base ` R )
2 cntzsubr.m 
 |-  M = ( mulGrp ` R )
3 cntzsubr.z 
 |-  Z = ( Cntz ` M )
4 2 1 mgpbas 
 |-  B = ( Base ` M )
5 4 3 cntzssv 
 |-  ( Z ` S ) C_ B
6 5 a1i 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( Z ` S ) C_ B )
7 simpll 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ z e. S ) -> R e. Ring )
8 ssel2 
 |-  ( ( S C_ B /\ z e. S ) -> z e. B )
9 8 adantll 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ z e. S ) -> z e. B )
10 eqid 
 |-  ( .r ` R ) = ( .r ` R )
11 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
12 1 10 11 ringlz 
 |-  ( ( R e. Ring /\ z e. B ) -> ( ( 0g ` R ) ( .r ` R ) z ) = ( 0g ` R ) )
13 7 9 12 syl2anc 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ z e. S ) -> ( ( 0g ` R ) ( .r ` R ) z ) = ( 0g ` R ) )
14 1 10 11 ringrz 
 |-  ( ( R e. Ring /\ z e. B ) -> ( z ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
15 7 9 14 syl2anc 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ z e. S ) -> ( z ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
16 13 15 eqtr4d 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ z e. S ) -> ( ( 0g ` R ) ( .r ` R ) z ) = ( z ( .r ` R ) ( 0g ` R ) ) )
17 16 ralrimiva 
 |-  ( ( R e. Ring /\ S C_ B ) -> A. z e. S ( ( 0g ` R ) ( .r ` R ) z ) = ( z ( .r ` R ) ( 0g ` R ) ) )
18 simpr 
 |-  ( ( R e. Ring /\ S C_ B ) -> S C_ B )
19 1 11 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. B )
20 19 adantr 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( 0g ` R ) e. B )
21 2 10 mgpplusg 
 |-  ( .r ` R ) = ( +g ` M )
22 4 21 3 cntzel 
 |-  ( ( S C_ B /\ ( 0g ` R ) e. B ) -> ( ( 0g ` R ) e. ( Z ` S ) <-> A. z e. S ( ( 0g ` R ) ( .r ` R ) z ) = ( z ( .r ` R ) ( 0g ` R ) ) ) )
23 18 20 22 syl2anc 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( ( 0g ` R ) e. ( Z ` S ) <-> A. z e. S ( ( 0g ` R ) ( .r ` R ) z ) = ( z ( .r ` R ) ( 0g ` R ) ) ) )
24 17 23 mpbird 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( 0g ` R ) e. ( Z ` S ) )
25 24 ne0d 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( Z ` S ) =/= (/) )
26 simpl2 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> x e. ( Z ` S ) )
27 simpr 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> z e. S )
28 21 3 cntzi 
 |-  ( ( x e. ( Z ` S ) /\ z e. S ) -> ( x ( .r ` R ) z ) = ( z ( .r ` R ) x ) )
29 26 27 28 syl2anc 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> ( x ( .r ` R ) z ) = ( z ( .r ` R ) x ) )
30 simpl3 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> y e. ( Z ` S ) )
31 21 3 cntzi 
 |-  ( ( y e. ( Z ` S ) /\ z e. S ) -> ( y ( .r ` R ) z ) = ( z ( .r ` R ) y ) )
32 30 27 31 syl2anc 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> ( y ( .r ` R ) z ) = ( z ( .r ` R ) y ) )
33 29 32 oveq12d 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) = ( ( z ( .r ` R ) x ) ( +g ` R ) ( z ( .r ` R ) y ) ) )
34 simpl1l 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> R e. Ring )
35 5 26 sseldi 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> x e. B )
36 5 30 sseldi 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> y e. B )
37 simp1r 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) -> S C_ B )
38 37 sselda 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> z e. B )
39 eqid 
 |-  ( +g ` R ) = ( +g ` R )
40 1 39 10 ringdir 
 |-  ( ( R e. Ring /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) )
41 34 35 36 38 40 syl13anc 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) )
42 1 39 10 ringdi 
 |-  ( ( R e. Ring /\ ( z e. B /\ x e. B /\ y e. B ) ) -> ( z ( .r ` R ) ( x ( +g ` R ) y ) ) = ( ( z ( .r ` R ) x ) ( +g ` R ) ( z ( .r ` R ) y ) ) )
43 34 38 35 36 42 syl13anc 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> ( z ( .r ` R ) ( x ( +g ` R ) y ) ) = ( ( z ( .r ` R ) x ) ( +g ` R ) ( z ( .r ` R ) y ) ) )
44 33 41 43 3eqtr4d 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( z ( .r ` R ) ( x ( +g ` R ) y ) ) )
45 44 ralrimiva 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) -> A. z e. S ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( z ( .r ` R ) ( x ( +g ` R ) y ) ) )
46 simp1l 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) -> R e. Ring )
47 simp2 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) -> x e. ( Z ` S ) )
48 5 47 sseldi 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) -> x e. B )
49 simp3 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) -> y e. ( Z ` S ) )
50 5 49 sseldi 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) -> y e. B )
51 1 39 ringacl 
 |-  ( ( R e. Ring /\ x e. B /\ y e. B ) -> ( x ( +g ` R ) y ) e. B )
52 46 48 50 51 syl3anc 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) -> ( x ( +g ` R ) y ) e. B )
53 4 21 3 cntzel 
 |-  ( ( S C_ B /\ ( x ( +g ` R ) y ) e. B ) -> ( ( x ( +g ` R ) y ) e. ( Z ` S ) <-> A. z e. S ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( z ( .r ` R ) ( x ( +g ` R ) y ) ) ) )
54 37 52 53 syl2anc 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) -> ( ( x ( +g ` R ) y ) e. ( Z ` S ) <-> A. z e. S ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( z ( .r ` R ) ( x ( +g ` R ) y ) ) ) )
55 45 54 mpbird 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) -> ( x ( +g ` R ) y ) e. ( Z ` S ) )
56 55 3expa 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ y e. ( Z ` S ) ) -> ( x ( +g ` R ) y ) e. ( Z ` S ) )
57 56 ralrimiva 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) -> A. y e. ( Z ` S ) ( x ( +g ` R ) y ) e. ( Z ` S ) )
58 28 adantll 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ z e. S ) -> ( x ( .r ` R ) z ) = ( z ( .r ` R ) x ) )
59 58 fveq2d 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ z e. S ) -> ( ( invg ` R ) ` ( x ( .r ` R ) z ) ) = ( ( invg ` R ) ` ( z ( .r ` R ) x ) ) )
60 eqid 
 |-  ( invg ` R ) = ( invg ` R )
61 simplll 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ z e. S ) -> R e. Ring )
62 simplr 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ z e. S ) -> x e. ( Z ` S ) )
63 5 62 sseldi 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ z e. S ) -> x e. B )
64 simplr 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) -> S C_ B )
65 64 sselda 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ z e. S ) -> z e. B )
66 1 10 60 61 63 65 ringmneg1 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ z e. S ) -> ( ( ( invg ` R ) ` x ) ( .r ` R ) z ) = ( ( invg ` R ) ` ( x ( .r ` R ) z ) ) )
67 1 10 60 61 65 63 ringmneg2 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ z e. S ) -> ( z ( .r ` R ) ( ( invg ` R ) ` x ) ) = ( ( invg ` R ) ` ( z ( .r ` R ) x ) ) )
68 59 66 67 3eqtr4d 
 |-  ( ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ z e. S ) -> ( ( ( invg ` R ) ` x ) ( .r ` R ) z ) = ( z ( .r ` R ) ( ( invg ` R ) ` x ) ) )
69 68 ralrimiva 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) -> A. z e. S ( ( ( invg ` R ) ` x ) ( .r ` R ) z ) = ( z ( .r ` R ) ( ( invg ` R ) ` x ) ) )
70 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
71 70 ad2antrr 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) -> R e. Grp )
72 simpr 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) -> x e. ( Z ` S ) )
73 5 72 sseldi 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) -> x e. B )
74 1 60 grpinvcl 
 |-  ( ( R e. Grp /\ x e. B ) -> ( ( invg ` R ) ` x ) e. B )
75 71 73 74 syl2anc 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) -> ( ( invg ` R ) ` x ) e. B )
76 4 21 3 cntzel 
 |-  ( ( S C_ B /\ ( ( invg ` R ) ` x ) e. B ) -> ( ( ( invg ` R ) ` x ) e. ( Z ` S ) <-> A. z e. S ( ( ( invg ` R ) ` x ) ( .r ` R ) z ) = ( z ( .r ` R ) ( ( invg ` R ) ` x ) ) ) )
77 64 75 76 syl2anc 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) -> ( ( ( invg ` R ) ` x ) e. ( Z ` S ) <-> A. z e. S ( ( ( invg ` R ) ` x ) ( .r ` R ) z ) = ( z ( .r ` R ) ( ( invg ` R ) ` x ) ) ) )
78 69 77 mpbird 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) -> ( ( invg ` R ) ` x ) e. ( Z ` S ) )
79 57 78 jca 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ x e. ( Z ` S ) ) -> ( A. y e. ( Z ` S ) ( x ( +g ` R ) y ) e. ( Z ` S ) /\ ( ( invg ` R ) ` x ) e. ( Z ` S ) ) )
80 79 ralrimiva 
 |-  ( ( R e. Ring /\ S C_ B ) -> A. x e. ( Z ` S ) ( A. y e. ( Z ` S ) ( x ( +g ` R ) y ) e. ( Z ` S ) /\ ( ( invg ` R ) ` x ) e. ( Z ` S ) ) )
81 70 adantr 
 |-  ( ( R e. Ring /\ S C_ B ) -> R e. Grp )
82 1 39 60 issubg2 
 |-  ( R e. Grp -> ( ( Z ` S ) e. ( SubGrp ` R ) <-> ( ( Z ` S ) C_ B /\ ( Z ` S ) =/= (/) /\ A. x e. ( Z ` S ) ( A. y e. ( Z ` S ) ( x ( +g ` R ) y ) e. ( Z ` S ) /\ ( ( invg ` R ) ` x ) e. ( Z ` S ) ) ) ) )
83 81 82 syl 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( ( Z ` S ) e. ( SubGrp ` R ) <-> ( ( Z ` S ) C_ B /\ ( Z ` S ) =/= (/) /\ A. x e. ( Z ` S ) ( A. y e. ( Z ` S ) ( x ( +g ` R ) y ) e. ( Z ` S ) /\ ( ( invg ` R ) ` x ) e. ( Z ` S ) ) ) ) )
84 6 25 80 83 mpbir3and 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( Z ` S ) e. ( SubGrp ` R ) )
85 2 ringmgp 
 |-  ( R e. Ring -> M e. Mnd )
86 4 3 cntzsubm 
 |-  ( ( M e. Mnd /\ S C_ B ) -> ( Z ` S ) e. ( SubMnd ` M ) )
87 85 86 sylan 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( Z ` S ) e. ( SubMnd ` M ) )
88 2 issubrg3 
 |-  ( R e. Ring -> ( ( Z ` S ) e. ( SubRing ` R ) <-> ( ( Z ` S ) e. ( SubGrp ` R ) /\ ( Z ` S ) e. ( SubMnd ` M ) ) ) )
89 88 adantr 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( ( Z ` S ) e. ( SubRing ` R ) <-> ( ( Z ` S ) e. ( SubGrp ` R ) /\ ( Z ` S ) e. ( SubMnd ` M ) ) ) )
90 84 87 89 mpbir2and 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( Z ` S ) e. ( SubRing ` R ) )