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

### Proof

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