Step | Hyp | Ref
| Expression |
1 | | smndex1ibas.n |
. . . . . . 7
β’ π β β |
2 | | nnnn0 12421 |
. . . . . . . 8
β’ (π β β β π β
β0) |
3 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π₯ = π β (( I βΎ
β0)βπ₯) = (( I βΎ
β0)βπ)) |
4 | 1, 2 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ π β
β0 |
5 | | fvresi 7120 |
. . . . . . . . . . . . 13
β’ (π β β0
β (( I βΎ β0)βπ) = π) |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . . . . 12
β’ (( I
βΎ β0)βπ) = π |
7 | 3, 6 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ (π₯ = π β (( I βΎ
β0)βπ₯) = π) |
8 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π₯ = π β (πΌβπ₯) = (πΌβπ)) |
9 | 7, 8 | eqeq12d 2753 |
. . . . . . . . . 10
β’ (π₯ = π β ((( I βΎ
β0)βπ₯) = (πΌβπ₯) β π = (πΌβπ))) |
10 | 9 | notbid 318 |
. . . . . . . . 9
β’ (π₯ = π β (Β¬ (( I βΎ
β0)βπ₯) = (πΌβπ₯) β Β¬ π = (πΌβπ))) |
11 | 10 | adantl 483 |
. . . . . . . 8
β’ ((π β β β§ π₯ = π) β (Β¬ (( I βΎ
β0)βπ₯) = (πΌβπ₯) β Β¬ π = (πΌβπ))) |
12 | | nnne0 12188 |
. . . . . . . . . 10
β’ (π β β β π β 0) |
13 | 12 | neneqd 2949 |
. . . . . . . . 9
β’ (π β β β Β¬
π = 0) |
14 | | smndex1ibas.i |
. . . . . . . . . . 11
β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) |
15 | | oveq1 7365 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π₯ mod π) = (π mod π)) |
16 | | nnrp 12927 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β+) |
17 | | modid0 13803 |
. . . . . . . . . . . . 13
β’ (π β β+
β (π mod π) = 0) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . 12
β’ (π β β β (π mod π) = 0) |
19 | 15, 18 | sylan9eqr 2799 |
. . . . . . . . . . 11
β’ ((π β β β§ π₯ = π) β (π₯ mod π) = 0) |
20 | | c0ex 11150 |
. . . . . . . . . . . 12
β’ 0 β
V |
21 | 20 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β β 0 β
V) |
22 | 14, 19, 2, 21 | fvmptd2 6957 |
. . . . . . . . . 10
β’ (π β β β (πΌβπ) = 0) |
23 | 22 | eqeq2d 2748 |
. . . . . . . . 9
β’ (π β β β (π = (πΌβπ) β π = 0)) |
24 | 13, 23 | mtbird 325 |
. . . . . . . 8
β’ (π β β β Β¬
π = (πΌβπ)) |
25 | 2, 11, 24 | rspcedvd 3584 |
. . . . . . 7
β’ (π β β β
βπ₯ β
β0 Β¬ (( I βΎ β0)βπ₯) = (πΌβπ₯)) |
26 | 1, 25 | ax-mp 5 |
. . . . . 6
β’
βπ₯ β
β0 Β¬ (( I βΎ β0)βπ₯) = (πΌβπ₯) |
27 | | rexnal 3104 |
. . . . . 6
β’
(βπ₯ β
β0 Β¬ (( I βΎ β0)βπ₯) = (πΌβπ₯) β Β¬ βπ₯ β β0 (( I βΎ
β0)βπ₯) = (πΌβπ₯)) |
28 | 26, 27 | mpbi 229 |
. . . . 5
β’ Β¬
βπ₯ β
β0 (( I βΎ β0)βπ₯) = (πΌβπ₯) |
29 | | fnresi 6631 |
. . . . . 6
β’ ( I
βΎ β0) Fn β0 |
30 | | ovex 7391 |
. . . . . . 7
β’ (π₯ mod π) β V |
31 | 30, 14 | fnmpti 6645 |
. . . . . 6
β’ πΌ Fn
β0 |
32 | | eqfnfv 6983 |
. . . . . 6
β’ ((( I
βΎ β0) Fn β0 β§ πΌ Fn β0) β (( I βΎ
β0) = πΌ
β βπ₯ β
β0 (( I βΎ β0)βπ₯) = (πΌβπ₯))) |
33 | 29, 31, 32 | mp2an 691 |
. . . . 5
β’ (( I
βΎ β0) = πΌ β βπ₯ β β0 (( I βΎ
β0)βπ₯) = (πΌβπ₯)) |
34 | 28, 33 | mtbir 323 |
. . . 4
β’ Β¬ (
I βΎ β0) = πΌ |
35 | 4 | a1i 11 |
. . . . . . . 8
β’ (π β (0..^π) β π β
β0) |
36 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π₯ = π β ((πΊβπ)βπ₯) = ((πΊβπ)βπ)) |
37 | 7, 36 | eqeq12d 2753 |
. . . . . . . . . 10
β’ (π₯ = π β ((( I βΎ
β0)βπ₯) = ((πΊβπ)βπ₯) β π = ((πΊβπ)βπ))) |
38 | 37 | notbid 318 |
. . . . . . . . 9
β’ (π₯ = π β (Β¬ (( I βΎ
β0)βπ₯) = ((πΊβπ)βπ₯) β Β¬ π = ((πΊβπ)βπ))) |
39 | 38 | adantl 483 |
. . . . . . . 8
β’ ((π β (0..^π) β§ π₯ = π) β (Β¬ (( I βΎ
β0)βπ₯) = ((πΊβπ)βπ₯) β Β¬ π = ((πΊβπ)βπ))) |
40 | | fzonel 13587 |
. . . . . . . . . . 11
β’ Β¬
π β (0..^π) |
41 | | eleq1 2826 |
. . . . . . . . . . . 12
β’ (π = π β (π β (0..^π) β π β (0..^π))) |
42 | 41 | eqcoms 2745 |
. . . . . . . . . . 11
β’ (π = π β (π β (0..^π) β π β (0..^π))) |
43 | 40, 42 | mtbiri 327 |
. . . . . . . . . 10
β’ (π = π β Β¬ π β (0..^π)) |
44 | 43 | con2i 139 |
. . . . . . . . 9
β’ (π β (0..^π) β Β¬ π = π) |
45 | | nn0ex 12420 |
. . . . . . . . . . . . 13
β’
β0 β V |
46 | 45 | mptex 7174 |
. . . . . . . . . . . 12
β’ (π₯ β β0
β¦ π) β
V |
47 | | smndex1ibas.g |
. . . . . . . . . . . . 13
β’ πΊ = (π β (0..^π) β¦ (π₯ β β0 β¦ π)) |
48 | 47 | fvmpt2 6960 |
. . . . . . . . . . . 12
β’ ((π β (0..^π) β§ (π₯ β β0 β¦ π) β V) β (πΊβπ) = (π₯ β β0 β¦ π)) |
49 | 46, 48 | mpan2 690 |
. . . . . . . . . . 11
β’ (π β (0..^π) β (πΊβπ) = (π₯ β β0 β¦ π)) |
50 | | eqidd 2738 |
. . . . . . . . . . 11
β’ ((π β (0..^π) β§ π₯ = π) β π = π) |
51 | | id 22 |
. . . . . . . . . . 11
β’ (π β (0..^π) β π β (0..^π)) |
52 | 49, 50, 35, 51 | fvmptd 6956 |
. . . . . . . . . 10
β’ (π β (0..^π) β ((πΊβπ)βπ) = π) |
53 | 52 | eqeq2d 2748 |
. . . . . . . . 9
β’ (π β (0..^π) β (π = ((πΊβπ)βπ) β π = π)) |
54 | 44, 53 | mtbird 325 |
. . . . . . . 8
β’ (π β (0..^π) β Β¬ π = ((πΊβπ)βπ)) |
55 | 35, 39, 54 | rspcedvd 3584 |
. . . . . . 7
β’ (π β (0..^π) β βπ₯ β β0 Β¬ (( I
βΎ β0)βπ₯) = ((πΊβπ)βπ₯)) |
56 | | rexnal 3104 |
. . . . . . 7
β’
(βπ₯ β
β0 Β¬ (( I βΎ β0)βπ₯) = ((πΊβπ)βπ₯) β Β¬ βπ₯ β β0 (( I βΎ
β0)βπ₯) = ((πΊβπ)βπ₯)) |
57 | 55, 56 | sylib 217 |
. . . . . 6
β’ (π β (0..^π) β Β¬ βπ₯ β β0 (( I βΎ
β0)βπ₯) = ((πΊβπ)βπ₯)) |
58 | | vex 3450 |
. . . . . . . . 9
β’ π β V |
59 | | eqid 2737 |
. . . . . . . . 9
β’ (π₯ β β0
β¦ π) = (π₯ β β0
β¦ π) |
60 | 58, 59 | fnmpti 6645 |
. . . . . . . 8
β’ (π₯ β β0
β¦ π) Fn
β0 |
61 | 49 | fneq1d 6596 |
. . . . . . . 8
β’ (π β (0..^π) β ((πΊβπ) Fn β0 β (π₯ β β0
β¦ π) Fn
β0)) |
62 | 60, 61 | mpbiri 258 |
. . . . . . 7
β’ (π β (0..^π) β (πΊβπ) Fn β0) |
63 | | eqfnfv 6983 |
. . . . . . 7
β’ ((( I
βΎ β0) Fn β0 β§ (πΊβπ) Fn β0) β (( I βΎ
β0) = (πΊβπ) β βπ₯ β β0 (( I βΎ
β0)βπ₯) = ((πΊβπ)βπ₯))) |
64 | 29, 62, 63 | sylancr 588 |
. . . . . 6
β’ (π β (0..^π) β (( I βΎ β0) =
(πΊβπ) β βπ₯ β β0 (( I βΎ
β0)βπ₯) = ((πΊβπ)βπ₯))) |
65 | 57, 64 | mtbird 325 |
. . . . 5
β’ (π β (0..^π) β Β¬ ( I βΎ
β0) = (πΊβπ)) |
66 | 65 | nrex 3078 |
. . . 4
β’ Β¬
βπ β (0..^π)( I βΎ
β0) = (πΊβπ) |
67 | 34, 66 | pm3.2ni 880 |
. . 3
β’ Β¬ ((
I βΎ β0) = πΌ β¨ βπ β (0..^π)( I βΎ β0) = (πΊβπ)) |
68 | | smndex1ibas.m |
. . . . . . . 8
β’ π =
(EndoFMndββ0) |
69 | 68 | efmndid 18699 |
. . . . . . 7
β’
(β0 β V β ( I βΎ β0) =
(0gβπ)) |
70 | 45, 69 | ax-mp 5 |
. . . . . 6
β’ ( I
βΎ β0) = (0gβπ) |
71 | 70 | eqcomi 2746 |
. . . . 5
β’
(0gβπ) = ( I βΎ
β0) |
72 | | smndex1mgm.b |
. . . . 5
β’ π΅ = ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)}) |
73 | 71, 72 | eleq12i 2831 |
. . . 4
β’
((0gβπ) β π΅ β ( I βΎ β0)
β ({πΌ} βͺ βͺ π β (0..^π){(πΊβπ)})) |
74 | | elun 4109 |
. . . . 5
β’ (( I
βΎ β0) β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)}) β (( I βΎ β0)
β {πΌ} β¨ ( I βΎ
β0) β βͺ π β (0..^π){(πΊβπ)})) |
75 | | resiexg 7852 |
. . . . . . . 8
β’
(β0 β V β ( I βΎ β0)
β V) |
76 | 45, 75 | ax-mp 5 |
. . . . . . 7
β’ ( I
βΎ β0) β V |
77 | 76 | elsn 4602 |
. . . . . 6
β’ (( I
βΎ β0) β {πΌ} β ( I βΎ β0) =
πΌ) |
78 | | eliun 4959 |
. . . . . . 7
β’ (( I
βΎ β0) β βͺ π β (0..^π){(πΊβπ)} β βπ β (0..^π)( I βΎ β0) β
{(πΊβπ)}) |
79 | 76 | elsn 4602 |
. . . . . . . 8
β’ (( I
βΎ β0) β {(πΊβπ)} β ( I βΎ β0) =
(πΊβπ)) |
80 | 79 | rexbii 3098 |
. . . . . . 7
β’
(βπ β
(0..^π)( I βΎ
β0) β {(πΊβπ)} β βπ β (0..^π)( I βΎ β0) = (πΊβπ)) |
81 | 78, 80 | bitri 275 |
. . . . . 6
β’ (( I
βΎ β0) β βͺ π β (0..^π){(πΊβπ)} β βπ β (0..^π)( I βΎ β0) = (πΊβπ)) |
82 | 77, 81 | orbi12i 914 |
. . . . 5
β’ ((( I
βΎ β0) β {πΌ} β¨ ( I βΎ β0)
β βͺ π β (0..^π){(πΊβπ)}) β (( I βΎ β0)
= πΌ β¨ βπ β (0..^π)( I βΎ β0) = (πΊβπ))) |
83 | 74, 82 | bitri 275 |
. . . 4
β’ (( I
βΎ β0) β ({πΌ} βͺ βͺ
π β (0..^π){(πΊβπ)}) β (( I βΎ β0)
= πΌ β¨ βπ β (0..^π)( I βΎ β0) = (πΊβπ))) |
84 | 73, 83 | bitri 275 |
. . 3
β’
((0gβπ) β π΅ β (( I βΎ β0) =
πΌ β¨ βπ β (0..^π)( I βΎ β0) = (πΊβπ))) |
85 | 67, 84 | mtbir 323 |
. 2
β’ Β¬
(0gβπ)
β π΅ |
86 | 85 | nelir 3053 |
1
β’
(0gβπ) β π΅ |