Step | Hyp | Ref
| Expression |
1 | | mzpcompact2 41104 |
. . 3
β’ (π β (mzPolyβπ) β βπ β Fin βπ β (mzPolyβπ)(π β π β§ π = (π β (β€ βm π) β¦ (πβ(π βΎ π))))) |
2 | 1 | 3ad2ant3 1136 |
. 2
β’ ((π β β0
β§ (π β V β§
(1...π) β π) β§ π β (mzPolyβπ)) β βπ β Fin βπ β (mzPolyβπ)(π β π β§ π = (π β (β€ βm π) β¦ (πβ(π βΎ π))))) |
3 | | fveq1 6846 |
. . . . . . . . . 10
β’ (π = (π β (β€ βm π) β¦ (πβ(π βΎ π))) β (πβπ’) = ((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’)) |
4 | 3 | eqeq1d 2739 |
. . . . . . . . 9
β’ (π = (π β (β€ βm π) β¦ (πβ(π βΎ π))) β ((πβπ’) = 0 β ((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’) = 0)) |
5 | 4 | anbi2d 630 |
. . . . . . . 8
β’ (π = (π β (β€ βm π) β¦ (πβ(π βΎ π))) β ((π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0) β (π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’) = 0))) |
6 | 5 | rexbidv 3176 |
. . . . . . 7
β’ (π = (π β (β€ βm π) β¦ (πβ(π βΎ π))) β (βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0) β βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’) = 0))) |
7 | 6 | abbidv 2806 |
. . . . . 6
β’ (π = (π β (β€ βm π) β¦ (πβ(π βΎ π))) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’) = 0)}) |
8 | 7 | ad2antll 728 |
. . . . 5
β’ ((((π β β0
β§ (π β V β§
(1...π) β π) β§ π β (mzPolyβπ)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ (π β π β§ π = (π β (β€ βm π) β¦ (πβ(π βΎ π))))) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’) = 0)}) |
9 | | simplll 774 |
. . . . . . . . . . 11
β’ ((((π β β0
β§ (π β V β§
(1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β π β
β0) |
10 | | simplrl 776 |
. . . . . . . . . . . 12
β’ ((((π β β0
β§ (π β V β§
(1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β π β Fin) |
11 | | fzfi 13884 |
. . . . . . . . . . . 12
β’
(1...π) β
Fin |
12 | | unfi 9123 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ (1...π) β Fin) β (π βͺ (1...π)) β Fin) |
13 | 10, 11, 12 | sylancl 587 |
. . . . . . . . . . 11
β’ ((((π β β0
β§ (π β V β§
(1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β (π βͺ (1...π)) β Fin) |
14 | | ssun2 4138 |
. . . . . . . . . . . 12
β’
(1...π) β
(π βͺ (1...π)) |
15 | 14 | a1i 11 |
. . . . . . . . . . 11
β’ ((((π β β0
β§ (π β V β§
(1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β (1...π) β (π βͺ (1...π))) |
16 | | eldioph2lem1 41112 |
. . . . . . . . . . 11
β’ ((π β β0
β§ (π βͺ (1...π)) β Fin β§ (1...π) β (π βͺ (1...π))) β βπ β (β€β₯βπ)βπ β V (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) |
17 | 9, 13, 15, 16 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π β β0
β§ (π β V β§
(1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β βπ β (β€β₯βπ)βπ β V (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) |
18 | | f1ococnv2 6816 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β (π β β‘π) = ( I βΎ (π βͺ (1...π)))) |
19 | 18 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β (π β β‘π) = ( I βΎ (π βͺ (1...π)))) |
20 | 19 | reseq1d 5941 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β ((π β β‘π) βΎ π) = (( I βΎ (π βͺ (1...π))) βΎ π)) |
21 | | ssun1 4137 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ π β (π βͺ (1...π)) |
22 | | resabs1 5972 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (π βͺ (1...π)) β (( I βΎ (π βͺ (1...π))) βΎ π) = ( I βΎ π)) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (( I
βΎ (π βͺ (1...π))) βΎ π) = ( I βΎ π) |
24 | 20, 23 | eqtr2di 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β ( I βΎ π) = ((π β β‘π) βΎ π)) |
25 | | resco 6207 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β β‘π) βΎ π) = (π β (β‘π βΎ π)) |
26 | 24, 25 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β ( I βΎ π) = (π β (β‘π βΎ π))) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β§ π β (β€ βm π)) β ( I βΎ π) = (π β (β‘π βΎ π))) |
28 | 27 | coeq2d 5823 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β§ π β (β€ βm π)) β (π β ( I βΎ π)) = (π β (π β (β‘π βΎ π)))) |
29 | | coires1 6221 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β ( I βΎ π)) = (π βΎ π) |
30 | | coass 6222 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β π) β (β‘π βΎ π)) = (π β (π β (β‘π βΎ π))) |
31 | 30 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π β (β‘π βΎ π))) = ((π β π) β (β‘π βΎ π)) |
32 | 28, 29, 31 | 3eqtr3g 2800 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β§ π β (β€ βm π)) β (π βΎ π) = ((π β π) β (β‘π βΎ π))) |
33 | 32 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β§ π β (β€ βm π)) β (πβ(π βΎ π)) = (πβ((π β π) β (β‘π βΎ π)))) |
34 | | ovexd 7397 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β§ π β (β€ βm π)) β (1...π) β V) |
35 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β§ π β (β€ βm π)) β π β (β€ βm π)) |
36 | | f1of1 6788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β π:(1...π)β1-1β(π βͺ (1...π))) |
37 | 36 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β π:(1...π)β1-1β(π βͺ (1...π))) |
38 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β β0
β§ (π β V β§
(1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β π β π) |
39 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β β0
β§ (π β V β§
(1...π) β π)) β (1...π) β π) |
40 | 39 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β β0
β§ (π β V β§
(1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β (1...π) β π) |
41 | 38, 40 | unssd 4151 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β β0
β§ (π β V β§
(1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β (π βͺ (1...π)) β π) |
42 | 41 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β (π βͺ (1...π)) β π) |
43 | | f1ss 6749 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π:(1...π)β1-1β(π βͺ (1...π)) β§ (π βͺ (1...π)) β π) β π:(1...π)β1-1βπ) |
44 | 37, 42, 43 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β π:(1...π)β1-1βπ) |
45 | | f1f 6743 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π:(1...π)β1-1βπ β π:(1...π)βΆπ) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β π:(1...π)βΆπ) |
47 | 46 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β§ π β (β€ βm π)) β π:(1...π)βΆπ) |
48 | | mapco2g 41066 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((1...π) β V
β§ π β (β€
βm π) β§
π:(1...π)βΆπ) β (π β π) β (β€ βm
(1...π))) |
49 | 34, 35, 47, 48 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β§ π β (β€ βm π)) β (π β π) β (β€ βm
(1...π))) |
50 | | coeq1 5818 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (β = (π β π) β (β β (β‘π βΎ π)) = ((π β π) β (β‘π βΎ π))) |
51 | 50 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (β = (π β π) β (πβ(β β (β‘π βΎ π))) = (πβ((π β π) β (β‘π βΎ π)))) |
52 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (β β (β€
βm (1...π))
β¦ (πβ(β β (β‘π βΎ π)))) = (β β (β€ βm (1...π)) β¦ (πβ(β β (β‘π βΎ π)))) |
53 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πβ((π β π) β (β‘π βΎ π))) β V |
54 | 51, 52, 53 | fvmpt 6953 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β π) β (β€ βm
(1...π)) β ((β β (β€
βm (1...π))
β¦ (πβ(β β (β‘π βΎ π))))β(π β π)) = (πβ((π β π) β (β‘π βΎ π)))) |
55 | 49, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β§ π β (β€ βm π)) β ((β β (β€ βm (1...π)) β¦ (πβ(β β (β‘π βΎ π))))β(π β π)) = (πβ((π β π) β (β‘π βΎ π)))) |
56 | 33, 55 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β§ π β (β€ βm π)) β (πβ(π βΎ π)) = ((β β (β€ βm (1...π)) β¦ (πβ(β β (β‘π βΎ π))))β(π β π))) |
57 | 56 | mpteq2dva 5210 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β (π β (β€ βm π) β¦ (πβ(π βΎ π))) = (π β (β€ βm π) β¦ ((β β (β€ βm (1...π)) β¦ (πβ(β β (β‘π βΎ π))))β(π β π)))) |
58 | 57 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β ((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’) = ((π β (β€ βm π) β¦ ((β β (β€ βm (1...π)) β¦ (πβ(β β (β‘π βΎ π))))β(π β π)))βπ’)) |
59 | 58 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β (((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’) = 0 β ((π β (β€ βm π) β¦ ((β β (β€ βm (1...π)) β¦ (πβ(β β (β‘π βΎ π))))β(π β π)))βπ’) = 0)) |
60 | 59 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β ((π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’) = 0) β (π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ ((β β (β€ βm (1...π)) β¦ (πβ(β β (β‘π βΎ π))))β(π β π)))βπ’) = 0))) |
61 | 60 | rexbidv 3176 |
. . . . . . . . . . . . . . 15
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β (βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’) = 0) β βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ ((β β (β€ βm (1...π)) β¦ (πβ(β β (β‘π βΎ π))))β(π β π)))βπ’) = 0))) |
62 | 61 | abbidv 2806 |
. . . . . . . . . . . . . 14
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ ((β β (β€ βm (1...π)) β¦ (πβ(β β (β‘π βΎ π))))β(π β π)))βπ’) = 0)}) |
63 | | simplrl 776 |
. . . . . . . . . . . . . . . 16
β’ (((π β β0
β§ (π β V β§
(1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β π β V) |
64 | 63 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β π β V) |
65 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β (π βΎ (1...π)) = ( I βΎ (1...π))) |
66 | | diophrw 41111 |
. . . . . . . . . . . . . . 15
β’ ((π β V β§ π:(1...π)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π))) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ ((β β (β€ βm (1...π)) β¦ (πβ(β β (β‘π βΎ π))))β(π β π)))βπ’) = 0)} = {π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ ((β β (β€ βm (1...π)) β¦ (πβ(β β (β‘π βΎ π))))βπ) = 0)}) |
67 | 64, 44, 65, 66 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ ((β β (β€ βm (1...π)) β¦ (πβ(β β (β‘π βΎ π))))β(π β π)))βπ’) = 0)} = {π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ ((β β (β€ βm (1...π)) β¦ (πβ(β β (β‘π βΎ π))))βπ) = 0)}) |
68 | 62, 67 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’) = 0)} = {π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ ((β β (β€ βm (1...π)) β¦ (πβ(β β (β‘π βΎ π))))βπ) = 0)}) |
69 | | simp-5l 784 |
. . . . . . . . . . . . . 14
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β π β
β0) |
70 | | simplrl 776 |
. . . . . . . . . . . . . 14
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β π β (β€β₯βπ)) |
71 | | ovexd 7397 |
. . . . . . . . . . . . . . 15
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β (1...π) β V) |
72 | | simplrr 777 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β0
β§ (π β V β§
(1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β π β (mzPolyβπ)) |
73 | 72 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β π β (mzPolyβπ)) |
74 | | f1ocnv 6801 |
. . . . . . . . . . . . . . . . . 18
β’ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β β‘π:(π βͺ (1...π))β1-1-ontoβ(1...π)) |
75 | | f1of 6789 |
. . . . . . . . . . . . . . . . . 18
β’ (β‘π:(π βͺ (1...π))β1-1-ontoβ(1...π) β β‘π:(π βͺ (1...π))βΆ(1...π)) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β β‘π:(π βͺ (1...π))βΆ(1...π)) |
77 | | fssres 6713 |
. . . . . . . . . . . . . . . . 17
β’ ((β‘π:(π βͺ (1...π))βΆ(1...π) β§ π β (π βͺ (1...π))) β (β‘π βΎ π):πβΆ(1...π)) |
78 | 76, 21, 77 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β (β‘π βΎ π):πβΆ(1...π)) |
79 | 78 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β (β‘π βΎ π):πβΆ(1...π)) |
80 | | mzprename 41101 |
. . . . . . . . . . . . . . 15
β’
(((1...π) β V
β§ π β
(mzPolyβπ) β§
(β‘π βΎ π):πβΆ(1...π)) β (β β (β€ βm (1...π)) β¦ (πβ(β β (β‘π βΎ π)))) β (mzPolyβ(1...π))) |
81 | 71, 73, 79, 80 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β (β β (β€ βm (1...π)) β¦ (πβ(β β (β‘π βΎ π)))) β (mzPolyβ(1...π))) |
82 | | eldioph 41110 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π β
(β€β₯βπ) β§ (β β (β€ βm (1...π)) β¦ (πβ(β β (β‘π βΎ π)))) β (mzPolyβ(1...π))) β {π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ ((β β (β€ βm (1...π)) β¦ (πβ(β β (β‘π βΎ π))))βπ) = 0)} β (Diophβπ)) |
83 | 69, 70, 81, 82 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β {π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ ((β β (β€ βm (1...π)) β¦ (πβ(β β (β‘π βΎ π))))βπ) = 0)} β (Diophβπ)) |
84 | 68, 83 | eqeltrd 2838 |
. . . . . . . . . . . 12
β’
((((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β§ (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’) = 0)} β (Diophβπ)) |
85 | 84 | ex 414 |
. . . . . . . . . . 11
β’
(((((π β
β0 β§ (π β V β§ (1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β§ (π β (β€β₯βπ) β§ π β V)) β ((π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π))) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’) = 0)} β (Diophβπ))) |
86 | 85 | rexlimdvva 3206 |
. . . . . . . . . 10
β’ ((((π β β0
β§ (π β V β§
(1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β (βπ β (β€β₯βπ)βπ β V (π:(1...π)β1-1-ontoβ(π βͺ (1...π)) β§ (π βΎ (1...π)) = ( I βΎ (1...π))) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’) = 0)} β (Diophβπ))) |
87 | 17, 86 | mpd 15 |
. . . . . . . . 9
β’ ((((π β β0
β§ (π β V β§
(1...π) β π)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’) = 0)} β (Diophβπ)) |
88 | 87 | exp31 421 |
. . . . . . . 8
β’ ((π β β0
β§ (π β V β§
(1...π) β π)) β ((π β Fin β§ π β (mzPolyβπ)) β (π β π β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’) = 0)} β (Diophβπ)))) |
89 | 88 | 3adant3 1133 |
. . . . . . 7
β’ ((π β β0
β§ (π β V β§
(1...π) β π) β§ π β (mzPolyβπ)) β ((π β Fin β§ π β (mzPolyβπ)) β (π β π β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’) = 0)} β (Diophβπ)))) |
90 | 89 | imp31 419 |
. . . . . 6
β’ ((((π β β0
β§ (π β V β§
(1...π) β π) β§ π β (mzPolyβπ)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ π β π) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’) = 0)} β (Diophβπ)) |
91 | 90 | adantrr 716 |
. . . . 5
β’ ((((π β β0
β§ (π β V β§
(1...π) β π) β§ π β (mzPolyβπ)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ (π β π β§ π = (π β (β€ βm π) β¦ (πβ(π βΎ π))))) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π βΎ π)))βπ’) = 0)} β (Diophβπ)) |
92 | 8, 91 | eqeltrd 2838 |
. . . 4
β’ ((((π β β0
β§ (π β V β§
(1...π) β π) β§ π β (mzPolyβπ)) β§ (π β Fin β§ π β (mzPolyβπ))) β§ (π β π β§ π = (π β (β€ βm π) β¦ (πβ(π βΎ π))))) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β (Diophβπ)) |
93 | 92 | ex 414 |
. . 3
β’ (((π β β0
β§ (π β V β§
(1...π) β π) β§ π β (mzPolyβπ)) β§ (π β Fin β§ π β (mzPolyβπ))) β ((π β π β§ π = (π β (β€ βm π) β¦ (πβ(π βΎ π)))) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β (Diophβπ))) |
94 | 93 | rexlimdvva 3206 |
. 2
β’ ((π β β0
β§ (π β V β§
(1...π) β π) β§ π β (mzPolyβπ)) β (βπ β Fin βπ β (mzPolyβπ)(π β π β§ π = (π β (β€ βm π) β¦ (πβ(π βΎ π)))) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β (Diophβπ))) |
95 | 2, 94 | mpd 15 |
1
β’ ((π β β0
β§ (π β V β§
(1...π) β π) β§ π β (mzPolyβπ)) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β (Diophβπ)) |