Step | Hyp | Ref
| Expression |
1 | | df-ne 2945 |
. . 3
β’ ((π· β π) β 0 β Β¬ (π· β π) = 0 ) |
2 | 1 | ralbii 3097 |
. 2
β’
(βπ β
π΅ (π· β π) β 0 β βπ β π΅ Β¬ (π· β π) = 0 ) |
3 | | smndex2dbas.m |
. . . 4
β’ π =
(EndoFMndββ0) |
4 | | smndex2dbas.b |
. . . 4
β’ π΅ = (Baseβπ) |
5 | 3, 4 | efmndbasf 18686 |
. . 3
β’ (π β π΅ β π:β0βΆβ0) |
6 | | 1nn0 12430 |
. . . . . . . . . . 11
β’ 1 β
β0 |
7 | | nn0z 12525 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β β0
β π₯ β
β€) |
8 | | 0zd 12512 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β β0
β 0 β β€) |
9 | | zneo 12587 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β€ β§ 0 β
β€) β (2 Β· π₯) β ((2 Β· 0) + 1)) |
10 | 7, 8, 9 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β0
β (2 Β· π₯) β
((2 Β· 0) + 1)) |
11 | | 2t0e0 12323 |
. . . . . . . . . . . . . . . . . . 19
β’ (2
Β· 0) = 0 |
12 | 11 | oveq1i 7368 |
. . . . . . . . . . . . . . . . . 18
β’ ((2
Β· 0) + 1) = (0 + 1) |
13 | | 0p1e1 12276 |
. . . . . . . . . . . . . . . . . 18
β’ (0 + 1) =
1 |
14 | 12, 13 | eqtri 2765 |
. . . . . . . . . . . . . . . . 17
β’ ((2
Β· 0) + 1) = 1 |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β0
β ((2 Β· 0) + 1) = 1) |
16 | 10, 15 | neeqtrd 3014 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β0
β (2 Β· π₯) β
1) |
17 | 16 | necomd 3000 |
. . . . . . . . . . . . . 14
β’ (π₯ β β0
β 1 β (2 Β· π₯)) |
18 | 17 | neneqd 2949 |
. . . . . . . . . . . . 13
β’ (π₯ β β0
β Β¬ 1 = (2 Β· π₯)) |
19 | 18 | nrex 3078 |
. . . . . . . . . . . 12
β’ Β¬
βπ₯ β
β0 1 = (2 Β· π₯) |
20 | | 1ex 11152 |
. . . . . . . . . . . . 13
β’ 1 β
V |
21 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
β’ (π¦ = 1 β (π¦ = (2 Β· π₯) β 1 = (2 Β· π₯))) |
22 | 21 | rexbidv 3176 |
. . . . . . . . . . . . 13
β’ (π¦ = 1 β (βπ₯ β β0
π¦ = (2 Β· π₯) β βπ₯ β β0 1 =
(2 Β· π₯))) |
23 | 20, 22 | elab 3631 |
. . . . . . . . . . . 12
β’ (1 β
{π¦ β£ βπ₯ β β0
π¦ = (2 Β· π₯)} β βπ₯ β β0 1 =
(2 Β· π₯)) |
24 | 19, 23 | mtbir 323 |
. . . . . . . . . . 11
β’ Β¬ 1
β {π¦ β£
βπ₯ β
β0 π¦ = (2
Β· π₯)} |
25 | | nelss 4008 |
. . . . . . . . . . 11
β’ ((1
β β0 β§ Β¬ 1 β {π¦ β£ βπ₯ β β0 π¦ = (2 Β· π₯)}) β Β¬
β0 β {π¦ β£ βπ₯ β β0 π¦ = (2 Β· π₯)}) |
26 | 6, 24, 25 | mp2an 691 |
. . . . . . . . . 10
β’ Β¬
β0 β {π¦ β£ βπ₯ β β0 π¦ = (2 Β· π₯)} |
27 | 26 | intnan 488 |
. . . . . . . . 9
β’ Β¬
({π¦ β£ βπ₯ β β0
π¦ = (2 Β· π₯)} β β0
β§ β0 β {π¦ β£ βπ₯ β β0 π¦ = (2 Β· π₯)}) |
28 | | eqss 3960 |
. . . . . . . . 9
β’ ({π¦ β£ βπ₯ β β0
π¦ = (2 Β· π₯)} = β0 β
({π¦ β£ βπ₯ β β0
π¦ = (2 Β· π₯)} β β0
β§ β0 β {π¦ β£ βπ₯ β β0 π¦ = (2 Β· π₯)})) |
29 | 27, 28 | mtbir 323 |
. . . . . . . 8
β’ Β¬
{π¦ β£ βπ₯ β β0
π¦ = (2 Β· π₯)} =
β0 |
30 | | smndex2dbas.d |
. . . . . . . . . 10
β’ π· = (π₯ β β0 β¦ (2
Β· π₯)) |
31 | 30 | rnmpt 5911 |
. . . . . . . . 9
β’ ran π· = {π¦ β£ βπ₯ β β0 π¦ = (2 Β· π₯)} |
32 | 31 | eqeq1i 2742 |
. . . . . . . 8
β’ (ran
π· = β0
β {π¦ β£
βπ₯ β
β0 π¦ = (2
Β· π₯)} =
β0) |
33 | 29, 32 | mtbir 323 |
. . . . . . 7
β’ Β¬
ran π· =
β0 |
34 | 33 | olci 865 |
. . . . . 6
β’ (Β¬
π· Fn β0
β¨ Β¬ ran π· =
β0) |
35 | | ianor 981 |
. . . . . . 7
β’ (Β¬
(π· Fn β0
β§ ran π· =
β0) β (Β¬ π· Fn β0 β¨ Β¬ ran π· =
β0)) |
36 | | df-fo 6503 |
. . . . . . 7
β’ (π·:β0βontoββ0 β (π· Fn β0 β§
ran π· =
β0)) |
37 | 35, 36 | xchnxbir 333 |
. . . . . 6
β’ (Β¬
π·:β0βontoββ0 β (Β¬ π· Fn β0 β¨
Β¬ ran π· =
β0)) |
38 | 34, 37 | mpbir 230 |
. . . . 5
β’ Β¬
π·:β0βontoββ0 |
39 | 38 | a1i 11 |
. . . 4
β’ (π:β0βΆβ0
β Β¬ π·:β0βontoββ0) |
40 | | smndex2dbas.0 |
. . . . . 6
β’ 0 =
(0gβπ) |
41 | 3, 4, 40, 30 | smndex2dbas 18725 |
. . . . 5
β’ π· β π΅ |
42 | 3, 4 | efmndbasf 18686 |
. . . . 5
β’ (π· β π΅ β π·:β0βΆβ0) |
43 | | simpl 484 |
. . . . . . 7
β’ ((π·:β0βΆβ0
β§ (π:β0βΆβ0
β§ (π· β π) = 0 )) β π·:β0βΆβ0) |
44 | | simpl 484 |
. . . . . . . 8
β’ ((π:β0βΆβ0
β§ (π· β π) = 0 ) β π:β0βΆβ0) |
45 | 44 | adantl 483 |
. . . . . . 7
β’ ((π·:β0βΆβ0
β§ (π:β0βΆβ0
β§ (π· β π) = 0 )) β π:β0βΆβ0) |
46 | | nn0ex 12420 |
. . . . . . . . . . . . 13
β’
β0 β V |
47 | 3 | efmndid 18699 |
. . . . . . . . . . . . 13
β’
(β0 β V β ( I βΎ β0) =
(0gβπ)) |
48 | 46, 47 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ( I
βΎ β0) = (0gβπ) |
49 | 40, 48 | eqtr4i 2768 |
. . . . . . . . . . 11
β’ 0 = ( I βΎ
β0) |
50 | 49 | eqeq2i 2750 |
. . . . . . . . . 10
β’ ((π· β π) = 0 β (π· β π) = ( I βΎ
β0)) |
51 | 50 | biimpi 215 |
. . . . . . . . 9
β’ ((π· β π) = 0 β (π· β π) = ( I βΎ
β0)) |
52 | 51 | adantl 483 |
. . . . . . . 8
β’ ((π:β0βΆβ0
β§ (π· β π) = 0 ) β (π· β π) = ( I βΎ
β0)) |
53 | 52 | adantl 483 |
. . . . . . 7
β’ ((π·:β0βΆβ0
β§ (π:β0βΆβ0
β§ (π· β π) = 0 )) β (π· β π) = ( I βΎ
β0)) |
54 | | fcofo 7235 |
. . . . . . 7
β’ ((π·:β0βΆβ0
β§ π:β0βΆβ0
β§ (π· β π) = ( I βΎ
β0)) β π·:β0βontoββ0) |
55 | 43, 45, 53, 54 | syl3anc 1372 |
. . . . . 6
β’ ((π·:β0βΆβ0
β§ (π:β0βΆβ0
β§ (π· β π) = 0 )) β π·:β0βontoββ0) |
56 | 55 | ex 414 |
. . . . 5
β’ (π·:β0βΆβ0
β ((π:β0βΆβ0
β§ (π· β π) = 0 ) β π·:β0βontoββ0)) |
57 | 41, 42, 56 | mp2b 10 |
. . . 4
β’ ((π:β0βΆβ0
β§ (π· β π) = 0 ) β π·:β0βontoββ0) |
58 | 39, 57 | mtand 815 |
. . 3
β’ (π:β0βΆβ0
β Β¬ (π· β π) = 0 ) |
59 | 5, 58 | syl 17 |
. 2
β’ (π β π΅ β Β¬ (π· β π) = 0 ) |
60 | 2, 59 | mprgbir 3072 |
1
β’
βπ β
π΅ (π· β π) β 0 |