Step | Hyp | Ref
| Expression |
1 | | nnnn0 11176 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
2 | | cznrng.y |
. . . . . . 7
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) |
3 | 2 | zncrng 19712 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑌 ∈
CRing) |
4 | 1, 3 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 𝑌 ∈ CRing) |
5 | | crngring 18381 |
. . . . . 6
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) |
6 | | cznrng.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑌) |
7 | | cznrng.0 |
. . . . . . . 8
⊢ 0 =
(0g‘𝑌) |
8 | 6, 7 | ring0cl 18392 |
. . . . . . 7
⊢ (𝑌 ∈ Ring → 0 ∈ 𝐵) |
9 | | eleq1a 2683 |
. . . . . . 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 444 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) → 𝐶 ∈ 𝐵) |
14 | | cznrng.x |
. . . . . 6
⊢ 𝑋 = (𝑌 sSet 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉) |
15 | 2, 6, 14 | cznabel 41746 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐶 ∈ 𝐵) → 𝑋 ∈ Abel) |
16 | 15 | adantlr 747 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) → 𝑋 ∈ Abel) |
17 | | eqid 2610 |
. . . . . 6
⊢
(mulGrp‘𝑋) =
(mulGrp‘𝑋) |
18 | 2, 6, 14 | cznrnglem 41745 |
. . . . . 6
⊢ 𝐵 = (Base‘𝑋) |
19 | 17, 18 | mgpbas 18318 |
. . . . 5
⊢ 𝐵 =
(Base‘(mulGrp‘𝑋)) |
20 | 14 | fveq2i 6106 |
. . . . . . 7
⊢
(mulGrp‘𝑋) =
(mulGrp‘(𝑌 sSet
〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉)) |
21 | | fvex 6113 |
. . . . . . . . 9
⊢
(ℤ/nℤ‘𝑁) ∈ V |
22 | 2, 21 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝑌 ∈ V |
23 | | fvex 6113 |
. . . . . . . . . 10
⊢
(Base‘𝑌)
∈ V |
24 | 6, 23 | eqeltri 2684 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
25 | 24, 24 | mpt2ex 7136 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V |
26 | | mulrid 15822 |
. . . . . . . . 9
⊢
.r = Slot (.r‘ndx) |
27 | 26 | setsid 15742 |
. . . . . . . 8
⊢ ((𝑌 ∈ V ∧ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) = (.r‘(𝑌 sSet 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉))) |
28 | 22, 25, 27 | mp2an 704 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) = (.r‘(𝑌 sSet 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉)) |
29 | 20, 28 | mgpplusg 18316 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) = (+g‘(mulGrp‘𝑋)) |
30 | 29 | eqcomi 2619 |
. . . . 5
⊢
(+g‘(mulGrp‘𝑋)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) |
31 | | ne0i 3880 |
. . . . . 6
⊢ (𝐶 ∈ 𝐵 → 𝐵 ≠ ∅) |
32 | 31 | adantl 481 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) → 𝐵 ≠ ∅) |
33 | | simpr 476 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ 𝐵) |
34 | 19, 30, 32, 33 | copissgrp 41598 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) → (mulGrp‘𝑋) ∈ SGrp) |
35 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝐶 = 0 → (𝐶(+g‘𝑌)𝐶) = ( 0 (+g‘𝑌)𝐶)) |
36 | 35 | ad3antlr 763 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝐶(+g‘𝑌)𝐶) = ( 0 (+g‘𝑌)𝐶)) |
37 | 4, 5 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑌 ∈ Ring) |
38 | | ringmnd 18379 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ Ring → 𝑌 ∈ Mnd) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑌 ∈ Mnd) |
40 | 39 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) → 𝑌 ∈ Mnd) |
41 | 40 | anim1i 590 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) → (𝑌 ∈ Mnd ∧ 𝐶 ∈ 𝐵)) |
42 | 41 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑌 ∈ Mnd ∧ 𝐶 ∈ 𝐵)) |
43 | | eqid 2610 |
. . . . . . . . . 10
⊢
(+g‘𝑌) = (+g‘𝑌) |
44 | 6, 43, 7 | mndlid 17134 |
. . . . . . . . 9
⊢ ((𝑌 ∈ Mnd ∧ 𝐶 ∈ 𝐵) → ( 0 (+g‘𝑌)𝐶) = 𝐶) |
45 | 42, 44 | syl 17 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ( 0 (+g‘𝑌)𝐶) = 𝐶) |
46 | 36, 45 | eqtrd 2644 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝐶(+g‘𝑌)𝐶) = 𝐶) |
47 | | eqidd 2611 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)) |
48 | | eqidd 2611 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → 𝐶 = 𝐶) |
49 | | simpr1 1060 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → 𝑎 ∈ 𝐵) |
50 | | simpr2 1061 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → 𝑏 ∈ 𝐵) |
51 | 33 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → 𝐶 ∈ 𝐵) |
52 | 47, 48, 49, 50, 51 | ovmpt2d 6686 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑏) = 𝐶) |
53 | | eqidd 2611 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑐)) → 𝐶 = 𝐶) |
54 | | simpr3 1062 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → 𝑐 ∈ 𝐵) |
55 | 47, 53, 49, 54, 51 | ovmpt2d 6686 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝐶) |
56 | 52, 55 | oveq12d 6567 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑏)(+g‘𝑌)(𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)) = (𝐶(+g‘𝑌)𝐶)) |
57 | | eqidd 2611 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑥 = 𝑎 ∧ 𝑦 = (𝑏(+g‘𝑌)𝑐))) → 𝐶 = 𝐶) |
58 | 37 | ad3antrrr 762 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → 𝑌 ∈ Ring) |
59 | 6, 43 | ringacl 18401 |
. . . . . . . . 9
⊢ ((𝑌 ∈ Ring ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) → (𝑏(+g‘𝑌)𝑐) ∈ 𝐵) |
60 | 58, 50, 54, 59 | syl3anc 1318 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑏(+g‘𝑌)𝑐) ∈ 𝐵) |
61 | 47, 57, 49, 60, 51 | ovmpt2d 6686 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)(𝑏(+g‘𝑌)𝑐)) = 𝐶) |
62 | 46, 56, 61 | 3eqtr4rd 2655 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)(𝑏(+g‘𝑌)𝑐)) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑏)(+g‘𝑌)(𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐))) |
63 | | eqidd 2611 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑥 = 𝑏 ∧ 𝑦 = 𝑐)) → 𝐶 = 𝐶) |
64 | 47, 63, 50, 54, 51 | ovmpt2d 6686 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑏(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝐶) |
65 | 55, 64 | oveq12d 6567 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)(+g‘𝑌)(𝑏(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)) = (𝐶(+g‘𝑌)𝐶)) |
66 | | eqidd 2611 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑥 = (𝑎(+g‘𝑌)𝑏) ∧ 𝑦 = 𝑐)) → 𝐶 = 𝐶) |
67 | 6, 43 | ringacl 18401 |
. . . . . . . . 9
⊢ ((𝑌 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(+g‘𝑌)𝑏) ∈ 𝐵) |
68 | 58, 49, 50, 67 | syl3anc 1318 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑎(+g‘𝑌)𝑏) ∈ 𝐵) |
69 | 47, 66, 68, 54, 51 | ovmpt2d 6686 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ((𝑎(+g‘𝑌)𝑏)(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝐶) |
70 | 46, 65, 69 | 3eqtr4rd 2655 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ((𝑎(+g‘𝑌)𝑏)(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)(+g‘𝑌)(𝑏(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐))) |
71 | 62, 70 | jca 553 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)(𝑏(+g‘𝑌)𝑐)) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑏)(+g‘𝑌)(𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)) ∧ ((𝑎(+g‘𝑌)𝑏)(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)(+g‘𝑌)(𝑏(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)))) |
72 | 71 | ralrimivvva 2955 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)(𝑏(+g‘𝑌)𝑐)) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑏)(+g‘𝑌)(𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)) ∧ ((𝑎(+g‘𝑌)𝑏)(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)(+g‘𝑌)(𝑏(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)))) |
73 | 16, 34, 72 | 3jca 1235 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵) → (𝑋 ∈ Abel ∧ (mulGrp‘𝑋) ∈ SGrp ∧
∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)(𝑏(+g‘𝑌)𝑐)) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑏)(+g‘𝑌)(𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)) ∧ ((𝑎(+g‘𝑌)𝑏)(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)(+g‘𝑌)(𝑏(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐))))) |
74 | 13, 73 | mpdan 699 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) → (𝑋 ∈ Abel ∧
(mulGrp‘𝑋) ∈
SGrp ∧ ∀𝑎 ∈
𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)(𝑏(+g‘𝑌)𝑐)) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑏)(+g‘𝑌)(𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)) ∧ ((𝑎(+g‘𝑌)𝑏)(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)(+g‘𝑌)(𝑏(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐))))) |
75 | | plusgid 15804 |
. . . . 5
⊢
+g = Slot (+g‘ndx) |
76 | | plusgndxnmulrndx 41743 |
. . . . 5
⊢
(+g‘ndx) ≠
(.r‘ndx) |
77 | 75, 76 | setsnid 15743 |
. . . 4
⊢
(+g‘𝑌) = (+g‘(𝑌 sSet 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉)) |
78 | 14 | fveq2i 6106 |
. . . 4
⊢
(+g‘𝑋) = (+g‘(𝑌 sSet 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉)) |
79 | 77, 78 | eqtr4i 2635 |
. . 3
⊢
(+g‘𝑌) = (+g‘𝑋) |
80 | 14 | eqcomi 2619 |
. . . . 5
⊢ (𝑌 sSet
〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉) = 𝑋 |
81 | 80 | fveq2i 6106 |
. . . 4
⊢
(.r‘(𝑌 sSet 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉)) = (.r‘𝑋) |
82 | 28, 81 | eqtri 2632 |
. . 3
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) = (.r‘𝑋) |
83 | 18, 17, 79, 82 | isrng 41666 |
. 2
⊢ (𝑋 ∈ Rng ↔ (𝑋 ∈ Abel ∧
(mulGrp‘𝑋) ∈
SGrp ∧ ∀𝑎 ∈
𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)(𝑏(+g‘𝑌)𝑐)) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑏)(+g‘𝑌)(𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)) ∧ ((𝑎(+g‘𝑌)𝑏)(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐)(+g‘𝑌)(𝑏(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐))))) |
84 | 74, 83 | sylibr 223 |
1
⊢ ((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) → 𝑋 ∈ Rng) |