Step | Hyp | Ref
| Expression |
1 | | elun 4109 |
. . 3
β’ (π β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)}) β (π β {πΌ} β¨ π β βͺ
π β (0..^π){(πΊβπ)})) |
2 | | elsni 4604 |
. . . . 5
β’ (π β {πΌ} β π = πΌ) |
3 | | smndex1ibas.m |
. . . . . . . 8
β’ π =
(EndoFMndββ0) |
4 | | smndex1ibas.n |
. . . . . . . 8
β’ π β β |
5 | | smndex1ibas.i |
. . . . . . . 8
β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) |
6 | 3, 4, 5 | smndex1iidm 18712 |
. . . . . . 7
β’ (πΌ β πΌ) = πΌ |
7 | | coeq2 5815 |
. . . . . . 7
β’ (π = πΌ β (πΌ β π) = (πΌ β πΌ)) |
8 | | id 22 |
. . . . . . 7
β’ (π = πΌ β π = πΌ) |
9 | 6, 7, 8 | 3eqtr4a 2803 |
. . . . . 6
β’ (π = πΌ β (πΌ β π) = π) |
10 | | coeq1 5814 |
. . . . . . 7
β’ (π = πΌ β (π β πΌ) = (πΌ β πΌ)) |
11 | 6, 10, 8 | 3eqtr4a 2803 |
. . . . . 6
β’ (π = πΌ β (π β πΌ) = π) |
12 | 9, 11 | jca 513 |
. . . . 5
β’ (π = πΌ β ((πΌ β π) = π β§ (π β πΌ) = π)) |
13 | 2, 12 | syl 17 |
. . . 4
β’ (π β {πΌ} β ((πΌ β π) = π β§ (π β πΌ) = π)) |
14 | | eliun 4959 |
. . . . 5
β’ (π β βͺ π β (0..^π){(πΊβπ)} β βπ β (0..^π)π β {(πΊβπ)}) |
15 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = π β (πΊβπ) = (πΊβπ)) |
16 | 15 | sneqd 4599 |
. . . . . . . 8
β’ (π = π β {(πΊβπ)} = {(πΊβπ)}) |
17 | 16 | eleq2d 2824 |
. . . . . . 7
β’ (π = π β (π β {(πΊβπ)} β π β {(πΊβπ)})) |
18 | 17 | cbvrexvw 3227 |
. . . . . 6
β’
(βπ β
(0..^π)π β {(πΊβπ)} β βπ β (0..^π)π β {(πΊβπ)}) |
19 | | elsni 4604 |
. . . . . . . . 9
β’ (π β {(πΊβπ)} β π = (πΊβπ)) |
20 | | smndex1ibas.g |
. . . . . . . . . . . 12
β’ πΊ = (π β (0..^π) β¦ (π₯ β β0 β¦ π)) |
21 | 3, 4, 5, 20 | smndex1igid 18715 |
. . . . . . . . . . 11
β’ (π β (0..^π) β (πΌ β (πΊβπ)) = (πΊβπ)) |
22 | 3, 4, 5 | smndex1ibas 18711 |
. . . . . . . . . . . 12
β’ πΌ β (Baseβπ) |
23 | 3, 4, 5, 20 | smndex1gid 18714 |
. . . . . . . . . . . 12
β’ ((πΌ β (Baseβπ) β§ π β (0..^π)) β ((πΊβπ) β πΌ) = (πΊβπ)) |
24 | 22, 23 | mpan 689 |
. . . . . . . . . . 11
β’ (π β (0..^π) β ((πΊβπ) β πΌ) = (πΊβπ)) |
25 | 21, 24 | jca 513 |
. . . . . . . . . 10
β’ (π β (0..^π) β ((πΌ β (πΊβπ)) = (πΊβπ) β§ ((πΊβπ) β πΌ) = (πΊβπ))) |
26 | | coeq2 5815 |
. . . . . . . . . . . 12
β’ (π = (πΊβπ) β (πΌ β π) = (πΌ β (πΊβπ))) |
27 | | id 22 |
. . . . . . . . . . . 12
β’ (π = (πΊβπ) β π = (πΊβπ)) |
28 | 26, 27 | eqeq12d 2753 |
. . . . . . . . . . 11
β’ (π = (πΊβπ) β ((πΌ β π) = π β (πΌ β (πΊβπ)) = (πΊβπ))) |
29 | | coeq1 5814 |
. . . . . . . . . . . 12
β’ (π = (πΊβπ) β (π β πΌ) = ((πΊβπ) β πΌ)) |
30 | 29, 27 | eqeq12d 2753 |
. . . . . . . . . . 11
β’ (π = (πΊβπ) β ((π β πΌ) = π β ((πΊβπ) β πΌ) = (πΊβπ))) |
31 | 28, 30 | anbi12d 632 |
. . . . . . . . . 10
β’ (π = (πΊβπ) β (((πΌ β π) = π β§ (π β πΌ) = π) β ((πΌ β (πΊβπ)) = (πΊβπ) β§ ((πΊβπ) β πΌ) = (πΊβπ)))) |
32 | 25, 31 | syl5ibr 246 |
. . . . . . . . 9
β’ (π = (πΊβπ) β (π β (0..^π) β ((πΌ β π) = π β§ (π β πΌ) = π))) |
33 | 19, 32 | syl 17 |
. . . . . . . 8
β’ (π β {(πΊβπ)} β (π β (0..^π) β ((πΌ β π) = π β§ (π β πΌ) = π))) |
34 | 33 | impcom 409 |
. . . . . . 7
β’ ((π β (0..^π) β§ π β {(πΊβπ)}) β ((πΌ β π) = π β§ (π β πΌ) = π)) |
35 | 34 | rexlimiva 3145 |
. . . . . 6
β’
(βπ β
(0..^π)π β {(πΊβπ)} β ((πΌ β π) = π β§ (π β πΌ) = π)) |
36 | 18, 35 | sylbi 216 |
. . . . 5
β’
(βπ β
(0..^π)π β {(πΊβπ)} β ((πΌ β π) = π β§ (π β πΌ) = π)) |
37 | 14, 36 | sylbi 216 |
. . . 4
β’ (π β βͺ π β (0..^π){(πΊβπ)} β ((πΌ β π) = π β§ (π β πΌ) = π)) |
38 | 13, 37 | jaoi 856 |
. . 3
β’ ((π β {πΌ} β¨ π β βͺ
π β (0..^π){(πΊβπ)}) β ((πΌ β π) = π β§ (π β πΌ) = π)) |
39 | 1, 38 | sylbi 216 |
. 2
β’ (π β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)}) β ((πΌ β π) = π β§ (π β πΌ) = π)) |
40 | | smndex1mgm.b |
. 2
β’ π΅ = ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)}) |
41 | 39, 40 | eleq2s 2856 |
1
β’ (π β π΅ β ((πΌ β π) = π β§ (π β πΌ) = π)) |