Step | Hyp | Ref
| Expression |
1 | | zex 12515 |
. . . . . 6
β’ β€
β V |
2 | | difexg 5289 |
. . . . . 6
β’ (β€
β V β (β€ β β) β V) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
β’ (β€
β β) β V |
4 | | ominf 9209 |
. . . . . 6
β’ Β¬
Ο β Fin |
5 | | nnuz 12813 |
. . . . . . . . . 10
β’ β =
(β€β₯β1) |
6 | | 0p1e1 12282 |
. . . . . . . . . . 11
β’ (0 + 1) =
1 |
7 | 6 | fveq2i 6850 |
. . . . . . . . . 10
β’
(β€β₯β(0 + 1)) =
(β€β₯β1) |
8 | 5, 7 | eqtr4i 2768 |
. . . . . . . . 9
β’ β =
(β€β₯β(0 + 1)) |
9 | 8 | difeq2i 4084 |
. . . . . . . 8
β’ (β€
β β) = (β€ β (β€β₯β(0 +
1))) |
10 | | 0z 12517 |
. . . . . . . . 9
β’ 0 β
β€ |
11 | | lzenom 41122 |
. . . . . . . . 9
β’ (0 β
β€ β (β€ β (β€β₯β(0 + 1))) β
Ο) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . 8
β’ (β€
β (β€β₯β(0 + 1))) β
Ο |
13 | 9, 12 | eqbrtri 5131 |
. . . . . . 7
β’ (β€
β β) β Ο |
14 | | enfi 9141 |
. . . . . . 7
β’ ((β€
β β) β Ο β ((β€ β β) β Fin
β Ο β Fin)) |
15 | 13, 14 | ax-mp 5 |
. . . . . 6
β’ ((β€
β β) β Fin β Ο β Fin) |
16 | 4, 15 | mtbir 323 |
. . . . 5
β’ Β¬
(β€ β β) β Fin |
17 | | disjdifr 4437 |
. . . . 5
β’ ((β€
β β) β© β) = β
|
18 | 3, 16, 17 | eldioph4b 41163 |
. . . 4
β’ (π β (Diophβπ) β (π β β0 β§
βπ β
(mzPolyβ((β€ β β) βͺ (1...π)))π = {π β (β0
βm (1...π))
β£ βπ β
(β0 βm (β€ β β))(πβ(π βͺ π)) = 0})) |
19 | | simpr 486 |
. . . . . . . . . . . 12
β’
(((((π β
β0 β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β§ π β (β0
βm (1...π))) β π β (β0
βm (1...π))) |
20 | | simp-4r 783 |
. . . . . . . . . . . 12
β’
(((((π β
β0 β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β§ π β (β0
βm (1...π))) β πΉ:(1...π)βΆ(1...π)) |
21 | | ovex 7395 |
. . . . . . . . . . . . 13
β’
(1...π) β
V |
22 | 21 | mapco2 41067 |
. . . . . . . . . . . 12
β’ ((π β (β0
βm (1...π))
β§ πΉ:(1...π)βΆ(1...π)) β (π β πΉ) β (β0
βm (1...π))) |
23 | 19, 20, 22 | syl2anc 585 |
. . . . . . . . . . 11
β’
(((((π β
β0 β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β§ π β (β0
βm (1...π))) β (π β πΉ) β (β0
βm (1...π))) |
24 | | uneq1 4121 |
. . . . . . . . . . . . . 14
β’ (π = (π β πΉ) β (π βͺ π) = ((π β πΉ) βͺ π)) |
25 | 24 | fveqeq2d 6855 |
. . . . . . . . . . . . 13
β’ (π = (π β πΉ) β ((πβ(π βͺ π)) = 0 β (πβ((π β πΉ) βͺ π)) = 0)) |
26 | 25 | rexbidv 3176 |
. . . . . . . . . . . 12
β’ (π = (π β πΉ) β (βπ β (β0
βm (β€ β β))(πβ(π βͺ π)) = 0 β βπ β (β0
βm (β€ β β))(πβ((π β πΉ) βͺ π)) = 0)) |
27 | 26 | elrab3 3651 |
. . . . . . . . . . 11
β’ ((π β πΉ) β (β0
βm (1...π))
β ((π β πΉ) β {π β (β0
βm (1...π))
β£ βπ β
(β0 βm (β€ β β))(πβ(π βͺ π)) = 0} β βπ β (β0
βm (β€ β β))(πβ((π β πΉ) βͺ π)) = 0)) |
28 | 23, 27 | syl 17 |
. . . . . . . . . 10
β’
(((((π β
β0 β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β§ π β (β0
βm (1...π))) β ((π β πΉ) β {π β (β0
βm (1...π))
β£ βπ β
(β0 βm (β€ β β))(πβ(π βͺ π)) = 0} β βπ β (β0
βm (β€ β β))(πβ((π β πΉ) βͺ π)) = 0)) |
29 | | simp-5r 785 |
. . . . . . . . . . . . . . 15
β’
((((((π β
β0 β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β§ π β (β0
βm (1...π))) β§ π β (β0
βm (β€ β β))) β πΉ:(1...π)βΆ(1...π)) |
30 | | simplr 768 |
. . . . . . . . . . . . . . 15
β’
((((((π β
β0 β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β§ π β (β0
βm (1...π))) β§ π β (β0
βm (β€ β β))) β π β (β0
βm (1...π))) |
31 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’
((((((π β
β0 β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β§ π β (β0
βm (1...π))) β§ π β (β0
βm (β€ β β))) β π β (β0
βm (β€ β β))) |
32 | | coundi 6204 |
. . . . . . . . . . . . . . . 16
β’ ((π βͺ π) β (πΉ βͺ ( I βΎ (β€ β
β)))) = (((π βͺ
π) β πΉ) βͺ ((π βͺ π) β ( I βΎ (β€ β
β)))) |
33 | | coundir 6205 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π βͺ π) β πΉ) = ((π β πΉ) βͺ (π β πΉ)) |
34 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (β0
βm (β€ β β)) β π:(β€ β
β)βΆβ0) |
35 | 34 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉ:(1...π)βΆ(1...π) β§ π β (β0
βm (1...π))
β§ π β
(β0 βm (β€ β β))) β
π:(β€ β
β)βΆβ0) |
36 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉ:(1...π)βΆ(1...π) β§ π β (β0
βm (1...π))
β§ π β
(β0 βm (β€ β β))) β
πΉ:(1...π)βΆ(1...π)) |
37 | | incom 4166 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((β€
β β) β© (1...π)) = ((1...π) β© (β€ β
β)) |
38 | | fz1ssnn 13479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(1...π) β
β |
39 | | disjdif 4436 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (β
β© (β€ β β)) = β
|
40 | | ssdisj 4424 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((1...π) β
β β§ (β β© (β€ β β)) = β
) β
((1...π) β© (β€
β β)) = β
) |
41 | 38, 39, 40 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((1...π) β©
(β€ β β)) = β
|
42 | 37, 41 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((β€
β β) β© (1...π)) = β
|
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉ:(1...π)βΆ(1...π) β§ π β (β0
βm (1...π))
β§ π β
(β0 βm (β€ β β))) β
((β€ β β) β© (1...π)) = β
) |
44 | | coeq0i 41105 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π:(β€ β
β)βΆβ0 β§ πΉ:(1...π)βΆ(1...π) β§ ((β€ β β) β©
(1...π)) = β
) β
(π β πΉ) = β
) |
45 | 35, 36, 43, 44 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉ:(1...π)βΆ(1...π) β§ π β (β0
βm (1...π))
β§ π β
(β0 βm (β€ β β))) β
(π β πΉ) = β
) |
46 | 45 | uneq2d 4128 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ:(1...π)βΆ(1...π) β§ π β (β0
βm (1...π))
β§ π β
(β0 βm (β€ β β))) β
((π β πΉ) βͺ (π β πΉ)) = ((π β πΉ) βͺ β
)) |
47 | 33, 46 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ:(1...π)βΆ(1...π) β§ π β (β0
βm (1...π))
β§ π β
(β0 βm (β€ β β))) β
((π βͺ π) β πΉ) = ((π β πΉ) βͺ β
)) |
48 | | un0 4355 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β πΉ) βͺ β
) = (π β πΉ) |
49 | 47, 48 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ:(1...π)βΆ(1...π) β§ π β (β0
βm (1...π))
β§ π β
(β0 βm (β€ β β))) β
((π βͺ π) β πΉ) = (π β πΉ)) |
50 | | coundir 6205 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π βͺ π) β ( I βΎ (β€ β
β))) = ((π β (
I βΎ (β€ β β))) βͺ (π β ( I βΎ (β€ β
β)))) |
51 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (β0
βm (1...π))
β π:(1...π)βΆβ0) |
52 | 51 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉ:(1...π)βΆ(1...π) β§ π β (β0
βm (1...π))
β§ π β
(β0 βm (β€ β β))) β
π:(1...π)βΆβ0) |
53 | | f1oi 6827 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ( I
βΎ (β€ β β)):(β€ β β)β1-1-ontoβ(β€ β β) |
54 | | f1of 6789 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (( I
βΎ (β€ β β)):(β€ β β)β1-1-ontoβ(β€ β β) β ( I βΎ
(β€ β β)):(β€ β β)βΆ(β€ β
β)) |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ( I
βΎ (β€ β β)):(β€ β β)βΆ(β€
β β) |
56 | | coeq0i 41105 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π:(1...π)βΆβ0 β§ ( I
βΎ (β€ β β)):(β€ β β)βΆ(β€
β β) β§ ((1...π) β© (β€ β β)) =
β
) β (π β
( I βΎ (β€ β β))) = β
) |
57 | 55, 41, 56 | mp3an23 1454 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π:(1...π)βΆβ0 β (π β ( I βΎ (β€
β β))) = β
) |
58 | 52, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉ:(1...π)βΆ(1...π) β§ π β (β0
βm (1...π))
β§ π β
(β0 βm (β€ β β))) β
(π β ( I βΎ
(β€ β β))) = β
) |
59 | | coires1 6221 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ( I βΎ (β€
β β))) = (π
βΎ (β€ β β)) |
60 | | ffn 6673 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π:(β€ β
β)βΆβ0 β π Fn (β€ β
β)) |
61 | | fnresdm 6625 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π Fn (β€ β β)
β (π βΎ (β€
β β)) = π) |
62 | 34, 60, 61 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (β0
βm (β€ β β)) β (π βΎ (β€ β β)) = π) |
63 | 59, 62 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (β0
βm (β€ β β)) β (π β ( I βΎ (β€ β
β))) = π) |
64 | 63 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉ:(1...π)βΆ(1...π) β§ π β (β0
βm (1...π))
β§ π β
(β0 βm (β€ β β))) β
(π β ( I βΎ
(β€ β β))) = π) |
65 | 58, 64 | uneq12d 4129 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ:(1...π)βΆ(1...π) β§ π β (β0
βm (1...π))
β§ π β
(β0 βm (β€ β β))) β
((π β ( I βΎ
(β€ β β))) βͺ (π β ( I βΎ (β€ β
β)))) = (β
βͺ π)) |
66 | 50, 65 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ:(1...π)βΆ(1...π) β§ π β (β0
βm (1...π))
β§ π β
(β0 βm (β€ β β))) β
((π βͺ π) β ( I βΎ (β€
β β))) = (β
βͺ π)) |
67 | | uncom 4118 |
. . . . . . . . . . . . . . . . . . 19
β’ (β
βͺ π) = (π βͺ β
) |
68 | | un0 4355 |
. . . . . . . . . . . . . . . . . . 19
β’ (π βͺ β
) = π |
69 | 67, 68 | eqtri 2765 |
. . . . . . . . . . . . . . . . . 18
β’ (β
βͺ π) = π |
70 | 66, 69 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ:(1...π)βΆ(1...π) β§ π β (β0
βm (1...π))
β§ π β
(β0 βm (β€ β β))) β
((π βͺ π) β ( I βΎ (β€
β β))) = π) |
71 | 49, 70 | uneq12d 4129 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ:(1...π)βΆ(1...π) β§ π β (β0
βm (1...π))
β§ π β
(β0 βm (β€ β β))) β
(((π βͺ π) β πΉ) βͺ ((π βͺ π) β ( I βΎ (β€ β
β)))) = ((π β
πΉ) βͺ π)) |
72 | 32, 71 | eqtr2id 2790 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:(1...π)βΆ(1...π) β§ π β (β0
βm (1...π))
β§ π β
(β0 βm (β€ β β))) β
((π β πΉ) βͺ π) = ((π βͺ π) β (πΉ βͺ ( I βΎ (β€ β
β))))) |
73 | 29, 30, 31, 72 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’
((((((π β
β0 β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β§ π β (β0
βm (1...π))) β§ π β (β0
βm (β€ β β))) β ((π β πΉ) βͺ π) = ((π βͺ π) β (πΉ βͺ ( I βΎ (β€ β
β))))) |
74 | 73 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’
((((((π β
β0 β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β§ π β (β0
βm (1...π))) β§ π β (β0
βm (β€ β β))) β (πβ((π β πΉ) βͺ π)) = (πβ((π βͺ π) β (πΉ βͺ ( I βΎ (β€ β
β)))))) |
75 | | nn0ssz 12529 |
. . . . . . . . . . . . . . . . 17
β’
β0 β β€ |
76 | | mapss 8834 |
. . . . . . . . . . . . . . . . 17
β’ ((β€
β V β§ β0 β β€) β (β0
βm ((β€ β β) βͺ (1...π))) β (β€ βm
((β€ β β) βͺ (1...π)))) |
77 | 1, 75, 76 | mp2an 691 |
. . . . . . . . . . . . . . . 16
β’
(β0 βm ((β€ β β) βͺ
(1...π))) β (β€
βm ((β€ β β) βͺ (1...π))) |
78 | 41 | reseq2i 5939 |
. . . . . . . . . . . . . . . . . . 19
β’ (π βΎ ((1...π) β© (β€ β β))) = (π βΎ
β
) |
79 | | res0 5946 |
. . . . . . . . . . . . . . . . . . 19
β’ (π βΎ β
) =
β
|
80 | 78, 79 | eqtri 2765 |
. . . . . . . . . . . . . . . . . 18
β’ (π βΎ ((1...π) β© (β€ β β))) =
β
|
81 | 41 | reseq2i 5939 |
. . . . . . . . . . . . . . . . . . 19
β’ (π βΎ ((1...π) β© (β€ β β))) = (π βΎ
β
) |
82 | | res0 5946 |
. . . . . . . . . . . . . . . . . . 19
β’ (π βΎ β
) =
β
|
83 | 81, 82 | eqtri 2765 |
. . . . . . . . . . . . . . . . . 18
β’ (π βΎ ((1...π) β© (β€ β β))) =
β
|
84 | 80, 83 | eqtr4i 2768 |
. . . . . . . . . . . . . . . . 17
β’ (π βΎ ((1...π) β© (β€ β β))) = (π βΎ ((1...π) β© (β€ β
β))) |
85 | | elmapresaun 8825 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (β0
βm (1...π))
β§ π β
(β0 βm (β€ β β)) β§ (π βΎ ((1...π) β© (β€ β β))) = (π βΎ ((1...π) β© (β€ β β)))) β
(π βͺ π) β (β0
βm ((1...π)
βͺ (β€ β β)))) |
86 | | uncom 4118 |
. . . . . . . . . . . . . . . . . . 19
β’
((1...π) βͺ
(β€ β β)) = ((β€ β β) βͺ (1...π)) |
87 | 86 | oveq2i 7373 |
. . . . . . . . . . . . . . . . . 18
β’
(β0 βm ((1...π) βͺ (β€ β β))) =
(β0 βm ((β€ β β) βͺ
(1...π))) |
88 | 85, 87 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (β0
βm (1...π))
β§ π β
(β0 βm (β€ β β)) β§ (π βΎ ((1...π) β© (β€ β β))) = (π βΎ ((1...π) β© (β€ β β)))) β
(π βͺ π) β (β0
βm ((β€ β β) βͺ (1...π)))) |
89 | 84, 88 | mp3an3 1451 |
. . . . . . . . . . . . . . . 16
β’ ((π β (β0
βm (1...π))
β§ π β
(β0 βm (β€ β β))) β
(π βͺ π) β (β0
βm ((β€ β β) βͺ (1...π)))) |
90 | 77, 89 | sselid 3947 |
. . . . . . . . . . . . . . 15
β’ ((π β (β0
βm (1...π))
β§ π β
(β0 βm (β€ β β))) β
(π βͺ π) β (β€ βm
((β€ β β) βͺ (1...π)))) |
91 | 90 | adantll 713 |
. . . . . . . . . . . . . 14
β’
((((((π β
β0 β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β§ π β (β0
βm (1...π))) β§ π β (β0
βm (β€ β β))) β (π βͺ π) β (β€ βm
((β€ β β) βͺ (1...π)))) |
92 | | coeq1 5818 |
. . . . . . . . . . . . . . . 16
β’ (π = (π βͺ π) β (π β (πΉ βͺ ( I βΎ (β€ β
β)))) = ((π βͺ
π) β (πΉ βͺ ( I βΎ (β€
β β))))) |
93 | 92 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
β’ (π = (π βͺ π) β (πβ(π β (πΉ βͺ ( I βΎ (β€ β
β))))) = (πβ((π βͺ π) β (πΉ βͺ ( I βΎ (β€ β
β)))))) |
94 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’ (π β (β€
βm ((β€ β β) βͺ (1...π))) β¦ (πβ(π β (πΉ βͺ ( I βΎ (β€ β
β)))))) = (π β
(β€ βm ((β€ β β) βͺ (1...π))) β¦ (πβ(π β (πΉ βͺ ( I βΎ (β€ β
β)))))) |
95 | | fvex 6860 |
. . . . . . . . . . . . . . 15
β’ (πβ((π βͺ π) β (πΉ βͺ ( I βΎ (β€ β
β))))) β V |
96 | 93, 94, 95 | fvmpt 6953 |
. . . . . . . . . . . . . 14
β’ ((π βͺ π) β (β€ βm
((β€ β β) βͺ (1...π))) β ((π β (β€ βm ((β€
β β) βͺ (1...π))) β¦ (πβ(π β (πΉ βͺ ( I βΎ (β€ β
β))))))β(π
βͺ π)) = (πβ((π βͺ π) β (πΉ βͺ ( I βΎ (β€ β
β)))))) |
97 | 91, 96 | syl 17 |
. . . . . . . . . . . . 13
β’
((((((π β
β0 β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β§ π β (β0
βm (1...π))) β§ π β (β0
βm (β€ β β))) β ((π β (β€ βm ((β€
β β) βͺ (1...π))) β¦ (πβ(π β (πΉ βͺ ( I βΎ (β€ β
β))))))β(π
βͺ π)) = (πβ((π βͺ π) β (πΉ βͺ ( I βΎ (β€ β
β)))))) |
98 | 74, 97 | eqtr4d 2780 |
. . . . . . . . . . . 12
β’
((((((π β
β0 β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β§ π β (β0
βm (1...π))) β§ π β (β0
βm (β€ β β))) β (πβ((π β πΉ) βͺ π)) = ((π β (β€ βm ((β€
β β) βͺ (1...π))) β¦ (πβ(π β (πΉ βͺ ( I βΎ (β€ β
β))))))β(π
βͺ π))) |
99 | 98 | eqeq1d 2739 |
. . . . . . . . . . 11
β’
((((((π β
β0 β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β§ π β (β0
βm (1...π))) β§ π β (β0
βm (β€ β β))) β ((πβ((π β πΉ) βͺ π)) = 0 β ((π β (β€ βm ((β€
β β) βͺ (1...π))) β¦ (πβ(π β (πΉ βͺ ( I βΎ (β€ β
β))))))β(π
βͺ π)) =
0)) |
100 | 99 | rexbidva 3174 |
. . . . . . . . . 10
β’
(((((π β
β0 β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β§ π β (β0
βm (1...π))) β (βπ β (β0
βm (β€ β β))(πβ((π β πΉ) βͺ π)) = 0 β βπ β (β0
βm (β€ β β))((π β (β€ βm ((β€
β β) βͺ (1...π))) β¦ (πβ(π β (πΉ βͺ ( I βΎ (β€ β
β))))))β(π
βͺ π)) =
0)) |
101 | 28, 100 | bitrd 279 |
. . . . . . . . 9
β’
(((((π β
β0 β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β§ π β (β0
βm (1...π))) β ((π β πΉ) β {π β (β0
βm (1...π))
β£ βπ β
(β0 βm (β€ β β))(πβ(π βͺ π)) = 0} β βπ β (β0
βm (β€ β β))((π β (β€ βm ((β€
β β) βͺ (1...π))) β¦ (πβ(π β (πΉ βͺ ( I βΎ (β€ β
β))))))β(π
βͺ π)) =
0)) |
102 | 101 | rabbidva 3417 |
. . . . . . . 8
β’ ((((π β β0
β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β {π β (β0
βm (1...π))
β£ (π β πΉ) β {π β (β0
βm (1...π))
β£ βπ β
(β0 βm (β€ β β))(πβ(π βͺ π)) = 0}} = {π β (β0
βm (1...π))
β£ βπ β
(β0 βm (β€ β β))((π β (β€
βm ((β€ β β) βͺ (1...π))) β¦ (πβ(π β (πΉ βͺ ( I βΎ (β€ β
β))))))β(π
βͺ π)) =
0}) |
103 | | simplll 774 |
. . . . . . . . 9
β’ ((((π β β0
β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β π β
β0) |
104 | | ovex 7395 |
. . . . . . . . . . . 12
β’
(1...π) β
V |
105 | 3, 104 | unex 7685 |
. . . . . . . . . . 11
β’ ((β€
β β) βͺ (1...π)) β V |
106 | 105 | a1i 11 |
. . . . . . . . . 10
β’ ((((π β β0
β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β ((β€ β β) βͺ
(1...π)) β
V) |
107 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β β0
β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β π β (mzPolyβ((β€ β
β) βͺ (1...π)))) |
108 | 55 | a1i 11 |
. . . . . . . . . . . . 13
β’ (πΉ:(1...π)βΆ(1...π) β ( I βΎ (β€ β
β)):(β€ β β)βΆ(β€ β
β)) |
109 | | id 22 |
. . . . . . . . . . . . 13
β’ (πΉ:(1...π)βΆ(1...π) β πΉ:(1...π)βΆ(1...π)) |
110 | | incom 4166 |
. . . . . . . . . . . . . . 15
β’ ((β€
β β) β© (1...π)) = ((1...π) β© (β€ β
β)) |
111 | | fz1ssnn 13479 |
. . . . . . . . . . . . . . . 16
β’
(1...π) β
β |
112 | | ssdisj 4424 |
. . . . . . . . . . . . . . . 16
β’
(((1...π) β
β β§ (β β© (β€ β β)) = β
) β
((1...π) β© (β€
β β)) = β
) |
113 | 111, 39, 112 | mp2an 691 |
. . . . . . . . . . . . . . 15
β’
((1...π) β©
(β€ β β)) = β
|
114 | 110, 113 | eqtri 2765 |
. . . . . . . . . . . . . 14
β’ ((β€
β β) β© (1...π)) = β
|
115 | 114 | a1i 11 |
. . . . . . . . . . . . 13
β’ (πΉ:(1...π)βΆ(1...π) β ((β€ β β) β©
(1...π)) =
β
) |
116 | | fun 6709 |
. . . . . . . . . . . . 13
β’ (((( I
βΎ (β€ β β)):(β€ β β)βΆ(β€
β β) β§ πΉ:(1...π)βΆ(1...π)) β§ ((β€ β β) β©
(1...π)) = β
) β
(( I βΎ (β€ β β)) βͺ πΉ):((β€ β β) βͺ
(1...π))βΆ((β€
β β) βͺ (1...π))) |
117 | 108, 109,
115, 116 | syl21anc 837 |
. . . . . . . . . . . 12
β’ (πΉ:(1...π)βΆ(1...π) β (( I βΎ (β€ β
β)) βͺ πΉ):((β€ β β) βͺ
(1...π))βΆ((β€
β β) βͺ (1...π))) |
118 | | uncom 4118 |
. . . . . . . . . . . . 13
β’ (( I
βΎ (β€ β β)) βͺ πΉ) = (πΉ βͺ ( I βΎ (β€ β
β))) |
119 | 118 | feq1i 6664 |
. . . . . . . . . . . 12
β’ ((( I
βΎ (β€ β β)) βͺ πΉ):((β€ β β) βͺ
(1...π))βΆ((β€
β β) βͺ (1...π)) β (πΉ βͺ ( I βΎ (β€ β
β))):((β€ β β) βͺ (1...π))βΆ((β€ β β) βͺ
(1...π))) |
120 | 117, 119 | sylib 217 |
. . . . . . . . . . 11
β’ (πΉ:(1...π)βΆ(1...π) β (πΉ βͺ ( I βΎ (β€ β
β))):((β€ β β) βͺ (1...π))βΆ((β€ β β) βͺ
(1...π))) |
121 | 120 | ad3antlr 730 |
. . . . . . . . . 10
β’ ((((π β β0
β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β (πΉ βͺ ( I βΎ (β€ β
β))):((β€ β β) βͺ (1...π))βΆ((β€ β β) βͺ
(1...π))) |
122 | | mzprename 41101 |
. . . . . . . . . 10
β’
((((β€ β β) βͺ (1...π)) β V β§ π β (mzPolyβ((β€ β
β) βͺ (1...π)))
β§ (πΉ βͺ ( I βΎ
(β€ β β))):((β€ β β) βͺ (1...π))βΆ((β€ β
β) βͺ (1...π)))
β (π β (β€
βm ((β€ β β) βͺ (1...π))) β¦ (πβ(π β (πΉ βͺ ( I βΎ (β€ β
β)))))) β (mzPolyβ((β€ β β) βͺ (1...π)))) |
123 | 106, 107,
121, 122 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((π β β0
β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β (π β (β€ βm ((β€
β β) βͺ (1...π))) β¦ (πβ(π β (πΉ βͺ ( I βΎ (β€ β
β)))))) β (mzPolyβ((β€ β β) βͺ (1...π)))) |
124 | 3, 16, 17 | eldioph4i 41164 |
. . . . . . . . 9
β’ ((π β β0
β§ (π β (β€
βm ((β€ β β) βͺ (1...π))) β¦ (πβ(π β (πΉ βͺ ( I βΎ (β€ β
β)))))) β (mzPolyβ((β€ β β) βͺ (1...π)))) β {π β (β0
βm (1...π))
β£ βπ β
(β0 βm (β€ β β))((π β (β€
βm ((β€ β β) βͺ (1...π))) β¦ (πβ(π β (πΉ βͺ ( I βΎ (β€ β
β))))))β(π
βͺ π)) = 0} β
(Diophβπ)) |
125 | 103, 123,
124 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β β0
β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β {π β (β0
βm (1...π))
β£ βπ β
(β0 βm (β€ β β))((π β (β€
βm ((β€ β β) βͺ (1...π))) β¦ (πβ(π β (πΉ βͺ ( I βΎ (β€ β
β))))))β(π
βͺ π)) = 0} β
(Diophβπ)) |
126 | 102, 125 | eqeltrd 2838 |
. . . . . . 7
β’ ((((π β β0
β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β {π β (β0
βm (1...π))
β£ (π β πΉ) β {π β (β0
βm (1...π))
β£ βπ β
(β0 βm (β€ β β))(πβ(π βͺ π)) = 0}} β (Diophβπ)) |
127 | | eleq2 2827 |
. . . . . . . . 9
β’ (π = {π β (β0
βm (1...π))
β£ βπ β
(β0 βm (β€ β β))(πβ(π βͺ π)) = 0} β ((π β πΉ) β π β (π β πΉ) β {π β (β0
βm (1...π))
β£ βπ β
(β0 βm (β€ β β))(πβ(π βͺ π)) = 0})) |
128 | 127 | rabbidv 3418 |
. . . . . . . 8
β’ (π = {π β (β0
βm (1...π))
β£ βπ β
(β0 βm (β€ β β))(πβ(π βͺ π)) = 0} β {π β (β0
βm (1...π))
β£ (π β πΉ) β π} = {π β (β0
βm (1...π))
β£ (π β πΉ) β {π β (β0
βm (1...π))
β£ βπ β
(β0 βm (β€ β β))(πβ(π βͺ π)) = 0}}) |
129 | 128 | eleq1d 2823 |
. . . . . . 7
β’ (π = {π β (β0
βm (1...π))
β£ βπ β
(β0 βm (β€ β β))(πβ(π βͺ π)) = 0} β ({π β (β0
βm (1...π))
β£ (π β πΉ) β π} β (Diophβπ) β {π β (β0
βm (1...π))
β£ (π β πΉ) β {π β (β0
βm (1...π))
β£ βπ β
(β0 βm (β€ β β))(πβ(π βͺ π)) = 0}} β (Diophβπ))) |
130 | 126, 129 | syl5ibrcom 247 |
. . . . . 6
β’ ((((π β β0
β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β§ π β (mzPolyβ((β€
β β) βͺ (1...π)))) β (π = {π β (β0
βm (1...π))
β£ βπ β
(β0 βm (β€ β β))(πβ(π βͺ π)) = 0} β {π β (β0
βm (1...π))
β£ (π β πΉ) β π} β (Diophβπ))) |
131 | 130 | rexlimdva 3153 |
. . . . 5
β’ (((π β β0
β§ πΉ:(1...π)βΆ(1...π)) β§ π β β0) β
(βπ β
(mzPolyβ((β€ β β) βͺ (1...π)))π = {π β (β0
βm (1...π))
β£ βπ β
(β0 βm (β€ β β))(πβ(π βͺ π)) = 0} β {π β (β0
βm (1...π))
β£ (π β πΉ) β π} β (Diophβπ))) |
132 | 131 | expimpd 455 |
. . . 4
β’ ((π β β0
β§ πΉ:(1...π)βΆ(1...π)) β ((π β β0 β§
βπ β
(mzPolyβ((β€ β β) βͺ (1...π)))π = {π β (β0
βm (1...π))
β£ βπ β
(β0 βm (β€ β β))(πβ(π βͺ π)) = 0}) β {π β (β0
βm (1...π))
β£ (π β πΉ) β π} β (Diophβπ))) |
133 | 18, 132 | biimtrid 241 |
. . 3
β’ ((π β β0
β§ πΉ:(1...π)βΆ(1...π)) β (π β (Diophβπ) β {π β (β0
βm (1...π))
β£ (π β πΉ) β π} β (Diophβπ))) |
134 | 133 | impcom 409 |
. 2
β’ ((π β (Diophβπ) β§ (π β β0 β§ πΉ:(1...π)βΆ(1...π))) β {π β (β0
βm (1...π))
β£ (π β πΉ) β π} β (Diophβπ)) |
135 | 134 | 3impb 1116 |
1
β’ ((π β (Diophβπ) β§ π β β0 β§ πΉ:(1...π)βΆ(1...π)) β {π β (β0
βm (1...π))
β£ (π β πΉ) β π} β (Diophβπ)) |