Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . . 8
β’ (((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β π₯ β (β€ βm π)) |
2 | | zex 12567 |
. . . . . . . . 9
β’ β€
β V |
3 | | simpll 766 |
. . . . . . . . 9
β’ (((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β π β V) |
4 | | elmapg 8833 |
. . . . . . . . 9
β’ ((β€
β V β§ π β V)
β (π₯ β (β€
βm π)
β π₯:πβΆβ€)) |
5 | 2, 3, 4 | sylancr 588 |
. . . . . . . 8
β’ (((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β (π₯ β (β€ βm π) β π₯:πβΆβ€)) |
6 | 1, 5 | mpbid 231 |
. . . . . . 7
β’ (((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β π₯:πβΆβ€) |
7 | | simplr 768 |
. . . . . . 7
β’ (((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β π
:πβΆπ) |
8 | | fcompt 7131 |
. . . . . . 7
β’ ((π₯:πβΆβ€ β§ π
:πβΆπ) β (π₯ β π
) = (π β π β¦ (π₯β(π
βπ)))) |
9 | 6, 7, 8 | syl2anc 585 |
. . . . . 6
β’ (((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β (π₯ β π
) = (π β π β¦ (π₯β(π
βπ)))) |
10 | | fveq1 6891 |
. . . . . . . . . 10
β’ (π = π₯ β (πβ(π
βπ)) = (π₯β(π
βπ))) |
11 | | eqid 2733 |
. . . . . . . . . 10
β’ (π β (β€
βm π)
β¦ (πβ(π
βπ))) = (π β (β€ βm π) β¦ (πβ(π
βπ))) |
12 | | fvex 6905 |
. . . . . . . . . 10
β’ (π₯β(π
βπ)) β V |
13 | 10, 11, 12 | fvmpt 6999 |
. . . . . . . . 9
β’ (π₯ β (β€
βm π)
β ((π β (β€
βm π)
β¦ (πβ(π
βπ)))βπ₯) = (π₯β(π
βπ))) |
14 | 13 | ad2antlr 726 |
. . . . . . . 8
β’ ((((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β§ π β π) β ((π β (β€ βm π) β¦ (πβ(π
βπ)))βπ₯) = (π₯β(π
βπ))) |
15 | 14 | eqcomd 2739 |
. . . . . . 7
β’ ((((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β§ π β π) β (π₯β(π
βπ)) = ((π β (β€ βm π) β¦ (πβ(π
βπ)))βπ₯)) |
16 | 15 | mpteq2dva 5249 |
. . . . . 6
β’ (((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β (π β π β¦ (π₯β(π
βπ))) = (π β π β¦ ((π β (β€ βm π) β¦ (πβ(π
βπ)))βπ₯))) |
17 | 9, 16 | eqtrd 2773 |
. . . . 5
β’ (((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β (π₯ β π
) = (π β π β¦ ((π β (β€ βm π) β¦ (πβ(π
βπ)))βπ₯))) |
18 | 17 | fveq2d 6896 |
. . . 4
β’ (((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β (πΉβ(π₯ β π
)) = (πΉβ(π β π β¦ ((π β (β€ βm π) β¦ (πβ(π
βπ)))βπ₯)))) |
19 | 18 | mpteq2dva 5249 |
. . 3
β’ ((π β V β§ π
:πβΆπ) β (π₯ β (β€ βm π) β¦ (πΉβ(π₯ β π
))) = (π₯ β (β€ βm π) β¦ (πΉβ(π β π β¦ ((π β (β€ βm π) β¦ (πβ(π
βπ)))βπ₯))))) |
20 | 19 | 3adant2 1132 |
. 2
β’ ((π β V β§ πΉ β (mzPolyβπ) β§ π
:πβΆπ) β (π₯ β (β€ βm π) β¦ (πΉβ(π₯ β π
))) = (π₯ β (β€ βm π) β¦ (πΉβ(π β π β¦ ((π β (β€ βm π) β¦ (πβ(π
βπ)))βπ₯))))) |
21 | | simpl1 1192 |
. . . . 5
β’ (((π β V β§ πΉ β (mzPolyβπ) β§ π
:πβΆπ) β§ π β π) β π β V) |
22 | | ffvelcdm 7084 |
. . . . . 6
β’ ((π
:πβΆπ β§ π β π) β (π
βπ) β π) |
23 | 22 | 3ad2antl3 1188 |
. . . . 5
β’ (((π β V β§ πΉ β (mzPolyβπ) β§ π
:πβΆπ) β§ π β π) β (π
βπ) β π) |
24 | | mzpproj 41475 |
. . . . 5
β’ ((π β V β§ (π
βπ) β π) β (π β (β€ βm π) β¦ (πβ(π
βπ))) β (mzPolyβπ)) |
25 | 21, 23, 24 | syl2anc 585 |
. . . 4
β’ (((π β V β§ πΉ β (mzPolyβπ) β§ π
:πβΆπ) β§ π β π) β (π β (β€ βm π) β¦ (πβ(π
βπ))) β (mzPolyβπ)) |
26 | 25 | ralrimiva 3147 |
. . 3
β’ ((π β V β§ πΉ β (mzPolyβπ) β§ π
:πβΆπ) β βπ β π (π β (β€ βm π) β¦ (πβ(π
βπ))) β (mzPolyβπ)) |
27 | | mzpsubst 41486 |
. . 3
β’ ((π β V β§ πΉ β (mzPolyβπ) β§ βπ β π (π β (β€ βm π) β¦ (πβ(π
βπ))) β (mzPolyβπ)) β (π₯ β (β€ βm π) β¦ (πΉβ(π β π β¦ ((π β (β€ βm π) β¦ (πβ(π
βπ)))βπ₯)))) β (mzPolyβπ)) |
28 | 26, 27 | syld3an3 1410 |
. 2
β’ ((π β V β§ πΉ β (mzPolyβπ) β§ π
:πβΆπ) β (π₯ β (β€ βm π) β¦ (πΉβ(π β π β¦ ((π β (β€ βm π) β¦ (πβ(π
βπ)))βπ₯)))) β (mzPolyβπ)) |
29 | 20, 28 | eqeltrd 2834 |
1
β’ ((π β V β§ πΉ β (mzPolyβπ) β§ π
:πβΆπ) β (π₯ β (β€ βm π) β¦ (πΉβ(π₯ β π
))) β (mzPolyβπ)) |