Metamath Proof Explorer

Theorem cntzsubrng

Description: Centralizers in a non-unital ring are subrings. (Contributed by AV, 17-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 cntzsubrng.b 
 |-  B = ( Base ` R )
2 cntzsubrng.m 
 |-  M = ( mulGrp ` R )
3 cntzsubrng.z 
 |-  Z = ( Cntz ` M )
4 2 1 mgpbas 
 |-  B = ( Base ` M )
5 4 3 cntzssv 
 |-  ( Z ` S ) C_ B
6 5 a1i 
 |-  ( ( R e. Rng /\ S C_ B ) -> ( Z ` S ) C_ B )
7 simpll 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ z e. S ) -> R e. Rng )
8 ssel2 
 |-  ( ( S C_ B /\ z e. S ) -> z e. B )
9 8 adantll 
 |-  ( ( ( R e. Rng /\ 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 rnglz 
 |-  ( ( R e. Rng /\ z e. B ) -> ( ( 0g ` R ) ( .r ` R ) z ) = ( 0g ` R ) )
13 7 9 12 syl2anc 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ z e. S ) -> ( ( 0g ` R ) ( .r ` R ) z ) = ( 0g ` R ) )
14 1 10 11 rngrz 
 |-  ( ( R e. Rng /\ z e. B ) -> ( z ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
15 7 9 14 syl2anc 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ z e. S ) -> ( z ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
16 13 15 eqtr4d 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ z e. S ) -> ( ( 0g ` R ) ( .r ` R ) z ) = ( z ( .r ` R ) ( 0g ` R ) ) )
17 16 ralrimiva 
 |-  ( ( R e. Rng /\ S C_ B ) -> A. z e. S ( ( 0g ` R ) ( .r ` R ) z ) = ( z ( .r ` R ) ( 0g ` R ) ) )
18 simpr 
 |-  ( ( R e. Rng /\ S C_ B ) -> S C_ B )
19 1 11 rng0cl 
 |-  ( R e. Rng -> ( 0g ` R ) e. B )
20 19 adantr 
 |-  ( ( R e. Rng /\ 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. Rng /\ 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. Rng /\ S C_ B ) -> ( 0g ` R ) e. ( Z ` S ) )
25 24 ne0d 
 |-  ( ( R e. Rng /\ S C_ B ) -> ( Z ` S ) =/= (/) )
26 simpl2 
 |-  ( ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> x e. ( Z ` S ) )
27 21 3 cntzi 
 |-  ( ( x e. ( Z ` S ) /\ z e. S ) -> ( x ( .r ` R ) z ) = ( z ( .r ` R ) x ) )
28 26 27 sylancom 
 |-  ( ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> ( x ( .r ` R ) z ) = ( z ( .r ` R ) x ) )
29 simpl3 
 |-  ( ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> y e. ( Z ` S ) )
30 21 3 cntzi 
 |-  ( ( y e. ( Z ` S ) /\ z e. S ) -> ( y ( .r ` R ) z ) = ( z ( .r ` R ) y ) )
31 29 30 sylancom 
 |-  ( ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> ( y ( .r ` R ) z ) = ( z ( .r ` R ) y ) )
32 28 31 oveq12d 
 |-  ( ( ( ( R e. Rng /\ 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 ) ) )
33 simpl1l 
 |-  ( ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> R e. Rng )
34 5 26 sselid 
 |-  ( ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> x e. B )
35 5 29 sselid 
 |-  ( ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> y e. B )
36 simp1r 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) -> S C_ B )
37 36 sselda 
 |-  ( ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) /\ z e. S ) -> z e. B )
38 eqid 
 |-  ( +g ` R ) = ( +g ` R )
39 1 38 10 rngdir 
 |-  ( ( R e. Rng /\ ( 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 ) ) )
