| Step | Hyp | Ref
| Expression |
| 1 | | smndex1ibas.m |
. . . . . . 7
⊢ 𝑀 =
(EndoFMnd‘ℕ0) |
| 2 | | smndex1ibas.n |
. . . . . . 7
⊢ 𝑁 ∈ ℕ |
| 3 | | smndex1ibas.i |
. . . . . . 7
⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) |
| 4 | | smndex1ibas.g |
. . . . . . 7
⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛)) |
| 5 | | smndex1mgm.b |
. . . . . . 7
⊢ 𝐵 = ({𝐼} ∪ ∪
𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)}) |
| 6 | 1, 2, 3, 4, 5 | smndex1basss 18918 |
. . . . . 6
⊢ 𝐵 ⊆ (Base‘𝑀) |
| 7 | | ssel 3977 |
. . . . . . 7
⊢ (𝐵 ⊆ (Base‘𝑀) → (𝑎 ∈ 𝐵 → 𝑎 ∈ (Base‘𝑀))) |
| 8 | | ssel 3977 |
. . . . . . 7
⊢ (𝐵 ⊆ (Base‘𝑀) → (𝑏 ∈ 𝐵 → 𝑏 ∈ (Base‘𝑀))) |
| 9 | 7, 8 | anim12d 609 |
. . . . . 6
⊢ (𝐵 ⊆ (Base‘𝑀) → ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎 ∈ (Base‘𝑀) ∧ 𝑏 ∈ (Base‘𝑀)))) |
| 10 | 6, 9 | ax-mp 5 |
. . . . 5
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎 ∈ (Base‘𝑀) ∧ 𝑏 ∈ (Base‘𝑀))) |
| 11 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑀) =
(Base‘𝑀) |
| 12 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝑀) = (+g‘𝑀) |
| 13 | 1, 11, 12 | efmndov 18894 |
. . . . 5
⊢ ((𝑎 ∈ (Base‘𝑀) ∧ 𝑏 ∈ (Base‘𝑀)) → (𝑎(+g‘𝑀)𝑏) = (𝑎 ∘ 𝑏)) |
| 14 | 10, 13 | syl 17 |
. . . 4
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(+g‘𝑀)𝑏) = (𝑎 ∘ 𝑏)) |
| 15 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝐼 ∧ 𝑏 = 𝐼) → 𝑎 = 𝐼) |
| 16 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝐼 ∧ 𝑏 = 𝐼) → 𝑏 = 𝐼) |
| 17 | 15, 16 | coeq12d 5875 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝐼 ∧ 𝑏 = 𝐼) → (𝑎 ∘ 𝑏) = (𝐼 ∘ 𝐼)) |
| 18 | 1, 2, 3 | smndex1iidm 18914 |
. . . . . . . . . . 11
⊢ (𝐼 ∘ 𝐼) = 𝐼 |
| 19 | 17, 18 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝐼 ∧ 𝑏 = 𝐼) → (𝑎 ∘ 𝑏) = 𝐼) |
| 20 | 19 | orcd 874 |
. . . . . . . . 9
⊢ ((𝑎 = 𝐼 ∧ 𝑏 = 𝐼) → ((𝑎 ∘ 𝑏) = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘))) |
| 21 | 20 | ex 412 |
. . . . . . . 8
⊢ (𝑎 = 𝐼 → (𝑏 = 𝐼 → ((𝑎 ∘ 𝑏) = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘)))) |
| 22 | | simpll 767 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 = 𝐼 ∧ 𝑘 ∈ (0..^𝑁)) ∧ 𝑏 = (𝐺‘𝑘)) → 𝑎 = 𝐼) |
| 23 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 = 𝐼 ∧ 𝑘 ∈ (0..^𝑁)) ∧ 𝑏 = (𝐺‘𝑘)) → 𝑏 = (𝐺‘𝑘)) |
| 24 | 22, 23 | coeq12d 5875 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 = 𝐼 ∧ 𝑘 ∈ (0..^𝑁)) ∧ 𝑏 = (𝐺‘𝑘)) → (𝑎 ∘ 𝑏) = (𝐼 ∘ (𝐺‘𝑘))) |
| 25 | 1, 2, 3, 4 | smndex1igid 18917 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (0..^𝑁) → (𝐼 ∘ (𝐺‘𝑘)) = (𝐺‘𝑘)) |
| 26 | 25 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 = 𝐼 ∧ 𝑘 ∈ (0..^𝑁)) ∧ 𝑏 = (𝐺‘𝑘)) → (𝐼 ∘ (𝐺‘𝑘)) = (𝐺‘𝑘)) |
| 27 | 24, 26 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (((𝑎 = 𝐼 ∧ 𝑘 ∈ (0..^𝑁)) ∧ 𝑏 = (𝐺‘𝑘)) → (𝑎 ∘ 𝑏) = (𝐺‘𝑘)) |
| 28 | 27 | ex 412 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝐼 ∧ 𝑘 ∈ (0..^𝑁)) → (𝑏 = (𝐺‘𝑘) → (𝑎 ∘ 𝑏) = (𝐺‘𝑘))) |
| 29 | 28 | reximdva 3168 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐼 → (∃𝑘 ∈ (0..^𝑁)𝑏 = (𝐺‘𝑘) → ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘))) |
| 30 | 29 | imp 406 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝐼 ∧ ∃𝑘 ∈ (0..^𝑁)𝑏 = (𝐺‘𝑘)) → ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘)) |
| 31 | 30 | olcd 875 |
. . . . . . . . 9
⊢ ((𝑎 = 𝐼 ∧ ∃𝑘 ∈ (0..^𝑁)𝑏 = (𝐺‘𝑘)) → ((𝑎 ∘ 𝑏) = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘))) |
| 32 | 31 | ex 412 |
. . . . . . . 8
⊢ (𝑎 = 𝐼 → (∃𝑘 ∈ (0..^𝑁)𝑏 = (𝐺‘𝑘) → ((𝑎 ∘ 𝑏) = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘)))) |
| 33 | 21, 32 | jaod 860 |
. . . . . . 7
⊢ (𝑎 = 𝐼 → ((𝑏 = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)𝑏 = (𝐺‘𝑘)) → ((𝑎 ∘ 𝑏) = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘)))) |
| 34 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝑏 = 𝐼 ∧ 𝑘 ∈ (0..^𝑁)) ∧ 𝑎 = (𝐺‘𝑘)) → 𝑎 = (𝐺‘𝑘)) |
| 35 | | simpll 767 |
. . . . . . . . . . . . . . 15
⊢ (((𝑏 = 𝐼 ∧ 𝑘 ∈ (0..^𝑁)) ∧ 𝑎 = (𝐺‘𝑘)) → 𝑏 = 𝐼) |
| 36 | 34, 35 | coeq12d 5875 |
. . . . . . . . . . . . . 14
⊢ (((𝑏 = 𝐼 ∧ 𝑘 ∈ (0..^𝑁)) ∧ 𝑎 = (𝐺‘𝑘)) → (𝑎 ∘ 𝑏) = ((𝐺‘𝑘) ∘ 𝐼)) |
| 37 | 1, 2, 3 | smndex1ibas 18913 |
. . . . . . . . . . . . . . . 16
⊢ 𝐼 ∈ (Base‘𝑀) |
| 38 | 1, 2, 3, 4 | smndex1gid 18916 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ (Base‘𝑀) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐺‘𝑘) ∘ 𝐼) = (𝐺‘𝑘)) |
| 39 | 37, 38 | mpan 690 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (0..^𝑁) → ((𝐺‘𝑘) ∘ 𝐼) = (𝐺‘𝑘)) |
| 40 | 39 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝑏 = 𝐼 ∧ 𝑘 ∈ (0..^𝑁)) ∧ 𝑎 = (𝐺‘𝑘)) → ((𝐺‘𝑘) ∘ 𝐼) = (𝐺‘𝑘)) |
| 41 | 36, 40 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (((𝑏 = 𝐼 ∧ 𝑘 ∈ (0..^𝑁)) ∧ 𝑎 = (𝐺‘𝑘)) → (𝑎 ∘ 𝑏) = (𝐺‘𝑘)) |
| 42 | 41 | ex 412 |
. . . . . . . . . . . 12
⊢ ((𝑏 = 𝐼 ∧ 𝑘 ∈ (0..^𝑁)) → (𝑎 = (𝐺‘𝑘) → (𝑎 ∘ 𝑏) = (𝐺‘𝑘))) |
| 43 | 42 | reximdva 3168 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝐼 → (∃𝑘 ∈ (0..^𝑁)𝑎 = (𝐺‘𝑘) → ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘))) |
| 44 | 43 | imp 406 |
. . . . . . . . . 10
⊢ ((𝑏 = 𝐼 ∧ ∃𝑘 ∈ (0..^𝑁)𝑎 = (𝐺‘𝑘)) → ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘)) |
| 45 | 44 | olcd 875 |
. . . . . . . . 9
⊢ ((𝑏 = 𝐼 ∧ ∃𝑘 ∈ (0..^𝑁)𝑎 = (𝐺‘𝑘)) → ((𝑎 ∘ 𝑏) = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘))) |
| 46 | 45 | expcom 413 |
. . . . . . . 8
⊢
(∃𝑘 ∈
(0..^𝑁)𝑎 = (𝐺‘𝑘) → (𝑏 = 𝐼 → ((𝑎 ∘ 𝑏) = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘)))) |
| 47 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (𝐺‘𝑘) = (𝐺‘𝑚)) |
| 48 | 47 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → (𝑏 = (𝐺‘𝑘) ↔ 𝑏 = (𝐺‘𝑚))) |
| 49 | 48 | cbvrexvw 3238 |
. . . . . . . . 9
⊢
(∃𝑘 ∈
(0..^𝑁)𝑏 = (𝐺‘𝑘) ↔ ∃𝑚 ∈ (0..^𝑁)𝑏 = (𝐺‘𝑚)) |
| 50 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑚 ∈ (0..^𝑁) ∧ 𝑏 = (𝐺‘𝑚)) ∧ 𝑘 ∈ (0..^𝑁)) ∧ 𝑎 = (𝐺‘𝑘)) → 𝑎 = (𝐺‘𝑘)) |
| 51 | | simpllr 776 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑚 ∈ (0..^𝑁) ∧ 𝑏 = (𝐺‘𝑚)) ∧ 𝑘 ∈ (0..^𝑁)) ∧ 𝑎 = (𝐺‘𝑘)) → 𝑏 = (𝐺‘𝑚)) |
| 52 | 50, 51 | coeq12d 5875 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑚 ∈ (0..^𝑁) ∧ 𝑏 = (𝐺‘𝑚)) ∧ 𝑘 ∈ (0..^𝑁)) ∧ 𝑎 = (𝐺‘𝑘)) → (𝑎 ∘ 𝑏) = ((𝐺‘𝑘) ∘ (𝐺‘𝑚))) |
| 53 | 1, 2, 3, 4 | smndex1gbas 18915 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ (0..^𝑁) → (𝐺‘𝑚) ∈ (Base‘𝑀)) |
| 54 | 1, 2, 3, 4 | smndex1gid 18916 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺‘𝑚) ∈ (Base‘𝑀) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐺‘𝑘) ∘ (𝐺‘𝑚)) = (𝐺‘𝑘)) |
| 55 | 53, 54 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ (0..^𝑁) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐺‘𝑘) ∘ (𝐺‘𝑚)) = (𝐺‘𝑘)) |
| 56 | 55 | ad4ant13 751 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑚 ∈ (0..^𝑁) ∧ 𝑏 = (𝐺‘𝑚)) ∧ 𝑘 ∈ (0..^𝑁)) ∧ 𝑎 = (𝐺‘𝑘)) → ((𝐺‘𝑘) ∘ (𝐺‘𝑚)) = (𝐺‘𝑘)) |
| 57 | 52, 56 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑚 ∈ (0..^𝑁) ∧ 𝑏 = (𝐺‘𝑚)) ∧ 𝑘 ∈ (0..^𝑁)) ∧ 𝑎 = (𝐺‘𝑘)) → (𝑎 ∘ 𝑏) = (𝐺‘𝑘)) |
| 58 | 57 | ex 412 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ (0..^𝑁) ∧ 𝑏 = (𝐺‘𝑚)) ∧ 𝑘 ∈ (0..^𝑁)) → (𝑎 = (𝐺‘𝑘) → (𝑎 ∘ 𝑏) = (𝐺‘𝑘))) |
| 59 | 58 | reximdva 3168 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ (0..^𝑁) ∧ 𝑏 = (𝐺‘𝑚)) → (∃𝑘 ∈ (0..^𝑁)𝑎 = (𝐺‘𝑘) → ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘))) |
| 60 | 59 | rexlimiva 3147 |
. . . . . . . . . . . 12
⊢
(∃𝑚 ∈
(0..^𝑁)𝑏 = (𝐺‘𝑚) → (∃𝑘 ∈ (0..^𝑁)𝑎 = (𝐺‘𝑘) → ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘))) |
| 61 | 60 | imp 406 |
. . . . . . . . . . 11
⊢
((∃𝑚 ∈
(0..^𝑁)𝑏 = (𝐺‘𝑚) ∧ ∃𝑘 ∈ (0..^𝑁)𝑎 = (𝐺‘𝑘)) → ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘)) |
| 62 | 61 | olcd 875 |
. . . . . . . . . 10
⊢
((∃𝑚 ∈
(0..^𝑁)𝑏 = (𝐺‘𝑚) ∧ ∃𝑘 ∈ (0..^𝑁)𝑎 = (𝐺‘𝑘)) → ((𝑎 ∘ 𝑏) = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘))) |
| 63 | 62 | expcom 413 |
. . . . . . . . 9
⊢
(∃𝑘 ∈
(0..^𝑁)𝑎 = (𝐺‘𝑘) → (∃𝑚 ∈ (0..^𝑁)𝑏 = (𝐺‘𝑚) → ((𝑎 ∘ 𝑏) = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘)))) |
| 64 | 49, 63 | biimtrid 242 |
. . . . . . . 8
⊢
(∃𝑘 ∈
(0..^𝑁)𝑎 = (𝐺‘𝑘) → (∃𝑘 ∈ (0..^𝑁)𝑏 = (𝐺‘𝑘) → ((𝑎 ∘ 𝑏) = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘)))) |
| 65 | 46, 64 | jaod 860 |
. . . . . . 7
⊢
(∃𝑘 ∈
(0..^𝑁)𝑎 = (𝐺‘𝑘) → ((𝑏 = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)𝑏 = (𝐺‘𝑘)) → ((𝑎 ∘ 𝑏) = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘)))) |
| 66 | 33, 65 | jaoi 858 |
. . . . . 6
⊢ ((𝑎 = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)𝑎 = (𝐺‘𝑘)) → ((𝑏 = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)𝑏 = (𝐺‘𝑘)) → ((𝑎 ∘ 𝑏) = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘)))) |
| 67 | 66 | imp 406 |
. . . . 5
⊢ (((𝑎 = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)𝑎 = (𝐺‘𝑘)) ∧ (𝑏 = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)𝑏 = (𝐺‘𝑘))) → ((𝑎 ∘ 𝑏) = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘))) |
| 68 | 5 | eleq2i 2833 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝐵 ↔ 𝑎 ∈ ({𝐼} ∪ ∪
𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})) |
| 69 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘)) |
| 70 | 69 | sneqd 4638 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → {(𝐺‘𝑛)} = {(𝐺‘𝑘)}) |
| 71 | 70 | cbviunv 5040 |
. . . . . . . . . 10
⊢ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)} = ∪
𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)} |
| 72 | 71 | uneq2i 4165 |
. . . . . . . . 9
⊢ ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)}) = ({𝐼} ∪ ∪
𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)}) |
| 73 | 72 | eleq2i 2833 |
. . . . . . . 8
⊢ (𝑎 ∈ ({𝐼} ∪ ∪
𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)}) ↔ 𝑎 ∈ ({𝐼} ∪ ∪
𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)})) |
| 74 | 68, 73 | bitri 275 |
. . . . . . 7
⊢ (𝑎 ∈ 𝐵 ↔ 𝑎 ∈ ({𝐼} ∪ ∪
𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)})) |
| 75 | | elun 4153 |
. . . . . . 7
⊢ (𝑎 ∈ ({𝐼} ∪ ∪
𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)}) ↔ (𝑎 ∈ {𝐼} ∨ 𝑎 ∈ ∪
𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)})) |
| 76 | | velsn 4642 |
. . . . . . . 8
⊢ (𝑎 ∈ {𝐼} ↔ 𝑎 = 𝐼) |
| 77 | | eliun 4995 |
. . . . . . . . 9
⊢ (𝑎 ∈ ∪ 𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)} ↔ ∃𝑘 ∈ (0..^𝑁)𝑎 ∈ {(𝐺‘𝑘)}) |
| 78 | | velsn 4642 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {(𝐺‘𝑘)} ↔ 𝑎 = (𝐺‘𝑘)) |
| 79 | 78 | rexbii 3094 |
. . . . . . . . 9
⊢
(∃𝑘 ∈
(0..^𝑁)𝑎 ∈ {(𝐺‘𝑘)} ↔ ∃𝑘 ∈ (0..^𝑁)𝑎 = (𝐺‘𝑘)) |
| 80 | 77, 79 | bitri 275 |
. . . . . . . 8
⊢ (𝑎 ∈ ∪ 𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)} ↔ ∃𝑘 ∈ (0..^𝑁)𝑎 = (𝐺‘𝑘)) |
| 81 | 76, 80 | orbi12i 915 |
. . . . . . 7
⊢ ((𝑎 ∈ {𝐼} ∨ 𝑎 ∈ ∪
𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)}) ↔ (𝑎 = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)𝑎 = (𝐺‘𝑘))) |
| 82 | 74, 75, 81 | 3bitri 297 |
. . . . . 6
⊢ (𝑎 ∈ 𝐵 ↔ (𝑎 = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)𝑎 = (𝐺‘𝑘))) |
| 83 | 5 | eleq2i 2833 |
. . . . . . . 8
⊢ (𝑏 ∈ 𝐵 ↔ 𝑏 ∈ ({𝐼} ∪ ∪
𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})) |
| 84 | 72 | eleq2i 2833 |
. . . . . . . 8
⊢ (𝑏 ∈ ({𝐼} ∪ ∪
𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)}) ↔ 𝑏 ∈ ({𝐼} ∪ ∪
𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)})) |
| 85 | 83, 84 | bitri 275 |
. . . . . . 7
⊢ (𝑏 ∈ 𝐵 ↔ 𝑏 ∈ ({𝐼} ∪ ∪
𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)})) |
| 86 | | elun 4153 |
. . . . . . 7
⊢ (𝑏 ∈ ({𝐼} ∪ ∪
𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)}) ↔ (𝑏 ∈ {𝐼} ∨ 𝑏 ∈ ∪
𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)})) |
| 87 | | velsn 4642 |
. . . . . . . 8
⊢ (𝑏 ∈ {𝐼} ↔ 𝑏 = 𝐼) |
| 88 | | eliun 4995 |
. . . . . . . . 9
⊢ (𝑏 ∈ ∪ 𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)} ↔ ∃𝑘 ∈ (0..^𝑁)𝑏 ∈ {(𝐺‘𝑘)}) |
| 89 | | velsn 4642 |
. . . . . . . . . 10
⊢ (𝑏 ∈ {(𝐺‘𝑘)} ↔ 𝑏 = (𝐺‘𝑘)) |
| 90 | 89 | rexbii 3094 |
. . . . . . . . 9
⊢
(∃𝑘 ∈
(0..^𝑁)𝑏 ∈ {(𝐺‘𝑘)} ↔ ∃𝑘 ∈ (0..^𝑁)𝑏 = (𝐺‘𝑘)) |
| 91 | 88, 90 | bitri 275 |
. . . . . . . 8
⊢ (𝑏 ∈ ∪ 𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)} ↔ ∃𝑘 ∈ (0..^𝑁)𝑏 = (𝐺‘𝑘)) |
| 92 | 87, 91 | orbi12i 915 |
. . . . . . 7
⊢ ((𝑏 ∈ {𝐼} ∨ 𝑏 ∈ ∪
𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)}) ↔ (𝑏 = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)𝑏 = (𝐺‘𝑘))) |
| 93 | 85, 86, 92 | 3bitri 297 |
. . . . . 6
⊢ (𝑏 ∈ 𝐵 ↔ (𝑏 = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)𝑏 = (𝐺‘𝑘))) |
| 94 | 82, 93 | anbi12i 628 |
. . . . 5
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ↔ ((𝑎 = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)𝑎 = (𝐺‘𝑘)) ∧ (𝑏 = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)𝑏 = (𝐺‘𝑘)))) |
| 95 | 5 | eleq2i 2833 |
. . . . . . 7
⊢ ((𝑎 ∘ 𝑏) ∈ 𝐵 ↔ (𝑎 ∘ 𝑏) ∈ ({𝐼} ∪ ∪
𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})) |
| 96 | 72 | eleq2i 2833 |
. . . . . . 7
⊢ ((𝑎 ∘ 𝑏) ∈ ({𝐼} ∪ ∪
𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)}) ↔ (𝑎 ∘ 𝑏) ∈ ({𝐼} ∪ ∪
𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)})) |
| 97 | 95, 96 | bitri 275 |
. . . . . 6
⊢ ((𝑎 ∘ 𝑏) ∈ 𝐵 ↔ (𝑎 ∘ 𝑏) ∈ ({𝐼} ∪ ∪
𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)})) |
| 98 | | elun 4153 |
. . . . . 6
⊢ ((𝑎 ∘ 𝑏) ∈ ({𝐼} ∪ ∪
𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)}) ↔ ((𝑎 ∘ 𝑏) ∈ {𝐼} ∨ (𝑎 ∘ 𝑏) ∈ ∪
𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)})) |
| 99 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
| 100 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑏 ∈ V |
| 101 | 99, 100 | coex 7952 |
. . . . . . . 8
⊢ (𝑎 ∘ 𝑏) ∈ V |
| 102 | 101 | elsn 4641 |
. . . . . . 7
⊢ ((𝑎 ∘ 𝑏) ∈ {𝐼} ↔ (𝑎 ∘ 𝑏) = 𝐼) |
| 103 | | eliun 4995 |
. . . . . . . 8
⊢ ((𝑎 ∘ 𝑏) ∈ ∪
𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)} ↔ ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) ∈ {(𝐺‘𝑘)}) |
| 104 | 101 | elsn 4641 |
. . . . . . . . 9
⊢ ((𝑎 ∘ 𝑏) ∈ {(𝐺‘𝑘)} ↔ (𝑎 ∘ 𝑏) = (𝐺‘𝑘)) |
| 105 | 104 | rexbii 3094 |
. . . . . . . 8
⊢
(∃𝑘 ∈
(0..^𝑁)(𝑎 ∘ 𝑏) ∈ {(𝐺‘𝑘)} ↔ ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘)) |
| 106 | 103, 105 | bitri 275 |
. . . . . . 7
⊢ ((𝑎 ∘ 𝑏) ∈ ∪
𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)} ↔ ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘)) |
| 107 | 102, 106 | orbi12i 915 |
. . . . . 6
⊢ (((𝑎 ∘ 𝑏) ∈ {𝐼} ∨ (𝑎 ∘ 𝑏) ∈ ∪
𝑘 ∈ (0..^𝑁){(𝐺‘𝑘)}) ↔ ((𝑎 ∘ 𝑏) = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘))) |
| 108 | 97, 98, 107 | 3bitri 297 |
. . . . 5
⊢ ((𝑎 ∘ 𝑏) ∈ 𝐵 ↔ ((𝑎 ∘ 𝑏) = 𝐼 ∨ ∃𝑘 ∈ (0..^𝑁)(𝑎 ∘ 𝑏) = (𝐺‘𝑘))) |
| 109 | 67, 94, 108 | 3imtr4i 292 |
. . . 4
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎 ∘ 𝑏) ∈ 𝐵) |
| 110 | 14, 109 | eqeltrd 2841 |
. . 3
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(+g‘𝑀)𝑏) ∈ 𝐵) |
| 111 | 110 | rgen2 3199 |
. 2
⊢
∀𝑎 ∈
𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵 |
| 112 | | smndex1mgm.s |
. . . 4
⊢ 𝑆 = (𝑀 ↾s 𝐵) |
| 113 | 112 | ovexi 7465 |
. . 3
⊢ 𝑆 ∈ V |
| 114 | 1, 2, 3, 4, 5, 112 | smndex1bas 18919 |
. . . . 5
⊢
(Base‘𝑆) =
𝐵 |
| 115 | 114 | eqcomi 2746 |
. . . 4
⊢ 𝐵 = (Base‘𝑆) |
| 116 | 115 | fvexi 6920 |
. . . . 5
⊢ 𝐵 ∈ V |
| 117 | 112, 12 | ressplusg 17334 |
. . . . 5
⊢ (𝐵 ∈ V →
(+g‘𝑀) =
(+g‘𝑆)) |
| 118 | 116, 117 | ax-mp 5 |
. . . 4
⊢
(+g‘𝑀) = (+g‘𝑆) |
| 119 | 115, 118 | ismgm 18654 |
. . 3
⊢ (𝑆 ∈ V → (𝑆 ∈ Mgm ↔ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵)) |
| 120 | 113, 119 | ax-mp 5 |
. 2
⊢ (𝑆 ∈ Mgm ↔ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵) |
| 121 | 111, 120 | mpbir 231 |
1
⊢ 𝑆 ∈ Mgm |