This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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