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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
cntzsdrg.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
cntzsdrg.z ⊢ 𝑍 = ( Cntz ‘ 𝑀 )
Assertion cntzsdrg ( ( 𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑍 ‘ 𝑆 ) ∈ ( SubDRing ‘ 𝑅 ) )

Proof

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