| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nnnn0 12535 | . . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) | 
| 2 |  | cznrng.y | . . . . . . 7
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) | 
| 3 | 2 | zncrng 21564 | . . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑌 ∈
CRing) | 
| 4 | 1, 3 | syl 17 | . . . . 5
⊢ (𝑁 ∈ ℕ → 𝑌 ∈ CRing) | 
| 5 |  | crngring 20243 | . . . . . 6
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) | 
| 6 |  | cznrng.b | . . . . . . . 8
⊢ 𝐵 = (Base‘𝑌) | 
| 7 |  | cznrng.0 | . . . . . . . 8
⊢  0 =
(0g‘𝑌) | 
| 8 | 6, 7 | ring0cl 20265 | . . . . . . 7
⊢ (𝑌 ∈ Ring → 0 ∈ 𝐵) | 
| 9 |  | eleq1a 2835 | . . . . . . 7
⊢ ( 0 ∈ 𝐵 → (𝐶 = 0 → 𝐶 ∈ 𝐵)) | 
| 10 | 8, 9 | syl 17 | . . . . . 6
⊢ (𝑌 ∈ Ring → (𝐶 = 0 → 𝐶 ∈ 𝐵)) | 
| 11 | 5, 10 | syl 17 | . . . . 5
⊢ (𝑌 ∈ CRing → (𝐶 = 0 → 𝐶 ∈ 𝐵)) | 
| 12 | 4, 11 | syl 17 | . . . 4
⊢ (𝑁 ∈ ℕ → (𝐶 = 0 → 𝐶 ∈ 𝐵)) | 
| 13 | 12 | imp 406 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) → 𝐶 ∈ 𝐵) | 
| 14 |  | cznrng.x | . . . . . 6
⊢ 𝑋 = (𝑌 sSet 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉) | 
| 15 | 2, 6, 14 | cznabel 48181 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐶 ∈ 𝐵) → 𝑋 ∈ Abel) | 
| 16 | 15 | adantlr 715 | . . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) → 𝑋 ∈ Abel) | 
| 17 |  | eqid 2736 | . . . . . 6
⊢
(mulGrp‘𝑋) =
(mulGrp‘𝑋) | 
| 18 | 2, 6, 14 | cznrnglem 48180 | . . . . . 6
⊢ 𝐵 = (Base‘𝑋) | 
| 19 | 17, 18 | mgpbas 20143 | . . . . 5
⊢ 𝐵 =
(Base‘(mulGrp‘𝑋)) | 
| 20 | 14 | fveq2i 6908 | . . . . . . 7
⊢
(mulGrp‘𝑋) =
(mulGrp‘(𝑌 sSet
〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉)) | 
| 21 | 2 | fvexi 6919 | . . . . . . . 8
⊢ 𝑌 ∈ V | 
| 22 | 6 | fvexi 6919 | . . . . . . . . 9
⊢ 𝐵 ∈ V | 
| 23 | 22, 22 | mpoex 8105 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V | 
| 24 |  | mulridx 17339 | . . . . . . . . 9
⊢
.r = Slot (.r‘ndx) | 
| 25 | 24 | setsid 17245 | . . . . . . . 8
⊢ ((𝑌 ∈ V ∧ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) = (.r‘(𝑌 sSet 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉))) | 
| 26 | 21, 23, 25 | mp2an 692 | . . . . . . 7
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) = (.r‘(𝑌 sSet 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉)) | 
| 27 | 20, 26 | mgpplusg 20142 | . . . . . 6
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) = (+g‘(mulGrp‘𝑋)) | 
| 28 | 27 | eqcomi 2745 | . . . . 5
⊢
(+g‘(mulGrp‘𝑋)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) | 
| 29 |  | ne0i 4340 | . . . . . 6
⊢ (𝐶 ∈ 𝐵 → 𝐵 ≠ ∅) | 
| 30 | 29 | adantl 481 | . . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) → 𝐵 ≠ ∅) | 
| 31 |  | simpr 484 | . . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ 𝐵) | 
| 32 | 19, 28, 30, 31 | copissgrp 48089 | . . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) → (mulGrp‘𝑋) ∈ Smgrp) | 
| 33 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝐶 = 0 → (𝐶(+g‘𝑌)𝐶) = ( 0 (+g‘𝑌)𝐶)) | 
| 34 | 33 | ad3antlr 731 | . . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝐶(+g‘𝑌)𝐶) = ( 0 (+g‘𝑌)𝐶)) | 
| 35 | 4, 5 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑌 ∈ Ring) | 
| 36 |  | ringmnd 20241 | . . . . . . . . . . . . 13
⊢ (𝑌 ∈ Ring → 𝑌 ∈ Mnd) | 
| 37 | 35, 36 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑌 ∈ Mnd) | 
| 38 | 37 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) → 𝑌 ∈ Mnd) | 
| 39 | 38 | anim1i 615 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) → (𝑌 ∈ Mnd ∧ 𝐶 ∈ 𝐵)) | 
| 40 | 39 | adantr 480 | . . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑌 ∈ Mnd ∧ 𝐶 ∈ 𝐵)) | 
| 41 |  | eqid 2736 | . . . . . . . . . 10
⊢
(+g‘𝑌) = (+g‘𝑌) | 
| 42 | 6, 41, 7 | mndlid 18768 | . . . . . . . . 9
⊢ ((𝑌 ∈ Mnd ∧ 𝐶 ∈ 𝐵) → ( 0 (+g‘𝑌)𝐶) = 𝐶) | 
| 43 | 40, 42 | syl 17 | . . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ( 0 (+g‘𝑌)𝐶) = 𝐶) | 
| 44 | 34, 43 | eqtrd 2776 | . . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝐶(+g‘𝑌)𝐶) = 𝐶) | 
| 45 |  | eqidd 2737 | . . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)) | 
| 46 |  | eqidd 2737 | . . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → 𝐶 = 𝐶) | 
| 47 |  | simpr1 1194 | . . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → 𝑎 ∈ 𝐵) | 
| 48 |  | simpr2 1195 | . . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → 𝑏 ∈ 𝐵) | 
| 49 | 31 | adantr 480 | . . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → 𝐶 ∈ 𝐵) | 
| 50 | 45, 46, 47, 48, 49 | ovmpod 7586 | . . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑏) = 𝐶) | 
| 51 |  | eqidd 2737 | . . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑐)) → 𝐶 = 𝐶) | 
| 52 |  | simpr3 1196 | . . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → 𝑐 ∈ 𝐵) | 
| 53 | 45, 51, 47, 52, 49 | ovmpod 7586 | . . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝐶) | 
| 54 | 50, 53 | oveq12d 7450 | . . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑏)(+g‘𝑌)(𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)) = (𝐶(+g‘𝑌)𝐶)) | 
| 55 |  | eqidd 2737 | . . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑥 = 𝑎 ∧ 𝑦 = (𝑏(+g‘𝑌)𝑐))) → 𝐶 = 𝐶) | 
| 56 | 35 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → 𝑌 ∈ Ring) | 
| 57 | 6, 41 | ringacl 20276 | . . . . . . . . 9
⊢ ((𝑌 ∈ Ring ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) → (𝑏(+g‘𝑌)𝑐) ∈ 𝐵) | 
| 58 | 56, 48, 52, 57 | syl3anc 1372 | . . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑏(+g‘𝑌)𝑐) ∈ 𝐵) | 
| 59 | 45, 55, 47, 58, 49 | ovmpod 7586 | . . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)(𝑏(+g‘𝑌)𝑐)) = 𝐶) | 
| 60 | 44, 54, 59 | 3eqtr4rd 2787 | . . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)(𝑏(+g‘𝑌)𝑐)) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑏)(+g‘𝑌)(𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐))) | 
| 61 |  | eqidd 2737 | . . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑥 = 𝑏 ∧ 𝑦 = 𝑐)) → 𝐶 = 𝐶) | 
| 62 | 45, 61, 48, 52, 49 | ovmpod 7586 | . . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑏(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝐶) | 
| 63 | 53, 62 | oveq12d 7450 | . . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)(+g‘𝑌)(𝑏(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)) = (𝐶(+g‘𝑌)𝐶)) | 
| 64 |  | eqidd 2737 | . . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑥 = (𝑎(+g‘𝑌)𝑏) ∧ 𝑦 = 𝑐)) → 𝐶 = 𝐶) | 
| 65 | 6, 41 | ringacl 20276 | . . . . . . . . 9
⊢ ((𝑌 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(+g‘𝑌)𝑏) ∈ 𝐵) | 
| 66 | 56, 47, 48, 65 | syl3anc 1372 | . . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑎(+g‘𝑌)𝑏) ∈ 𝐵) | 
| 67 | 45, 64, 66, 52, 49 | ovmpod 7586 | . . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ((𝑎(+g‘𝑌)𝑏)(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝐶) | 
| 68 | 44, 63, 67 | 3eqtr4rd 2787 | . . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ((𝑎(+g‘𝑌)𝑏)(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)(+g‘𝑌)(𝑏(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐))) | 
| 69 | 60, 68 | jca 511 | . . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)(𝑏(+g‘𝑌)𝑐)) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑏)(+g‘𝑌)(𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)) ∧ ((𝑎(+g‘𝑌)𝑏)(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)(+g‘𝑌)(𝑏(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)))) | 
| 70 | 69 | ralrimivvva 3204 | . . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)(𝑏(+g‘𝑌)𝑐)) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑏)(+g‘𝑌)(𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)) ∧ ((𝑎(+g‘𝑌)𝑏)(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)(+g‘𝑌)(𝑏(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)))) | 
| 71 | 16, 32, 70 | 3jca 1128 | . . 3
⊢ (((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) → (𝑋 ∈ Abel ∧ (mulGrp‘𝑋) ∈ Smgrp ∧
∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)(𝑏(+g‘𝑌)𝑐)) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑏)(+g‘𝑌)(𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)) ∧ ((𝑎(+g‘𝑌)𝑏)(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)(+g‘𝑌)(𝑏(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐))))) | 
| 72 | 13, 71 | mpdan 687 | . 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) → (𝑋 ∈ Abel ∧
(mulGrp‘𝑋) ∈
Smgrp ∧ ∀𝑎
∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)(𝑏(+g‘𝑌)𝑐)) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑏)(+g‘𝑌)(𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)) ∧ ((𝑎(+g‘𝑌)𝑏)(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)(+g‘𝑌)(𝑏(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐))))) | 
| 73 |  | plusgid 17325 | . . . . 5
⊢
+g = Slot (+g‘ndx) | 
| 74 |  | plusgndxnmulrndx 17342 | . . . . 5
⊢
(+g‘ndx) ≠
(.r‘ndx) | 
| 75 | 73, 74 | setsnid 17246 | . . . 4
⊢
(+g‘𝑌) = (+g‘(𝑌 sSet 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉)) | 
| 76 | 14 | fveq2i 6908 | . . . 4
⊢
(+g‘𝑋) = (+g‘(𝑌 sSet 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉)) | 
| 77 | 75, 76 | eqtr4i 2767 | . . 3
⊢
(+g‘𝑌) = (+g‘𝑋) | 
| 78 | 14 | eqcomi 2745 | . . . . 5
⊢ (𝑌 sSet
〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉) = 𝑋 | 
| 79 | 78 | fveq2i 6908 | . . . 4
⊢
(.r‘(𝑌 sSet 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉)) = (.r‘𝑋) | 
| 80 | 26, 79 | eqtri 2764 | . . 3
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) = (.r‘𝑋) | 
| 81 | 18, 17, 77, 80 | isrng 20152 | . 2
⊢ (𝑋 ∈ Rng ↔ (𝑋 ∈ Abel ∧
(mulGrp‘𝑋) ∈
Smgrp ∧ ∀𝑎
∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)(𝑏(+g‘𝑌)𝑐)) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑏)(+g‘𝑌)(𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)) ∧ ((𝑎(+g‘𝑌)𝑏)(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)(+g‘𝑌)(𝑏(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐))))) | 
| 82 | 72, 81 | sylibr 234 | 1
⊢ ((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) → 𝑋 ∈ Rng) |