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

Proof

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