Step | Hyp | Ref
| Expression |
1 | | simpr 483 |
. . . . . . . 8
β’ (((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β π₯ β (β€ βm π)) |
2 | | zex 12571 |
. . . . . . . . 9
β’ β€
β V |
3 | | simpll 763 |
. . . . . . . . 9
β’ (((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β π β V) |
4 | | elmapg 8835 |
. . . . . . . . 9
β’ ((β€
β V β§ π β V)
β (π₯ β (β€
βm π)
β π₯:πβΆβ€)) |
5 | 2, 3, 4 | sylancr 585 |
. . . . . . . 8
β’ (((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β (π₯ β (β€ βm π) β π₯:πβΆβ€)) |
6 | 1, 5 | mpbid 231 |
. . . . . . 7
β’ (((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β π₯:πβΆβ€) |
7 | | simplr 765 |
. . . . . . 7
β’ (((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β π
:πβΆπ) |
8 | | fcompt 7132 |
. . . . . . 7
β’ ((π₯:πβΆβ€ β§ π
:πβΆπ) β (π₯ β π
) = (π β π β¦ (π₯β(π
βπ)))) |
9 | 6, 7, 8 | syl2anc 582 |
. . . . . 6
β’ (((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β (π₯ β π
) = (π β π β¦ (π₯β(π
βπ)))) |
10 | | fveq1 6889 |
. . . . . . . . . 10
β’ (π = π₯ β (πβ(π
βπ)) = (π₯β(π
βπ))) |
11 | | eqid 2730 |
. . . . . . . . . 10
β’ (π β (β€
βm π)
β¦ (πβ(π
βπ))) = (π β (β€ βm π) β¦ (πβ(π
βπ))) |
12 | | fvex 6903 |
. . . . . . . . . 10
β’ (π₯β(π
βπ)) β V |
13 | 10, 11, 12 | fvmpt 6997 |
. . . . . . . . 9
β’ (π₯ β (β€
βm π)
β ((π β (β€
βm π)
β¦ (πβ(π
βπ)))βπ₯) = (π₯β(π
βπ))) |
14 | 13 | ad2antlr 723 |
. . . . . . . 8
β’ ((((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β§ π β π) β ((π β (β€ βm π) β¦ (πβ(π
βπ)))βπ₯) = (π₯β(π
βπ))) |
15 | 14 | eqcomd 2736 |
. . . . . . 7
β’ ((((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β§ π β π) β (π₯β(π
βπ)) = ((π β (β€ βm π) β¦ (πβ(π
βπ)))βπ₯)) |
16 | 15 | mpteq2dva 5247 |
. . . . . 6
β’ (((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β (π β π β¦ (π₯β(π
βπ))) = (π β π β¦ ((π β (β€ βm π) β¦ (πβ(π
βπ)))βπ₯))) |
17 | 9, 16 | eqtrd 2770 |
. . . . 5
β’ (((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β (π₯ β π
) = (π β π β¦ ((π β (β€ βm π) β¦ (πβ(π
βπ)))βπ₯))) |
18 | 17 | fveq2d 6894 |
. . . 4
β’ (((π β V β§ π
:πβΆπ) β§ π₯ β (β€ βm π)) β (πΉβ(π₯ β π
)) = (πΉβ(π β π β¦ ((π β (β€ βm π) β¦ (πβ(π
βπ)))βπ₯)))) |
19 | 18 | mpteq2dva 5247 |
. . 3
β’ ((π β V β§ π
:πβΆπ) β (π₯ β (β€ βm π) β¦ (πΉβ(π₯ β π
))) = (π₯ β (β€ βm π) β¦ (πΉβ(π β π β¦ ((π β (β€ βm π) β¦ (πβ(π
βπ)))βπ₯))))) |
20 | 19 | 3adant2 1129 |
. 2
β’ ((π β V β§ πΉ β (mzPolyβπ) β§ π
:πβΆπ) β (π₯ β (β€ βm π) β¦ (πΉβ(π₯ β π
))) = (π₯ β (β€ βm π) β¦ (πΉβ(π β π β¦ ((π β (β€ βm π) β¦ (πβ(π
βπ)))βπ₯))))) |
21 | | simpl1 1189 |
. . . . 5
β’ (((π β V β§ πΉ β (mzPolyβπ) β§ π
:πβΆπ) β§ π β π) β π β V) |
22 | | ffvelcdm 7082 |
. . . . . 6
β’ ((π
:πβΆπ β§ π β π) β (π
βπ) β π) |
23 | 22 | 3ad2antl3 1185 |
. . . . 5
β’ (((π β V β§ πΉ β (mzPolyβπ) β§ π
:πβΆπ) β§ π β π) β (π
βπ) β π) |
24 | | mzpproj 41777 |
. . . . 5
β’ ((π β V β§ (π
βπ) β π) β (π β (β€ βm π) β¦ (πβ(π
βπ))) β (mzPolyβπ)) |
25 | 21, 23, 24 | syl2anc 582 |
. . . 4
β’ (((π β V β§ πΉ β (mzPolyβπ) β§ π
:πβΆπ) β§ π β π) β (π β (β€ βm π) β¦ (πβ(π
βπ))) β (mzPolyβπ)) |
26 | 25 | ralrimiva 3144 |
. . 3
β’ ((π β V β§ πΉ β (mzPolyβπ) β§ π
:πβΆπ) β βπ β π (π β (β€ βm π) β¦ (πβ(π
βπ))) β (mzPolyβπ)) |
27 | | mzpsubst 41788 |
. . 3
β’ ((π β V β§ πΉ β (mzPolyβπ) β§ βπ β π (π β (β€ βm π) β¦ (πβ(π
βπ))) β (mzPolyβπ)) β (π₯ β (β€ βm π) β¦ (πΉβ(π β π β¦ ((π β (β€ βm π) β¦ (πβ(π
βπ)))βπ₯)))) β (mzPolyβπ)) |
28 | 26, 27 | syld3an3 1407 |
. 2
β’ ((π β V β§ πΉ β (mzPolyβπ) β§ π
:πβΆπ) β (π₯ β (β€ βm π) β¦ (πΉβ(π β π β¦ ((π β (β€ βm π) β¦ (πβ(π
βπ)))βπ₯)))) β (mzPolyβπ)) |
29 | 20, 28 | eqeltrd 2831 |
1
β’ ((π β V β§ πΉ β (mzPolyβπ) β§ π
:πβΆπ) β (π₯ β (β€ βm π) β¦ (πΉβ(π₯ β π
))) β (mzPolyβπ)) |