| Step | Hyp | Ref
| Expression |
| 1 | | cntzsubrng.m |
. . . . . 6
⊢ 𝑀 = (mulGrp‘𝑅) |
| 2 | | cntzsubrng.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
| 3 | 1, 2 | mgpbas 20142 |
. . . . 5
⊢ 𝐵 = (Base‘𝑀) |
| 4 | | cntzsubrng.z |
. . . . 5
⊢ 𝑍 = (Cntz‘𝑀) |
| 5 | 3, 4 | cntzssv 19346 |
. . . 4
⊢ (𝑍‘𝑆) ⊆ 𝐵 |
| 6 | 5 | a1i 11 |
. . 3
⊢ ((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ⊆ 𝐵) |
| 7 | | simpll 767 |
. . . . . . . 8
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑧 ∈ 𝑆) → 𝑅 ∈ Rng) |
| 8 | | ssel2 3978 |
. . . . . . . . 9
⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝐵) |
| 9 | 8 | adantll 714 |
. . . . . . . 8
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝐵) |
| 10 | | eqid 2737 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 11 | | eqid 2737 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 12 | 2, 10, 11 | rnglz 20162 |
. . . . . . . 8
⊢ ((𝑅 ∈ Rng ∧ 𝑧 ∈ 𝐵) → ((0g‘𝑅)(.r‘𝑅)𝑧) = (0g‘𝑅)) |
| 13 | 7, 9, 12 | syl2anc 584 |
. . . . . . 7
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑧 ∈ 𝑆) → ((0g‘𝑅)(.r‘𝑅)𝑧) = (0g‘𝑅)) |
| 14 | 2, 10, 11 | rngrz 20163 |
. . . . . . . 8
⊢ ((𝑅 ∈ Rng ∧ 𝑧 ∈ 𝐵) → (𝑧(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
| 15 | 7, 9, 14 | syl2anc 584 |
. . . . . . 7
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑧 ∈ 𝑆) → (𝑧(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
| 16 | 13, 15 | eqtr4d 2780 |
. . . . . 6
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑧 ∈ 𝑆) → ((0g‘𝑅)(.r‘𝑅)𝑧) = (𝑧(.r‘𝑅)(0g‘𝑅))) |
| 17 | 16 | ralrimiva 3146 |
. . . . 5
⊢ ((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) → ∀𝑧 ∈ 𝑆 ((0g‘𝑅)(.r‘𝑅)𝑧) = (𝑧(.r‘𝑅)(0g‘𝑅))) |
| 18 | | simpr 484 |
. . . . . 6
⊢ ((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) → 𝑆 ⊆ 𝐵) |
| 19 | 2, 11 | rng0cl 20160 |
. . . . . . 7
⊢ (𝑅 ∈ Rng →
(0g‘𝑅)
∈ 𝐵) |
| 20 | 19 | adantr 480 |
. . . . . 6
⊢ ((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) → (0g‘𝑅) ∈ 𝐵) |
| 21 | 1, 10 | mgpplusg 20141 |
. . . . . . 7
⊢
(.r‘𝑅) = (+g‘𝑀) |
| 22 | 3, 21, 4 | cntzel 19341 |
. . . . . 6
⊢ ((𝑆 ⊆ 𝐵 ∧ (0g‘𝑅) ∈ 𝐵) → ((0g‘𝑅) ∈ (𝑍‘𝑆) ↔ ∀𝑧 ∈ 𝑆 ((0g‘𝑅)(.r‘𝑅)𝑧) = (𝑧(.r‘𝑅)(0g‘𝑅)))) |
| 23 | 18, 20, 22 | syl2anc 584 |
. . . . 5
⊢ ((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) → ((0g‘𝑅) ∈ (𝑍‘𝑆) ↔ ∀𝑧 ∈ 𝑆 ((0g‘𝑅)(.r‘𝑅)𝑧) = (𝑧(.r‘𝑅)(0g‘𝑅)))) |
| 24 | 17, 23 | mpbird 257 |
. . . 4
⊢ ((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) → (0g‘𝑅) ∈ (𝑍‘𝑆)) |
| 25 | 24 | ne0d 4342 |
. . 3
⊢ ((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ≠ ∅) |
| 26 | | simpl2 1193 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → 𝑥 ∈ (𝑍‘𝑆)) |
| 27 | 21, 4 | cntzi 19347 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝑍‘𝑆) ∧ 𝑧 ∈ 𝑆) → (𝑥(.r‘𝑅)𝑧) = (𝑧(.r‘𝑅)𝑥)) |
| 28 | 26, 27 | sylancom 588 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → (𝑥(.r‘𝑅)𝑧) = (𝑧(.r‘𝑅)𝑥)) |
| 29 | | simpl3 1194 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → 𝑦 ∈ (𝑍‘𝑆)) |
| 30 | 21, 4 | cntzi 19347 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ (𝑍‘𝑆) ∧ 𝑧 ∈ 𝑆) → (𝑦(.r‘𝑅)𝑧) = (𝑧(.r‘𝑅)𝑦)) |
| 31 | 29, 30 | sylancom 588 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → (𝑦(.r‘𝑅)𝑧) = (𝑧(.r‘𝑅)𝑦)) |
| 32 | 28, 31 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)) = ((𝑧(.r‘𝑅)𝑥)(+g‘𝑅)(𝑧(.r‘𝑅)𝑦))) |
| 33 | | simpl1l 1225 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → 𝑅 ∈ Rng) |
| 34 | 5, 26 | sselid 3981 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → 𝑥 ∈ 𝐵) |
| 35 | 5, 29 | sselid 3981 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → 𝑦 ∈ 𝐵) |
| 36 | | simp1r 1199 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) → 𝑆 ⊆ 𝐵) |
| 37 | 36 | sselda 3983 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝐵) |
| 38 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 39 | 2, 38, 10 | rngdir 20158 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Rng ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧))) |
| 40 | 33, 34, 35, 37, 39 | syl13anc 1374 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧))) |
| 41 | 2, 38, 10 | rngdi 20157 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Rng ∧ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑧(.r‘𝑅)(𝑥(+g‘𝑅)𝑦)) = ((𝑧(.r‘𝑅)𝑥)(+g‘𝑅)(𝑧(.r‘𝑅)𝑦))) |
| 42 | 33, 37, 34, 35, 41 | syl13anc 1374 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → (𝑧(.r‘𝑅)(𝑥(+g‘𝑅)𝑦)) = ((𝑧(.r‘𝑅)𝑥)(+g‘𝑅)(𝑧(.r‘𝑅)𝑦))) |
| 43 | 32, 40, 42 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑧(.r‘𝑅)(𝑥(+g‘𝑅)𝑦))) |
| 44 | 43 | ralrimiva 3146 |
. . . . . . . 8
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) → ∀𝑧 ∈ 𝑆 ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑧(.r‘𝑅)(𝑥(+g‘𝑅)𝑦))) |
| 45 | | simp1l 1198 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) → 𝑅 ∈ Rng) |
| 46 | | simp2 1138 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) → 𝑥 ∈ (𝑍‘𝑆)) |
| 47 | 5, 46 | sselid 3981 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) → 𝑥 ∈ 𝐵) |
| 48 | | simp3 1139 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) → 𝑦 ∈ (𝑍‘𝑆)) |
| 49 | 5, 48 | sselid 3981 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) → 𝑦 ∈ 𝐵) |
| 50 | 2, 38 | rngacl 20159 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Rng ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+g‘𝑅)𝑦) ∈ 𝐵) |
| 51 | 45, 47, 49, 50 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) → (𝑥(+g‘𝑅)𝑦) ∈ 𝐵) |
| 52 | 3, 21, 4 | cntzel 19341 |
. . . . . . . . 9
⊢ ((𝑆 ⊆ 𝐵 ∧ (𝑥(+g‘𝑅)𝑦) ∈ 𝐵) → ((𝑥(+g‘𝑅)𝑦) ∈ (𝑍‘𝑆) ↔ ∀𝑧 ∈ 𝑆 ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑧(.r‘𝑅)(𝑥(+g‘𝑅)𝑦)))) |
| 53 | 36, 51, 52 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) → ((𝑥(+g‘𝑅)𝑦) ∈ (𝑍‘𝑆) ↔ ∀𝑧 ∈ 𝑆 ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑧(.r‘𝑅)(𝑥(+g‘𝑅)𝑦)))) |
| 54 | 44, 53 | mpbird 257 |
. . . . . . 7
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆) ∧ 𝑦 ∈ (𝑍‘𝑆)) → (𝑥(+g‘𝑅)𝑦) ∈ (𝑍‘𝑆)) |
| 55 | 54 | 3expa 1119 |
. . . . . 6
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) ∧ 𝑦 ∈ (𝑍‘𝑆)) → (𝑥(+g‘𝑅)𝑦) ∈ (𝑍‘𝑆)) |
| 56 | 55 | ralrimiva 3146 |
. . . . 5
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) → ∀𝑦 ∈ (𝑍‘𝑆)(𝑥(+g‘𝑅)𝑦) ∈ (𝑍‘𝑆)) |
| 57 | 27 | adantll 714 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → (𝑥(.r‘𝑅)𝑧) = (𝑧(.r‘𝑅)𝑥)) |
| 58 | 57 | fveq2d 6910 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → ((invg‘𝑅)‘(𝑥(.r‘𝑅)𝑧)) = ((invg‘𝑅)‘(𝑧(.r‘𝑅)𝑥))) |
| 59 | | eqid 2737 |
. . . . . . . . 9
⊢
(invg‘𝑅) = (invg‘𝑅) |
| 60 | | simplll 775 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → 𝑅 ∈ Rng) |
| 61 | | simplr 769 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → 𝑥 ∈ (𝑍‘𝑆)) |
| 62 | 5, 61 | sselid 3981 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → 𝑥 ∈ 𝐵) |
| 63 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) → 𝑆 ⊆ 𝐵) |
| 64 | 63 | sselda 3983 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝐵) |
| 65 | 2, 10, 59, 60, 62, 64 | rngmneg1 20164 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → (((invg‘𝑅)‘𝑥)(.r‘𝑅)𝑧) = ((invg‘𝑅)‘(𝑥(.r‘𝑅)𝑧))) |
| 66 | 2, 10, 59, 60, 64, 62 | rngmneg2 20165 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → (𝑧(.r‘𝑅)((invg‘𝑅)‘𝑥)) = ((invg‘𝑅)‘(𝑧(.r‘𝑅)𝑥))) |
| 67 | 58, 65, 66 | 3eqtr4d 2787 |
. . . . . . 7
⊢ ((((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) ∧ 𝑧 ∈ 𝑆) → (((invg‘𝑅)‘𝑥)(.r‘𝑅)𝑧) = (𝑧(.r‘𝑅)((invg‘𝑅)‘𝑥))) |
| 68 | 67 | ralrimiva 3146 |
. . . . . 6
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) → ∀𝑧 ∈ 𝑆 (((invg‘𝑅)‘𝑥)(.r‘𝑅)𝑧) = (𝑧(.r‘𝑅)((invg‘𝑅)‘𝑥))) |
| 69 | | rnggrp 20155 |
. . . . . . . . 9
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Grp) |
| 70 | 69 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) → 𝑅 ∈ Grp) |
| 71 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) → 𝑥 ∈ (𝑍‘𝑆)) |
| 72 | 5, 71 | sselid 3981 |
. . . . . . . 8
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) → 𝑥 ∈ 𝐵) |
| 73 | 2, 59, 70, 72 | grpinvcld 19006 |
. . . . . . 7
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) → ((invg‘𝑅)‘𝑥) ∈ 𝐵) |
| 74 | 3, 21, 4 | cntzel 19341 |
. . . . . . 7
⊢ ((𝑆 ⊆ 𝐵 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝐵) → (((invg‘𝑅)‘𝑥) ∈ (𝑍‘𝑆) ↔ ∀𝑧 ∈ 𝑆 (((invg‘𝑅)‘𝑥)(.r‘𝑅)𝑧) = (𝑧(.r‘𝑅)((invg‘𝑅)‘𝑥)))) |
| 75 | 63, 73, 74 | syl2anc 584 |
. . . . . 6
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) → (((invg‘𝑅)‘𝑥) ∈ (𝑍‘𝑆) ↔ ∀𝑧 ∈ 𝑆 (((invg‘𝑅)‘𝑥)(.r‘𝑅)𝑧) = (𝑧(.r‘𝑅)((invg‘𝑅)‘𝑥)))) |
| 76 | 68, 75 | mpbird 257 |
. . . . 5
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) → ((invg‘𝑅)‘𝑥) ∈ (𝑍‘𝑆)) |
| 77 | 56, 76 | jca 511 |
. . . 4
⊢ (((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑍‘𝑆)) → (∀𝑦 ∈ (𝑍‘𝑆)(𝑥(+g‘𝑅)𝑦) ∈ (𝑍‘𝑆) ∧ ((invg‘𝑅)‘𝑥) ∈ (𝑍‘𝑆))) |
| 78 | 77 | ralrimiva 3146 |
. . 3
⊢ ((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) → ∀𝑥 ∈ (𝑍‘𝑆)(∀𝑦 ∈ (𝑍‘𝑆)(𝑥(+g‘𝑅)𝑦) ∈ (𝑍‘𝑆) ∧ ((invg‘𝑅)‘𝑥) ∈ (𝑍‘𝑆))) |
| 79 | 69 | adantr 480 |
. . . 4
⊢ ((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) → 𝑅 ∈ Grp) |
| 80 | 2, 38, 59 | issubg2 19159 |
. . . 4
⊢ (𝑅 ∈ Grp → ((𝑍‘𝑆) ∈ (SubGrp‘𝑅) ↔ ((𝑍‘𝑆) ⊆ 𝐵 ∧ (𝑍‘𝑆) ≠ ∅ ∧ ∀𝑥 ∈ (𝑍‘𝑆)(∀𝑦 ∈ (𝑍‘𝑆)(𝑥(+g‘𝑅)𝑦) ∈ (𝑍‘𝑆) ∧ ((invg‘𝑅)‘𝑥) ∈ (𝑍‘𝑆))))) |
| 81 | 79, 80 | syl 17 |
. . 3
⊢ ((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) → ((𝑍‘𝑆) ∈ (SubGrp‘𝑅) ↔ ((𝑍‘𝑆) ⊆ 𝐵 ∧ (𝑍‘𝑆) ≠ ∅ ∧ ∀𝑥 ∈ (𝑍‘𝑆)(∀𝑦 ∈ (𝑍‘𝑆)(𝑥(+g‘𝑅)𝑦) ∈ (𝑍‘𝑆) ∧ ((invg‘𝑅)‘𝑥) ∈ (𝑍‘𝑆))))) |
| 82 | 6, 25, 78, 81 | mpbir3and 1343 |
. 2
⊢ ((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubGrp‘𝑅)) |
| 83 | | eqid 2737 |
. . . . 5
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
| 84 | 83 | rngmgp 20153 |
. . . 4
⊢ (𝑅 ∈ Rng →
(mulGrp‘𝑅) ∈
Smgrp) |
| 85 | 83, 2 | mgpbas 20142 |
. . . . . 6
⊢ 𝐵 =
(Base‘(mulGrp‘𝑅)) |
| 86 | 85 | sseq2i 4013 |
. . . . 5
⊢ (𝑆 ⊆ 𝐵 ↔ 𝑆 ⊆ (Base‘(mulGrp‘𝑅))) |
| 87 | 86 | biimpi 216 |
. . . 4
⊢ (𝑆 ⊆ 𝐵 → 𝑆 ⊆ (Base‘(mulGrp‘𝑅))) |
| 88 | | eqid 2737 |
. . . . 5
⊢
(Base‘(mulGrp‘𝑅)) = (Base‘(mulGrp‘𝑅)) |
| 89 | 1 | fveq2i 6909 |
. . . . . 6
⊢
(Cntz‘𝑀) =
(Cntz‘(mulGrp‘𝑅)) |
| 90 | 4, 89 | eqtri 2765 |
. . . . 5
⊢ 𝑍 =
(Cntz‘(mulGrp‘𝑅)) |
| 91 | | eqid 2737 |
. . . . 5
⊢ (𝑍‘𝑆) = (𝑍‘𝑆) |
| 92 | 88, 90, 91 | cntzsgrpcl 19352 |
. . . 4
⊢
(((mulGrp‘𝑅)
∈ Smgrp ∧ 𝑆
⊆ (Base‘(mulGrp‘𝑅))) → ∀𝑥 ∈ (𝑍‘𝑆)∀𝑦 ∈ (𝑍‘𝑆)(𝑥(+g‘(mulGrp‘𝑅))𝑦) ∈ (𝑍‘𝑆)) |
| 93 | 84, 87, 92 | syl2an 596 |
. . 3
⊢ ((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) → ∀𝑥 ∈ (𝑍‘𝑆)∀𝑦 ∈ (𝑍‘𝑆)(𝑥(+g‘(mulGrp‘𝑅))𝑦) ∈ (𝑍‘𝑆)) |
| 94 | 83, 10 | mgpplusg 20141 |
. . . . . 6
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
| 95 | 94 | oveqi 7444 |
. . . . 5
⊢ (𝑥(.r‘𝑅)𝑦) = (𝑥(+g‘(mulGrp‘𝑅))𝑦) |
| 96 | 95 | eleq1i 2832 |
. . . 4
⊢ ((𝑥(.r‘𝑅)𝑦) ∈ (𝑍‘𝑆) ↔ (𝑥(+g‘(mulGrp‘𝑅))𝑦) ∈ (𝑍‘𝑆)) |
| 97 | 96 | 2ralbii 3128 |
. . 3
⊢
(∀𝑥 ∈
(𝑍‘𝑆)∀𝑦 ∈ (𝑍‘𝑆)(𝑥(.r‘𝑅)𝑦) ∈ (𝑍‘𝑆) ↔ ∀𝑥 ∈ (𝑍‘𝑆)∀𝑦 ∈ (𝑍‘𝑆)(𝑥(+g‘(mulGrp‘𝑅))𝑦) ∈ (𝑍‘𝑆)) |
| 98 | 93, 97 | sylibr 234 |
. 2
⊢ ((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) → ∀𝑥 ∈ (𝑍‘𝑆)∀𝑦 ∈ (𝑍‘𝑆)(𝑥(.r‘𝑅)𝑦) ∈ (𝑍‘𝑆)) |
| 99 | 2, 10 | issubrng2 20558 |
. . 3
⊢ (𝑅 ∈ Rng → ((𝑍‘𝑆) ∈ (SubRng‘𝑅) ↔ ((𝑍‘𝑆) ∈ (SubGrp‘𝑅) ∧ ∀𝑥 ∈ (𝑍‘𝑆)∀𝑦 ∈ (𝑍‘𝑆)(𝑥(.r‘𝑅)𝑦) ∈ (𝑍‘𝑆)))) |
| 100 | 99 | adantr 480 |
. 2
⊢ ((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) → ((𝑍‘𝑆) ∈ (SubRng‘𝑅) ↔ ((𝑍‘𝑆) ∈ (SubGrp‘𝑅) ∧ ∀𝑥 ∈ (𝑍‘𝑆)∀𝑦 ∈ (𝑍‘𝑆)(𝑥(.r‘𝑅)𝑦) ∈ (𝑍‘𝑆)))) |
| 101 | 82, 98, 100 | mpbir2and 713 |
1
⊢ ((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubRng‘𝑅)) |