40 33 34 35 37 39 syl13anc 
 |-  ( ( ( ( R e. Rng /\ 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 ) ) )
41 1 38 10 rngdi 
 |-  ( ( R e. Rng /\ ( 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 ) ) )
42 33 37 34 35 41 syl13anc 
 |-  ( ( ( ( R e. Rng /\ 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 ) ) )
43 32 40 42 3eqtr4d 
 |-  ( ( ( ( R e. Rng /\ 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 ) ) )
44 43 ralrimiva 
 |-  ( ( ( R e. Rng /\ 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 ) ) )
45 simp1l 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) -> R e. Rng )
46 simp2 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) -> x e. ( Z ` S ) )
47 5 46 sselid 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) -> x e. B )
48 simp3 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) -> y e. ( Z ` S ) )
49 5 48 sselid 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) -> y e. B )
50 1 38 rngacl 
 |-  ( ( R e. Rng /\ x e. B /\ y e. B ) -> ( x ( +g ` R ) y ) e. B )
51 45 47 49 50 syl3anc 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) -> ( x ( +g ` R ) y ) e. B )
52 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 ) ) ) )
53 36 51 52 syl2anc 
 |-  ( ( ( R e. Rng /\ 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 ) ) ) )
54 44 53 mpbird 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) /\ y e. ( Z ` S ) ) -> ( x ( +g ` R ) y ) e. ( Z ` S ) )
55 54 3expa 
 |-  ( ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ y e. ( Z ` S ) ) -> ( x ( +g ` R ) y ) e. ( Z ` S ) )
56 55 ralrimiva 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) ) -> A. y e. ( Z ` S ) ( x ( +g ` R ) y ) e. ( Z ` S ) )
57 27 adantll 
 |-  ( ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ z e. S ) -> ( x ( .r ` R ) z ) = ( z ( .r ` R ) x ) )
58 57 fveq2d 
 |-  ( ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ z e. S ) -> ( ( invg ` R ) ` ( x ( .r ` R ) z ) ) = ( ( invg ` R ) ` ( z ( .r ` R ) x ) ) )
59 eqid 
 |-  ( invg ` R ) = ( invg ` R )
60 simplll 
 |-  ( ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ z e. S ) -> R e. Rng )
61 simplr 
 |-  ( ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ z e. S ) -> x e. ( Z ` S ) )
62 5 61 sselid 
 |-  ( ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ z e. S ) -> x e. B )
63 simplr 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) ) -> S C_ B )
64 63 sselda 
 |-  ( ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ z e. S ) -> z e. B )
65 1 10 59 60 62 64 rngmneg1 
 |-  ( ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ z e. S ) -> ( ( ( invg ` R ) ` x ) ( .r ` R ) z ) = ( ( invg ` R ) ` ( x ( .r ` R ) z ) ) )
66 1 10 59 60 64 62 rngmneg2 
 |-  ( ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ z e. S ) -> ( z ( .r ` R ) ( ( invg ` R ) ` x ) ) = ( ( invg ` R ) ` ( z ( .r ` R ) x ) ) )
67 58 65 66 3eqtr4d 
 |-  ( ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ z e. S ) -> ( ( ( invg ` R ) ` x ) ( .r ` R ) z ) = ( z ( .r ` R ) ( ( invg ` R ) ` x ) ) )
68 67 ralrimiva 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) ) -> A. z e. S ( ( ( invg ` R ) ` x ) ( .r ` R ) z ) = ( z ( .r ` R ) ( ( invg ` R ) ` x ) ) )
69 rnggrp 
 |-  ( R e. Rng -> R e. Grp )
70 69 ad2antrr 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) ) -> R e. Grp )
71 simpr 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) ) -> x e. ( Z ` S ) )
72 5 71 sselid 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) ) -> x e. B )
73 1 59 70 72 grpinvcld 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) ) -> ( ( invg ` R ) ` x ) e. B )
74 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 ) ) ) )
75 63 73 74 syl2anc 
 |-  ( ( ( R e. Rng /\ 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 ) ) ) )
76 68 75 mpbird 
 |-  ( ( ( R e. Rng /\ S C_ B ) /\ x e. ( Z ` S ) ) -> ( ( invg ` R ) ` x ) e. ( Z ` S ) )
77 56 76 jca 
 |-  ( ( ( R e. Rng /\ 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 ) ) )
78 77 ralrimiva 
 |-  ( ( R e. Rng /\ 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 ) ) )
79 69 adantr 
 |-  ( ( R e. Rng /\ S C_ B ) -> R e. Grp )
80 1 38 59 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 ) ) ) ) )
81 79 80 syl 
 |-  ( ( R e. Rng /\ 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 ) ) ) ) )
82 6 25 78 81 mpbir3and 
 |-  ( ( R e. Rng /\ S C_ B ) -> ( Z ` S ) e. ( SubGrp ` R ) )
83 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
84 83 rngmgp 
 |-  ( R e. Rng -> ( mulGrp ` R ) e. Smgrp )
