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}={\mathrm{Base}}_{{R}}$
cntzsubr.m ${⊢}{M}={\mathrm{mulGrp}}_{{R}}$
cntzsubr.z ${⊢}{Z}=\mathrm{Cntz}\left({M}\right)$
Assertion cntzsubr ${⊢}\left({R}\in \mathrm{Ring}\wedge {S}\subseteq {B}\right)\to {Z}\left({S}\right)\in \mathrm{SubRing}\left({R}\right)$

Proof

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