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 18719 |
. 2
β’ π β Smgrp |
8 | | nn0ex 12420 |
. . . . . . . . 9
β’
β0 β V |
9 | 8 | mptex 7174 |
. . . . . . . 8
β’ (π₯ β β0
β¦ (π₯ mod π)) β V |
10 | 3, 9 | eqeltri 2834 |
. . . . . . 7
β’ πΌ β V |
11 | 10 | snid 4623 |
. . . . . 6
β’ πΌ β {πΌ} |
12 | | elun1 4137 |
. . . . . 6
β’ (πΌ β {πΌ} β πΌ β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)})) |
13 | 11, 12 | ax-mp 5 |
. . . . 5
β’ πΌ β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)}) |
14 | 13, 5 | eleqtrri 2837 |
. . . 4
β’ πΌ β π΅ |
15 | | id 22 |
. . . . 5
β’ (πΌ β π΅ β πΌ β π΅) |
16 | | coeq1 5814 |
. . . . . . . . 9
β’ (π = πΌ β (π β π) = (πΌ β π)) |
17 | 16 | eqeq1d 2739 |
. . . . . . . 8
β’ (π = πΌ β ((π β π) = π β (πΌ β π) = π)) |
18 | | coeq2 5815 |
. . . . . . . . 9
β’ (π = πΌ β (π β π) = (π β πΌ)) |
19 | 18 | eqeq1d 2739 |
. . . . . . . 8
β’ (π = πΌ β ((π β π) = π β (π β πΌ) = π)) |
20 | 17, 19 | anbi12d 632 |
. . . . . . 7
β’ (π = πΌ β (((π β π) = π β§ (π β π) = π) β ((πΌ β π) = π β§ (π β πΌ) = π))) |
21 | 20 | ralbidv 3175 |
. . . . . 6
β’ (π = πΌ β (βπ β π΅ ((π β π) = π β§ (π β π) = π) β βπ β π΅ ((πΌ β π) = π β§ (π β πΌ) = π))) |
22 | 21 | adantl 483 |
. . . . 5
β’ ((πΌ β π΅ β§ π = πΌ) β (βπ β π΅ ((π β π) = π β§ (π β π) = π) β βπ β π΅ ((πΌ β π) = π β§ (π β πΌ) = π))) |
23 | 1, 2, 3, 4, 5, 6 | smndex1mndlem 18720 |
. . . . . . 7
β’ (π β π΅ β ((πΌ β π) = π β§ (π β πΌ) = π)) |
24 | 23 | rgen 3067 |
. . . . . 6
β’
βπ β
π΅ ((πΌ β π) = π β§ (π β πΌ) = π) |
25 | 24 | a1i 11 |
. . . . 5
β’ (πΌ β π΅ β βπ β π΅ ((πΌ β π) = π β§ (π β πΌ) = π)) |
26 | 15, 22, 25 | rspcedvd 3584 |
. . . 4
β’ (πΌ β π΅ β βπ β π΅ βπ β π΅ ((π β π) = π β§ (π β π) = π)) |
27 | 14, 26 | ax-mp 5 |
. . 3
β’
βπ β
π΅ βπ β π΅ ((π β π) = π β§ (π β π) = π) |
28 | 1, 2, 3, 4, 5 | smndex1basss 18716 |
. . . . . . 7
β’ π΅ β (Baseβπ) |
29 | | ssel 3938 |
. . . . . . . 8
β’ (π΅ β (Baseβπ) β (π β π΅ β π β (Baseβπ))) |
30 | | ssel 3938 |
. . . . . . . 8
β’ (π΅ β (Baseβπ) β (π β π΅ β π β (Baseβπ))) |
31 | 29, 30 | anim12d 610 |
. . . . . . 7
β’ (π΅ β (Baseβπ) β ((π β π΅ β§ π β π΅) β (π β (Baseβπ) β§ π β (Baseβπ)))) |
32 | 28, 31 | ax-mp 5 |
. . . . . 6
β’ ((π β π΅ β§ π β π΅) β (π β (Baseβπ) β§ π β (Baseβπ))) |
33 | | eqid 2737 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
34 | | snex 5389 |
. . . . . . . . . . . . 13
β’ {πΌ} β V |
35 | | ovex 7391 |
. . . . . . . . . . . . . 14
β’
(0..^π) β
V |
36 | | snex 5389 |
. . . . . . . . . . . . . 14
β’ {(πΊβπ)} β V |
37 | 35, 36 | iunex 7902 |
. . . . . . . . . . . . 13
β’ βͺ π β (0..^π){(πΊβπ)} β V |
38 | 34, 37 | unex 7681 |
. . . . . . . . . . . 12
β’ ({πΌ} βͺ βͺ π β (0..^π){(πΊβπ)}) β V |
39 | 5, 38 | eqeltri 2834 |
. . . . . . . . . . 11
β’ π΅ β V |
40 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(+gβπ) = (+gβπ) |
41 | 6, 40 | ressplusg 17172 |
. . . . . . . . . . 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 18692 |
. . . . . . . 8
β’ ((π β (Baseβπ) β§ π β (Baseβπ)) β (π(+gβπ)π) = (π β π)) |
45 | 44 | eqeq1d 2739 |
. . . . . . 7
β’ ((π β (Baseβπ) β§ π β (Baseβπ)) β ((π(+gβπ)π) = π β (π β π) = π)) |
46 | 43 | oveqi 7371 |
. . . . . . . . 9
β’ (π(+gβπ)π) = (π(+gβπ)π) |
47 | 1, 33, 40 | efmndov 18692 |
. . . . . . . . . 10
β’ ((π β (Baseβπ) β§ π β (Baseβπ)) β (π(+gβπ)π) = (π β π)) |
48 | 47 | ancoms 460 |
. . . . . . . . 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 3173 |
. . . 4
β’ (π β π΅ β (βπ β π΅ ((π(+gβπ)π) = π β§ (π(+gβπ)π) = π) β βπ β π΅ ((π β π) = π β§ (π β π) = π))) |
54 | 53 | rexbiia 3096 |
. . 3
β’
(βπ β
π΅ βπ β π΅ ((π(+gβπ)π) = π β§ (π(+gβπ)π) = π) β βπ β π΅ βπ β π΅ ((π β π) = π β§ (π β π) = π)) |
55 | 27, 54 | mpbir 230 |
. 2
β’
βπ β
π΅ βπ β π΅ ((π(+gβπ)π) = π β§ (π(+gβπ)π) = π) |
56 | 1, 2, 3, 4, 5, 6 | smndex1bas 18717 |
. . . 4
β’
(Baseβπ) =
π΅ |
57 | 56 | eqcomi 2746 |
. . 3
β’ π΅ = (Baseβπ) |
58 | | eqid 2737 |
. . 3
β’
(+gβπ) = (+gβπ) |
59 | 57, 58 | ismnddef 18559 |
. 2
β’ (π β Mnd β (π β Smgrp β§ βπ β π΅ βπ β π΅ ((π(+gβπ)π) = π β§ (π(+gβπ)π) = π))) |
60 | 7, 55, 59 | mpbir2an 710 |
1
β’ π β Mnd |