85 83 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
86 85 sseq2i 
 |-  ( S C_ B <-> S C_ ( Base ` ( mulGrp ` R ) ) )
87 86 biimpi 
 |-  ( S C_ B -> S C_ ( Base ` ( mulGrp ` R ) ) )
88 eqid 
 |-  ( Base ` ( mulGrp ` R ) ) = ( Base ` ( mulGrp ` R ) )
89 2 fveq2i 
 |-  ( Cntz ` M ) = ( Cntz ` ( mulGrp ` R ) )
90 3 89 eqtri 
 |-  Z = ( Cntz ` ( mulGrp ` R ) )
91 eqid 
 |-  ( Z ` S ) = ( Z ` S )
92 88 90 91 cntzsgrpcl 
 |-  ( ( ( mulGrp ` R ) e. Smgrp /\ S C_ ( Base ` ( mulGrp ` R ) ) ) -> A. x e. ( Z ` S ) A. y e. ( Z ` S ) ( x ( +g ` ( mulGrp ` R ) ) y ) e. ( Z ` S ) )
93 84 87 92 syl2an 
 |-  ( ( R e. Rng /\ S C_ B ) -> A. x e. ( Z ` S ) A. y e. ( Z ` S ) ( x ( +g ` ( mulGrp ` R ) ) y ) e. ( Z ` S ) )
94 83 10 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
95 94 oveqi 
 |-  ( x ( .r ` R ) y ) = ( x ( +g ` ( mulGrp ` R ) ) y )
96 95 eleq1i 
 |-  ( ( x ( .r ` R ) y ) e. ( Z ` S ) <-> ( x ( +g ` ( mulGrp ` R ) ) y ) e. ( Z ` S ) )
97 96 2ralbii 
 |-  ( A. x e. ( Z ` S ) A. y e. ( Z ` S ) ( x ( .r ` R ) y ) e. ( Z ` S ) <-> A. x e. ( Z ` S ) A. y e. ( Z ` S ) ( x ( +g ` ( mulGrp ` R ) ) y ) e. ( Z ` S ) )
98 93 97 sylibr 
 |-  ( ( R e. Rng /\ S C_ B ) -> A. x e. ( Z ` S ) A. y e. ( Z ` S ) ( x ( .r ` R ) y ) e. ( Z ` S ) )
99 1 10 issubrng2 
 |-  ( R e. Rng -> ( ( Z ` S ) e. ( SubRng ` R ) <-> ( ( Z ` S ) e. ( SubGrp ` R ) /\ A. x e. ( Z ` S ) A. y e. ( Z ` S ) ( x ( .r ` R ) y ) e. ( Z ` S ) ) ) )
100 99 adantr 
 |-  ( ( R e. Rng /\ S C_ B ) -> ( ( Z ` S ) e. ( SubRng ` R ) <-> ( ( Z ` S ) e. ( SubGrp ` R ) /\ A. x e. ( Z ` S ) A. y e. ( Z ` S ) ( x ( .r ` R ) y ) e. ( Z ` S ) ) ) )
101 82 98 100 mpbir2and 
 |-  ( ( R e. Rng /\ S C_ B ) -> ( Z ` S ) e. ( SubRng ` R ) )