| Step | Hyp | Ref
| Expression |
| 1 | | smndex1ibas.m |
. . 3
⊢ 𝑀 =
(EndoFMnd‘ℕ0) |
| 2 | | smndex1ibas.n |
. . 3
⊢ 𝑁 ∈ ℕ |
| 3 | | smndex1ibas.i |
. . 3
⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) |
| 4 | | smndex1ibas.g |
. . 3
⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛)) |
| 5 | | smndex1mgm.b |
. . 3
⊢ 𝐵 = ({𝐼} ∪ ∪
𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)}) |
| 6 | | smndex1mgm.s |
. . 3
⊢ 𝑆 = (𝑀 ↾s 𝐵) |
| 7 | 1, 2, 3, 4, 5, 6 | smndex1sgrp 18921 |
. 2
⊢ 𝑆 ∈ Smgrp |
| 8 | | nn0ex 12532 |
. . . . . . . . 9
⊢
ℕ0 ∈ V |
| 9 | 8 | mptex 7243 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ0
↦ (𝑥 mod 𝑁)) ∈ V |
| 10 | 3, 9 | eqeltri 2837 |
. . . . . . 7
⊢ 𝐼 ∈ V |
| 11 | 10 | snid 4662 |
. . . . . 6
⊢ 𝐼 ∈ {𝐼} |
| 12 | | elun1 4182 |
. . . . . 6
⊢ (𝐼 ∈ {𝐼} → 𝐼 ∈ ({𝐼} ∪ ∪
𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})) |
| 13 | 11, 12 | ax-mp 5 |
. . . . 5
⊢ 𝐼 ∈ ({𝐼} ∪ ∪
𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)}) |
| 14 | 13, 5 | eleqtrri 2840 |
. . . 4
⊢ 𝐼 ∈ 𝐵 |
| 15 | | id 22 |
. . . . 5
⊢ (𝐼 ∈ 𝐵 → 𝐼 ∈ 𝐵) |
| 16 | | coeq1 5868 |
. . . . . . . . 9
⊢ (𝑎 = 𝐼 → (𝑎 ∘ 𝑏) = (𝐼 ∘ 𝑏)) |
| 17 | 16 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑎 = 𝐼 → ((𝑎 ∘ 𝑏) = 𝑏 ↔ (𝐼 ∘ 𝑏) = 𝑏)) |
| 18 | | coeq2 5869 |
. . . . . . . . 9
⊢ (𝑎 = 𝐼 → (𝑏 ∘ 𝑎) = (𝑏 ∘ 𝐼)) |
| 19 | 18 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑎 = 𝐼 → ((𝑏 ∘ 𝑎) = 𝑏 ↔ (𝑏 ∘ 𝐼) = 𝑏)) |
| 20 | 17, 19 | anbi12d 632 |
. . . . . . 7
⊢ (𝑎 = 𝐼 → (((𝑎 ∘ 𝑏) = 𝑏 ∧ (𝑏 ∘ 𝑎) = 𝑏) ↔ ((𝐼 ∘ 𝑏) = 𝑏 ∧ (𝑏 ∘ 𝐼) = 𝑏))) |
| 21 | 20 | ralbidv 3178 |
. . . . . 6
⊢ (𝑎 = 𝐼 → (∀𝑏 ∈ 𝐵 ((𝑎 ∘ 𝑏) = 𝑏 ∧ (𝑏 ∘ 𝑎) = 𝑏) ↔ ∀𝑏 ∈ 𝐵 ((𝐼 ∘ 𝑏) = 𝑏 ∧ (𝑏 ∘ 𝐼) = 𝑏))) |
| 22 | 21 | adantl 481 |
. . . . 5
⊢ ((𝐼 ∈ 𝐵 ∧ 𝑎 = 𝐼) → (∀𝑏 ∈ 𝐵 ((𝑎 ∘ 𝑏) = 𝑏 ∧ (𝑏 ∘ 𝑎) = 𝑏) ↔ ∀𝑏 ∈ 𝐵 ((𝐼 ∘ 𝑏) = 𝑏 ∧ (𝑏 ∘ 𝐼) = 𝑏))) |
| 23 | 1, 2, 3, 4, 5, 6 | smndex1mndlem 18922 |
. . . . . . 7
⊢ (𝑏 ∈ 𝐵 → ((𝐼 ∘ 𝑏) = 𝑏 ∧ (𝑏 ∘ 𝐼) = 𝑏)) |
| 24 | 23 | rgen 3063 |
. . . . . 6
⊢
∀𝑏 ∈
𝐵 ((𝐼 ∘ 𝑏) = 𝑏 ∧ (𝑏 ∘ 𝐼) = 𝑏) |
| 25 | 24 | a1i 11 |
. . . . 5
⊢ (𝐼 ∈ 𝐵 → ∀𝑏 ∈ 𝐵 ((𝐼 ∘ 𝑏) = 𝑏 ∧ (𝑏 ∘ 𝐼) = 𝑏)) |
| 26 | 15, 22, 25 | rspcedvd 3624 |
. . . 4
⊢ (𝐼 ∈ 𝐵 → ∃𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎 ∘ 𝑏) = 𝑏 ∧ (𝑏 ∘ 𝑎) = 𝑏)) |
| 27 | 14, 26 | ax-mp 5 |
. . 3
⊢
∃𝑎 ∈
𝐵 ∀𝑏 ∈ 𝐵 ((𝑎 ∘ 𝑏) = 𝑏 ∧ (𝑏 ∘ 𝑎) = 𝑏) |
| 28 | 1, 2, 3, 4, 5 | smndex1basss 18918 |
. . . . . . 7
⊢ 𝐵 ⊆ (Base‘𝑀) |
| 29 | | ssel 3977 |
. . . . . . . 8
⊢ (𝐵 ⊆ (Base‘𝑀) → (𝑎 ∈ 𝐵 → 𝑎 ∈ (Base‘𝑀))) |
| 30 | | ssel 3977 |
. . . . . . . 8
⊢ (𝐵 ⊆ (Base‘𝑀) → (𝑏 ∈ 𝐵 → 𝑏 ∈ (Base‘𝑀))) |
| 31 | 29, 30 | anim12d 609 |
. . . . . . 7
⊢ (𝐵 ⊆ (Base‘𝑀) → ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎 ∈ (Base‘𝑀) ∧ 𝑏 ∈ (Base‘𝑀)))) |
| 32 | 28, 31 | ax-mp 5 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎 ∈ (Base‘𝑀) ∧ 𝑏 ∈ (Base‘𝑀))) |
| 33 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝑀) =
(Base‘𝑀) |
| 34 | | snex 5436 |
. . . . . . . . . . . . 13
⊢ {𝐼} ∈ V |
| 35 | | ovex 7464 |
. . . . . . . . . . . . . 14
⊢
(0..^𝑁) ∈
V |
| 36 | | snex 5436 |
. . . . . . . . . . . . . 14
⊢ {(𝐺‘𝑛)} ∈ V |
| 37 | 35, 36 | iunex 7993 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)} ∈ V |
| 38 | 34, 37 | unex 7764 |
. . . . . . . . . . . 12
⊢ ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)}) ∈ V |
| 39 | 5, 38 | eqeltri 2837 |
. . . . . . . . . . 11
⊢ 𝐵 ∈ V |
| 40 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(+g‘𝑀) = (+g‘𝑀) |
| 41 | 6, 40 | ressplusg 17334 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ V →
(+g‘𝑀) =
(+g‘𝑆)) |
| 42 | 39, 41 | ax-mp 5 |
. . . . . . . . . 10
⊢
(+g‘𝑀) = (+g‘𝑆) |
| 43 | 42 | eqcomi 2746 |
. . . . . . . . 9
⊢
(+g‘𝑆) = (+g‘𝑀) |
| 44 | 1, 33, 43 | efmndov 18894 |
. . . . . . . 8
⊢ ((𝑎 ∈ (Base‘𝑀) ∧ 𝑏 ∈ (Base‘𝑀)) → (𝑎(+g‘𝑆)𝑏) = (𝑎 ∘ 𝑏)) |
| 45 | 44 | eqeq1d 2739 |
. . . . . . 7
⊢ ((𝑎 ∈ (Base‘𝑀) ∧ 𝑏 ∈ (Base‘𝑀)) → ((𝑎(+g‘𝑆)𝑏) = 𝑏 ↔ (𝑎 ∘ 𝑏) = 𝑏)) |
| 46 | 43 | oveqi 7444 |
. . . . . . . . 9
⊢ (𝑏(+g‘𝑆)𝑎) = (𝑏(+g‘𝑀)𝑎) |
| 47 | 1, 33, 40 | efmndov 18894 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ (Base‘𝑀) ∧ 𝑎 ∈ (Base‘𝑀)) → (𝑏(+g‘𝑀)𝑎) = (𝑏 ∘ 𝑎)) |
| 48 | 47 | ancoms 458 |
. . . . . . . . 9
⊢ ((𝑎 ∈ (Base‘𝑀) ∧ 𝑏 ∈ (Base‘𝑀)) → (𝑏(+g‘𝑀)𝑎) = (𝑏 ∘ 𝑎)) |
| 49 | 46, 48 | eqtrid 2789 |
. . . . . . . 8
⊢ ((𝑎 ∈ (Base‘𝑀) ∧ 𝑏 ∈ (Base‘𝑀)) → (𝑏(+g‘𝑆)𝑎) = (𝑏 ∘ 𝑎)) |
| 50 | 49 | eqeq1d 2739 |
. . . . . . 7
⊢ ((𝑎 ∈ (Base‘𝑀) ∧ 𝑏 ∈ (Base‘𝑀)) → ((𝑏(+g‘𝑆)𝑎) = 𝑏 ↔ (𝑏 ∘ 𝑎) = 𝑏)) |
| 51 | 45, 50 | anbi12d 632 |
. . . . . 6
⊢ ((𝑎 ∈ (Base‘𝑀) ∧ 𝑏 ∈ (Base‘𝑀)) → (((𝑎(+g‘𝑆)𝑏) = 𝑏 ∧ (𝑏(+g‘𝑆)𝑎) = 𝑏) ↔ ((𝑎 ∘ 𝑏) = 𝑏 ∧ (𝑏 ∘ 𝑎) = 𝑏))) |
| 52 | 32, 51 | syl 17 |
. . . . 5
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (((𝑎(+g‘𝑆)𝑏) = 𝑏 ∧ (𝑏(+g‘𝑆)𝑎) = 𝑏) ↔ ((𝑎 ∘ 𝑏) = 𝑏 ∧ (𝑏 ∘ 𝑎) = 𝑏))) |
| 53 | 52 | ralbidva 3176 |
. . . 4
⊢ (𝑎 ∈ 𝐵 → (∀𝑏 ∈ 𝐵 ((𝑎(+g‘𝑆)𝑏) = 𝑏 ∧ (𝑏(+g‘𝑆)𝑎) = 𝑏) ↔ ∀𝑏 ∈ 𝐵 ((𝑎 ∘ 𝑏) = 𝑏 ∧ (𝑏 ∘ 𝑎) = 𝑏))) |
| 54 | 53 | rexbiia 3092 |
. . 3
⊢
(∃𝑎 ∈
𝐵 ∀𝑏 ∈ 𝐵 ((𝑎(+g‘𝑆)𝑏) = 𝑏 ∧ (𝑏(+g‘𝑆)𝑎) = 𝑏) ↔ ∃𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎 ∘ 𝑏) = 𝑏 ∧ (𝑏 ∘ 𝑎) = 𝑏)) |
| 55 | 27, 54 | mpbir 231 |
. 2
⊢
∃𝑎 ∈
𝐵 ∀𝑏 ∈ 𝐵 ((𝑎(+g‘𝑆)𝑏) = 𝑏 ∧ (𝑏(+g‘𝑆)𝑎) = 𝑏) |
| 56 | 1, 2, 3, 4, 5, 6 | smndex1bas 18919 |
. . . 4
⊢
(Base‘𝑆) =
𝐵 |
| 57 | 56 | eqcomi 2746 |
. . 3
⊢ 𝐵 = (Base‘𝑆) |
| 58 | | eqid 2737 |
. . 3
⊢
(+g‘𝑆) = (+g‘𝑆) |
| 59 | 57, 58 | ismnddef 18749 |
. 2
⊢ (𝑆 ∈ Mnd ↔ (𝑆 ∈ Smgrp ∧ ∃𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎(+g‘𝑆)𝑏) = 𝑏 ∧ (𝑏(+g‘𝑆)𝑎) = 𝑏))) |
| 60 | 7, 55, 59 | mpbir2an 711 |
1
⊢ 𝑆 ∈ Mnd |