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 18716 |
. . . . . 6
β’ π΅ β (Baseβπ) |
7 | | ssel 3938 |
. . . . . . 7
β’ (π΅ β (Baseβπ) β (π β π΅ β π β (Baseβπ))) |
8 | | ssel 3938 |
. . . . . . 7
β’ (π΅ β (Baseβπ) β (π β π΅ β π β (Baseβπ))) |
9 | 7, 8 | anim12d 610 |
. . . . . 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 18692 |
. . . . 5
β’ ((π β (Baseβπ) β§ π β (Baseβπ)) β (π(+gβπ)π) = (π β π)) |
14 | 10, 13 | syl 17 |
. . . 4
β’ ((π β π΅ β§ π β π΅) β (π(+gβπ)π) = (π β π)) |
15 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π = πΌ β§ π = πΌ) β π = πΌ) |
16 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π = πΌ β§ π = πΌ) β π = πΌ) |
17 | 15, 16 | coeq12d 5821 |
. . . . . . . . . . 11
β’ ((π = πΌ β§ π = πΌ) β (π β π) = (πΌ β πΌ)) |
18 | 1, 2, 3 | smndex1iidm 18712 |
. . . . . . . . . . 11
β’ (πΌ β πΌ) = πΌ |
19 | 17, 18 | eqtrdi 2793 |
. . . . . . . . . 10
β’ ((π = πΌ β§ π = πΌ) β (π β π) = πΌ) |
20 | 19 | orcd 872 |
. . . . . . . . 9
β’ ((π = πΌ β§ π = πΌ) β ((π β π) = πΌ β¨ βπ β (0..^π)(π β π) = (πΊβπ))) |
21 | 20 | ex 414 |
. . . . . . . 8
β’ (π = πΌ β (π = πΌ β ((π β π) = πΌ β¨ βπ β (0..^π)(π β π) = (πΊβπ)))) |
22 | | simpll 766 |
. . . . . . . . . . . . . . 15
β’ (((π = πΌ β§ π β (0..^π)) β§ π = (πΊβπ)) β π = πΌ) |
23 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ (((π = πΌ β§ π β (0..^π)) β§ π = (πΊβπ)) β π = (πΊβπ)) |
24 | 22, 23 | coeq12d 5821 |
. . . . . . . . . . . . . 14
β’ (((π = πΌ β§ π β (0..^π)) β§ π = (πΊβπ)) β (π β π) = (πΌ β (πΊβπ))) |
25 | 1, 2, 3, 4 | smndex1igid 18715 |
. . . . . . . . . . . . . . 15
β’ (π β (0..^π) β (πΌ β (πΊβπ)) = (πΊβπ)) |
26 | 25 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π = πΌ β§ π β (0..^π)) β§ π = (πΊβπ)) β (πΌ β (πΊβπ)) = (πΊβπ)) |
27 | 24, 26 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π = πΌ β§ π β (0..^π)) β§ π = (πΊβπ)) β (π β π) = (πΊβπ)) |
28 | 27 | ex 414 |
. . . . . . . . . . . 12
β’ ((π = πΌ β§ π β (0..^π)) β (π = (πΊβπ) β (π β π) = (πΊβπ))) |
29 | 28 | reximdva 3166 |
. . . . . . . . . . 11
β’ (π = πΌ β (βπ β (0..^π)π = (πΊβπ) β βπ β (0..^π)(π β π) = (πΊβπ))) |
30 | 29 | imp 408 |
. . . . . . . . . 10
β’ ((π = πΌ β§ βπ β (0..^π)π = (πΊβπ)) β βπ β (0..^π)(π β π) = (πΊβπ)) |
31 | 30 | olcd 873 |
. . . . . . . . 9
β’ ((π = πΌ β§ βπ β (0..^π)π = (πΊβπ)) β ((π β π) = πΌ β¨ βπ β (0..^π)(π β π) = (πΊβπ))) |
32 | 31 | ex 414 |
. . . . . . . 8
β’ (π = πΌ β (βπ β (0..^π)π = (πΊβπ) β ((π β π) = πΌ β¨ βπ β (0..^π)(π β π) = (πΊβπ)))) |
33 | 21, 32 | jaod 858 |
. . . . . . 7
β’ (π = πΌ β ((π = πΌ β¨ βπ β (0..^π)π = (πΊβπ)) β ((π β π) = πΌ β¨ βπ β (0..^π)(π β π) = (πΊβπ)))) |
34 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ (((π = πΌ β§ π β (0..^π)) β§ π = (πΊβπ)) β π = (πΊβπ)) |
35 | | simpll 766 |
. . . . . . . . . . . . . . 15
β’ (((π = πΌ β§ π β (0..^π)) β§ π = (πΊβπ)) β π = πΌ) |
36 | 34, 35 | coeq12d 5821 |
. . . . . . . . . . . . . 14
β’ (((π = πΌ β§ π β (0..^π)) β§ π = (πΊβπ)) β (π β π) = ((πΊβπ) β πΌ)) |
37 | 1, 2, 3 | smndex1ibas 18711 |
. . . . . . . . . . . . . . . 16
β’ πΌ β (Baseβπ) |
38 | 1, 2, 3, 4 | smndex1gid 18714 |
. . . . . . . . . . . . . . . 16
β’ ((πΌ β (Baseβπ) β§ π β (0..^π)) β ((πΊβπ) β πΌ) = (πΊβπ)) |
39 | 37, 38 | mpan 689 |
. . . . . . . . . . . . . . 15
β’ (π β (0..^π) β ((πΊβπ) β πΌ) = (πΊβπ)) |
40 | 39 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π = πΌ β§ π β (0..^π)) β§ π = (πΊβπ)) β ((πΊβπ) β πΌ) = (πΊβπ)) |
41 | 36, 40 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π = πΌ β§ π β (0..^π)) β§ π = (πΊβπ)) β (π β π) = (πΊβπ)) |
42 | 41 | ex 414 |
. . . . . . . . . . . 12
β’ ((π = πΌ β§ π β (0..^π)) β (π = (πΊβπ) β (π β π) = (πΊβπ))) |
43 | 42 | reximdva 3166 |
. . . . . . . . . . 11
β’ (π = πΌ β (βπ β (0..^π)π = (πΊβπ) β βπ β (0..^π)(π β π) = (πΊβπ))) |
44 | 43 | imp 408 |
. . . . . . . . . 10
β’ ((π = πΌ β§ βπ β (0..^π)π = (πΊβπ)) β βπ β (0..^π)(π β π) = (πΊβπ)) |
45 | 44 | olcd 873 |
. . . . . . . . 9
β’ ((π = πΌ β§ βπ β (0..^π)π = (πΊβπ)) β ((π β π) = πΌ β¨ βπ β (0..^π)(π β π) = (πΊβπ))) |
46 | 45 | expcom 415 |
. . . . . . . 8
β’
(βπ β
(0..^π)π = (πΊβπ) β (π = πΌ β ((π β π) = πΌ β¨ βπ β (0..^π)(π β π) = (πΊβπ)))) |
47 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π = π β (πΊβπ) = (πΊβπ)) |
48 | 47 | eqeq2d 2748 |
. . . . . . . . . 10
β’ (π = π β (π = (πΊβπ) β π = (πΊβπ))) |
49 | 48 | cbvrexvw 3227 |
. . . . . . . . 9
β’
(βπ β
(0..^π)π = (πΊβπ) β βπ β (0..^π)π = (πΊβπ)) |
50 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β (0..^π) β§ π = (πΊβπ)) β§ π β (0..^π)) β§ π = (πΊβπ)) β π = (πΊβπ)) |
51 | | simpllr 775 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β (0..^π) β§ π = (πΊβπ)) β§ π β (0..^π)) β§ π = (πΊβπ)) β π = (πΊβπ)) |
52 | 50, 51 | coeq12d 5821 |
. . . . . . . . . . . . . . . 16
β’ ((((π β (0..^π) β§ π = (πΊβπ)) β§ π β (0..^π)) β§ π = (πΊβπ)) β (π β π) = ((πΊβπ) β (πΊβπ))) |
53 | 1, 2, 3, 4 | smndex1gbas 18713 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0..^π) β (πΊβπ) β (Baseβπ)) |
54 | 1, 2, 3, 4 | smndex1gid 18714 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΊβπ) β (Baseβπ) β§ π β (0..^π)) β ((πΊβπ) β (πΊβπ)) = (πΊβπ)) |
55 | 53, 54 | sylan 581 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (0..^π) β§ π β (0..^π)) β ((πΊβπ) β (πΊβπ)) = (πΊβπ)) |
56 | 55 | ad4ant13 750 |
. . . . . . . . . . . . . . . 16
β’ ((((π β (0..^π) β§ π = (πΊβπ)) β§ π β (0..^π)) β§ π = (πΊβπ)) β ((πΊβπ) β (πΊβπ)) = (πΊβπ)) |
57 | 52, 56 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ ((((π β (0..^π) β§ π = (πΊβπ)) β§ π β (0..^π)) β§ π = (πΊβπ)) β (π β π) = (πΊβπ)) |
58 | 57 | ex 414 |
. . . . . . . . . . . . . 14
β’ (((π β (0..^π) β§ π = (πΊβπ)) β§ π β (0..^π)) β (π = (πΊβπ) β (π β π) = (πΊβπ))) |
59 | 58 | reximdva 3166 |
. . . . . . . . . . . . 13
β’ ((π β (0..^π) β§ π = (πΊβπ)) β (βπ β (0..^π)π = (πΊβπ) β βπ β (0..^π)(π β π) = (πΊβπ))) |
60 | 59 | rexlimiva 3145 |
. . . . . . . . . . . 12
β’
(βπ β
(0..^π)π = (πΊβπ) β (βπ β (0..^π)π = (πΊβπ) β βπ β (0..^π)(π β π) = (πΊβπ))) |
61 | 60 | imp 408 |
. . . . . . . . . . 11
β’
((βπ β
(0..^π)π = (πΊβπ) β§ βπ β (0..^π)π = (πΊβπ)) β βπ β (0..^π)(π β π) = (πΊβπ)) |
62 | 61 | olcd 873 |
. . . . . . . . . 10
β’
((βπ β
(0..^π)π = (πΊβπ) β§ βπ β (0..^π)π = (πΊβπ)) β ((π β π) = πΌ β¨ βπ β (0..^π)(π β π) = (πΊβπ))) |
63 | 62 | expcom 415 |
. . . . . . . . 9
β’
(βπ β
(0..^π)π = (πΊβπ) β (βπ β (0..^π)π = (πΊβπ) β ((π β π) = πΌ β¨ βπ β (0..^π)(π β π) = (πΊβπ)))) |
64 | 49, 63 | biimtrid 241 |
. . . . . . . 8
β’
(βπ β
(0..^π)π = (πΊβπ) β (βπ β (0..^π)π = (πΊβπ) β ((π β π) = πΌ β¨ βπ β (0..^π)(π β π) = (πΊβπ)))) |
65 | 46, 64 | jaod 858 |
. . . . . . 7
β’
(βπ β
(0..^π)π = (πΊβπ) β ((π = πΌ β¨ βπ β (0..^π)π = (πΊβπ)) β ((π β π) = πΌ β¨ βπ β (0..^π)(π β π) = (πΊβπ)))) |
66 | 33, 65 | jaoi 856 |
. . . . . 6
β’ ((π = πΌ β¨ βπ β (0..^π)π = (πΊβπ)) β ((π = πΌ β¨ βπ β (0..^π)π = (πΊβπ)) β ((π β π) = πΌ β¨ βπ β (0..^π)(π β π) = (πΊβπ)))) |
67 | 66 | imp 408 |
. . . . 5
β’ (((π = πΌ β¨ βπ β (0..^π)π = (πΊβπ)) β§ (π = πΌ β¨ βπ β (0..^π)π = (πΊβπ))) β ((π β π) = πΌ β¨ βπ β (0..^π)(π β π) = (πΊβπ))) |
68 | 5 | eleq2i 2830 |
. . . . . . . 8
β’ (π β π΅ β π β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)})) |
69 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = π β (πΊβπ) = (πΊβπ)) |
70 | 69 | sneqd 4599 |
. . . . . . . . . . 11
β’ (π = π β {(πΊβπ)} = {(πΊβπ)}) |
71 | 70 | cbviunv 5001 |
. . . . . . . . . 10
β’ βͺ π β (0..^π){(πΊβπ)} = βͺ
π β (0..^π){(πΊβπ)} |
72 | 71 | uneq2i 4121 |
. . . . . . . . 9
β’ ({πΌ} βͺ βͺ π β (0..^π){(πΊβπ)}) = ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)}) |
73 | 72 | eleq2i 2830 |
. . . . . . . 8
β’ (π β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)}) β π β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)})) |
74 | 68, 73 | bitri 275 |
. . . . . . 7
β’ (π β π΅ β π β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)})) |
75 | | elun 4109 |
. . . . . . 7
β’ (π β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)}) β (π β {πΌ} β¨ π β βͺ
π β (0..^π){(πΊβπ)})) |
76 | | velsn 4603 |
. . . . . . . 8
β’ (π β {πΌ} β π = πΌ) |
77 | | eliun 4959 |
. . . . . . . . 9
β’ (π β βͺ π β (0..^π){(πΊβπ)} β βπ β (0..^π)π β {(πΊβπ)}) |
78 | | velsn 4603 |
. . . . . . . . . 10
β’ (π β {(πΊβπ)} β π = (πΊβπ)) |
79 | 78 | rexbii 3098 |
. . . . . . . . 9
β’
(βπ β
(0..^π)π β {(πΊβπ)} β βπ β (0..^π)π = (πΊβπ)) |
80 | 77, 79 | bitri 275 |
. . . . . . . 8
β’ (π β βͺ π β (0..^π){(πΊβπ)} β βπ β (0..^π)π = (πΊβπ)) |
81 | 76, 80 | orbi12i 914 |
. . . . . . 7
β’ ((π β {πΌ} β¨ π β βͺ
π β (0..^π){(πΊβπ)}) β (π = πΌ β¨ βπ β (0..^π)π = (πΊβπ))) |
82 | 74, 75, 81 | 3bitri 297 |
. . . . . 6
β’ (π β π΅ β (π = πΌ β¨ βπ β (0..^π)π = (πΊβπ))) |
83 | 5 | eleq2i 2830 |
. . . . . . . 8
β’ (π β π΅ β π β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)})) |
84 | 72 | eleq2i 2830 |
. . . . . . . 8
β’ (π β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)}) β π β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)})) |
85 | 83, 84 | bitri 275 |
. . . . . . 7
β’ (π β π΅ β π β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)})) |
86 | | elun 4109 |
. . . . . . 7
β’ (π β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)}) β (π β {πΌ} β¨ π β βͺ
π β (0..^π){(πΊβπ)})) |
87 | | velsn 4603 |
. . . . . . . 8
β’ (π β {πΌ} β π = πΌ) |
88 | | eliun 4959 |
. . . . . . . . 9
β’ (π β βͺ π β (0..^π){(πΊβπ)} β βπ β (0..^π)π β {(πΊβπ)}) |
89 | | velsn 4603 |
. . . . . . . . . 10
β’ (π β {(πΊβπ)} β π = (πΊβπ)) |
90 | 89 | rexbii 3098 |
. . . . . . . . 9
β’
(βπ β
(0..^π)π β {(πΊβπ)} β βπ β (0..^π)π = (πΊβπ)) |
91 | 88, 90 | bitri 275 |
. . . . . . . 8
β’ (π β βͺ π β (0..^π){(πΊβπ)} β βπ β (0..^π)π = (πΊβπ)) |
92 | 87, 91 | orbi12i 914 |
. . . . . . 7
β’ ((π β {πΌ} β¨ π β βͺ
π β (0..^π){(πΊβπ)}) β (π = πΌ β¨ βπ β (0..^π)π = (πΊβπ))) |
93 | 85, 86, 92 | 3bitri 297 |
. . . . . 6
β’ (π β π΅ β (π = πΌ β¨ βπ β (0..^π)π = (πΊβπ))) |
94 | 82, 93 | anbi12i 628 |
. . . . 5
β’ ((π β π΅ β§ π β π΅) β ((π = πΌ β¨ βπ β (0..^π)π = (πΊβπ)) β§ (π = πΌ β¨ βπ β (0..^π)π = (πΊβπ)))) |
95 | 5 | eleq2i 2830 |
. . . . . . 7
β’ ((π β π) β π΅ β (π β π) β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)})) |
96 | 72 | eleq2i 2830 |
. . . . . . 7
β’ ((π β π) β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)}) β (π β π) β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)})) |
97 | 95, 96 | bitri 275 |
. . . . . 6
β’ ((π β π) β π΅ β (π β π) β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)})) |
98 | | elun 4109 |
. . . . . 6
β’ ((π β π) β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)}) β ((π β π) β {πΌ} β¨ (π β π) β βͺ
π β (0..^π){(πΊβπ)})) |
99 | | vex 3450 |
. . . . . . . . 9
β’ π β V |
100 | | vex 3450 |
. . . . . . . . 9
β’ π β V |
101 | 99, 100 | coex 7868 |
. . . . . . . 8
β’ (π β π) β V |
102 | 101 | elsn 4602 |
. . . . . . 7
β’ ((π β π) β {πΌ} β (π β π) = πΌ) |
103 | | eliun 4959 |
. . . . . . . 8
β’ ((π β π) β βͺ
π β (0..^π){(πΊβπ)} β βπ β (0..^π)(π β π) β {(πΊβπ)}) |
104 | 101 | elsn 4602 |
. . . . . . . . 9
β’ ((π β π) β {(πΊβπ)} β (π β π) = (πΊβπ)) |
105 | 104 | rexbii 3098 |
. . . . . . . 8
β’
(βπ β
(0..^π)(π β π) β {(πΊβπ)} β βπ β (0..^π)(π β π) = (πΊβπ)) |
106 | 103, 105 | bitri 275 |
. . . . . . 7
β’ ((π β π) β βͺ
π β (0..^π){(πΊβπ)} β βπ β (0..^π)(π β π) = (πΊβπ)) |
107 | 102, 106 | orbi12i 914 |
. . . . . 6
β’ (((π β π) β {πΌ} β¨ (π β π) β βͺ
π β (0..^π){(πΊβπ)}) β ((π β π) = πΌ β¨ βπ β (0..^π)(π β π) = (πΊβπ))) |
108 | 97, 98, 107 | 3bitri 297 |
. . . . 5
β’ ((π β π) β π΅ β ((π β π) = πΌ β¨ βπ β (0..^π)(π β π) = (πΊβπ))) |
109 | 67, 94, 108 | 3imtr4i 292 |
. . . 4
β’ ((π β π΅ β§ π β π΅) β (π β π) β π΅) |
110 | 14, 109 | eqeltrd 2838 |
. . 3
β’ ((π β π΅ β§ π β π΅) β (π(+gβπ)π) β π΅) |
111 | 110 | rgen2 3195 |
. 2
β’
βπ β
π΅ βπ β π΅ (π(+gβπ)π) β π΅ |
112 | | smndex1mgm.s |
. . . 4
β’ π = (π βΎs π΅) |
113 | 112 | ovexi 7392 |
. . 3
β’ π β V |
114 | 1, 2, 3, 4, 5, 112 | smndex1bas 18717 |
. . . . 5
β’
(Baseβπ) =
π΅ |
115 | 114 | eqcomi 2746 |
. . . 4
β’ π΅ = (Baseβπ) |
116 | 115 | fvexi 6857 |
. . . . 5
β’ π΅ β V |
117 | 112, 12 | ressplusg 17172 |
. . . . 5
β’ (π΅ β V β
(+gβπ) =
(+gβπ)) |
118 | 116, 117 | ax-mp 5 |
. . . 4
β’
(+gβπ) = (+gβπ) |
119 | 115, 118 | ismgm 18499 |
. . 3
β’ (π β V β (π β Mgm β βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅)) |
120 | 113, 119 | ax-mp 5 |
. 2
β’ (π β Mgm β βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅) |
121 | 111, 120 | mpbir 230 |
1
β’ π β Mgm |