Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. 2
β’ ((π β V β§ πΉ β (mzPolyβπ) β§ βπ¦ β π πΊ β (mzPolyβπ)) β π β V) |
2 | | elfvex 6929 |
. . 3
β’ (πΉ β (mzPolyβπ) β π β V) |
3 | 2 | 3ad2ant2 1134 |
. 2
β’ ((π β V β§ πΉ β (mzPolyβπ) β§ βπ¦ β π πΊ β (mzPolyβπ)) β π β V) |
4 | | simp3 1138 |
. 2
β’ ((π β V β§ πΉ β (mzPolyβπ) β§ βπ¦ β π πΊ β (mzPolyβπ)) β βπ¦ β π πΊ β (mzPolyβπ)) |
5 | | simp2 1137 |
. 2
β’ ((π β V β§ πΉ β (mzPolyβπ) β§ βπ¦ β π πΊ β (mzPolyβπ)) β πΉ β (mzPolyβπ)) |
6 | | simpr 485 |
. . . . . . 7
β’ ((((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β β€) β§ π₯ β (β€ βm π)) β π₯ β (β€ βm π)) |
7 | | simpll3 1214 |
. . . . . . 7
β’ ((((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β β€) β§ π₯ β (β€ βm π)) β βπ¦ β π πΊ β (mzPolyβπ)) |
8 | | simpll2 1213 |
. . . . . . 7
β’ ((((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β β€) β§ π₯ β (β€ βm π)) β π β V) |
9 | | mzpf 41464 |
. . . . . . . . . . . . . 14
β’ (πΊ β (mzPolyβπ) β πΊ:(β€ βm π)βΆβ€) |
10 | 9 | ffvelcdmda 7086 |
. . . . . . . . . . . . 13
β’ ((πΊ β (mzPolyβπ) β§ π₯ β (β€ βm π)) β (πΊβπ₯) β β€) |
11 | 10 | expcom 414 |
. . . . . . . . . . . 12
β’ (π₯ β (β€
βm π)
β (πΊ β
(mzPolyβπ) β
(πΊβπ₯) β β€)) |
12 | 11 | ralimdv 3169 |
. . . . . . . . . . 11
β’ (π₯ β (β€
βm π)
β (βπ¦ β
π πΊ β (mzPolyβπ) β βπ¦ β π (πΊβπ₯) β β€)) |
13 | 12 | imp 407 |
. . . . . . . . . 10
β’ ((π₯ β (β€
βm π) β§
βπ¦ β π πΊ β (mzPolyβπ)) β βπ¦ β π (πΊβπ₯) β β€) |
14 | | eqid 2732 |
. . . . . . . . . . 11
β’ (π¦ β π β¦ (πΊβπ₯)) = (π¦ β π β¦ (πΊβπ₯)) |
15 | 14 | fmpt 7109 |
. . . . . . . . . 10
β’
(βπ¦ β
π (πΊβπ₯) β β€ β (π¦ β π β¦ (πΊβπ₯)):πβΆβ€) |
16 | 13, 15 | sylib 217 |
. . . . . . . . 9
β’ ((π₯ β (β€
βm π) β§
βπ¦ β π πΊ β (mzPolyβπ)) β (π¦ β π β¦ (πΊβπ₯)):πβΆβ€) |
17 | 16 | adantr 481 |
. . . . . . . 8
β’ (((π₯ β (β€
βm π) β§
βπ¦ β π πΊ β (mzPolyβπ)) β§ π β V) β (π¦ β π β¦ (πΊβπ₯)):πβΆβ€) |
18 | | zex 12566 |
. . . . . . . . 9
β’ β€
β V |
19 | | simpr 485 |
. . . . . . . . 9
β’ (((π₯ β (β€
βm π) β§
βπ¦ β π πΊ β (mzPolyβπ)) β§ π β V) β π β V) |
20 | | elmapg 8832 |
. . . . . . . . 9
β’ ((β€
β V β§ π β V)
β ((π¦ β π β¦ (πΊβπ₯)) β (β€ βm π) β (π¦ β π β¦ (πΊβπ₯)):πβΆβ€)) |
21 | 18, 19, 20 | sylancr 587 |
. . . . . . . 8
β’ (((π₯ β (β€
βm π) β§
βπ¦ β π πΊ β (mzPolyβπ)) β§ π β V) β ((π¦ β π β¦ (πΊβπ₯)) β (β€ βm π) β (π¦ β π β¦ (πΊβπ₯)):πβΆβ€)) |
22 | 17, 21 | mpbird 256 |
. . . . . . 7
β’ (((π₯ β (β€
βm π) β§
βπ¦ β π πΊ β (mzPolyβπ)) β§ π β V) β (π¦ β π β¦ (πΊβπ₯)) β (β€ βm π)) |
23 | 6, 7, 8, 22 | syl21anc 836 |
. . . . . 6
β’ ((((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β β€) β§ π₯ β (β€ βm π)) β (π¦ β π β¦ (πΊβπ₯)) β (β€ βm π)) |
24 | | vex 3478 |
. . . . . . 7
β’ π β V |
25 | 24 | fvconst2 7204 |
. . . . . 6
β’ ((π¦ β π β¦ (πΊβπ₯)) β (β€ βm π) β (((β€
βm π)
Γ {π})β(π¦ β π β¦ (πΊβπ₯))) = π) |
26 | 23, 25 | syl 17 |
. . . . 5
β’ ((((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β β€) β§ π₯ β (β€ βm π)) β (((β€
βm π)
Γ {π})β(π¦ β π β¦ (πΊβπ₯))) = π) |
27 | 26 | mpteq2dva 5248 |
. . . 4
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β β€) β (π₯ β (β€ βm π) β¦ (((β€
βm π)
Γ {π})β(π¦ β π β¦ (πΊβπ₯)))) = (π₯ β (β€ βm π) β¦ π)) |
28 | | mzpconstmpt 41468 |
. . . . 5
β’ ((π β V β§ π β β€) β (π₯ β (β€
βm π)
β¦ π) β
(mzPolyβπ)) |
29 | 28 | 3ad2antl1 1185 |
. . . 4
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β β€) β (π₯ β (β€ βm π) β¦ π) β (mzPolyβπ)) |
30 | 27, 29 | eqeltrd 2833 |
. . 3
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β β€) β (π₯ β (β€ βm π) β¦ (((β€
βm π)
Γ {π})β(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) |
31 | | simpr 485 |
. . . . . . . . 9
β’ ((((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β π) β§ π₯ β (β€ βm π)) β π₯ β (β€ βm π)) |
32 | | simpll3 1214 |
. . . . . . . . 9
β’ ((((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β π) β§ π₯ β (β€ βm π)) β βπ¦ β π πΊ β (mzPolyβπ)) |
33 | | simpll2 1213 |
. . . . . . . . 9
β’ ((((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β π) β§ π₯ β (β€ βm π)) β π β V) |
34 | 31, 32, 33, 22 | syl21anc 836 |
. . . . . . . 8
β’ ((((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β π) β§ π₯ β (β€ βm π)) β (π¦ β π β¦ (πΊβπ₯)) β (β€ βm π)) |
35 | | fveq1 6890 |
. . . . . . . . 9
β’ (π = (π¦ β π β¦ (πΊβπ₯)) β (πβπ) = ((π¦ β π β¦ (πΊβπ₯))βπ)) |
36 | | eqid 2732 |
. . . . . . . . 9
β’ (π β (β€
βm π)
β¦ (πβπ)) = (π β (β€ βm π) β¦ (πβπ)) |
37 | | fvex 6904 |
. . . . . . . . 9
β’ ((π¦ β π β¦ (πΊβπ₯))βπ) β V |
38 | 35, 36, 37 | fvmpt 6998 |
. . . . . . . 8
β’ ((π¦ β π β¦ (πΊβπ₯)) β (β€ βm π) β ((π β (β€ βm π) β¦ (πβπ))β(π¦ β π β¦ (πΊβπ₯))) = ((π¦ β π β¦ (πΊβπ₯))βπ)) |
39 | 34, 38 | syl 17 |
. . . . . . 7
β’ ((((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β π) β§ π₯ β (β€ βm π)) β ((π β (β€ βm π) β¦ (πβπ))β(π¦ β π β¦ (πΊβπ₯))) = ((π¦ β π β¦ (πΊβπ₯))βπ)) |
40 | | simplr 767 |
. . . . . . . 8
β’ ((((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β π) β§ π₯ β (β€ βm π)) β π β π) |
41 | | fvex 6904 |
. . . . . . . 8
β’
(β¦π /
π¦β¦πΊβπ₯) β V |
42 | | csbeq1 3896 |
. . . . . . . . . 10
β’ (π = π β β¦π / π¦β¦πΊ = β¦π / π¦β¦πΊ) |
43 | 42 | fveq1d 6893 |
. . . . . . . . 9
β’ (π = π β (β¦π / π¦β¦πΊβπ₯) = (β¦π / π¦β¦πΊβπ₯)) |
44 | | nfcv 2903 |
. . . . . . . . . 10
β’
β²π(πΊβπ₯) |
45 | | nfcsb1v 3918 |
. . . . . . . . . . 11
β’
β²π¦β¦π / π¦β¦πΊ |
46 | | nfcv 2903 |
. . . . . . . . . . 11
β’
β²π¦π₯ |
47 | 45, 46 | nffv 6901 |
. . . . . . . . . 10
β’
β²π¦(β¦π / π¦β¦πΊβπ₯) |
48 | | csbeq1a 3907 |
. . . . . . . . . . 11
β’ (π¦ = π β πΊ = β¦π / π¦β¦πΊ) |
49 | 48 | fveq1d 6893 |
. . . . . . . . . 10
β’ (π¦ = π β (πΊβπ₯) = (β¦π / π¦β¦πΊβπ₯)) |
50 | 44, 47, 49 | cbvmpt 5259 |
. . . . . . . . 9
β’ (π¦ β π β¦ (πΊβπ₯)) = (π β π β¦ (β¦π / π¦β¦πΊβπ₯)) |
51 | 43, 50 | fvmptg 6996 |
. . . . . . . 8
β’ ((π β π β§ (β¦π / π¦β¦πΊβπ₯) β V) β ((π¦ β π β¦ (πΊβπ₯))βπ) = (β¦π / π¦β¦πΊβπ₯)) |
52 | 40, 41, 51 | sylancl 586 |
. . . . . . 7
β’ ((((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β π) β§ π₯ β (β€ βm π)) β ((π¦ β π β¦ (πΊβπ₯))βπ) = (β¦π / π¦β¦πΊβπ₯)) |
53 | 39, 52 | eqtrd 2772 |
. . . . . 6
β’ ((((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β π) β§ π₯ β (β€ βm π)) β ((π β (β€ βm π) β¦ (πβπ))β(π¦ β π β¦ (πΊβπ₯))) = (β¦π / π¦β¦πΊβπ₯)) |
54 | 53 | mpteq2dva 5248 |
. . . . 5
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β π) β (π₯ β (β€ βm π) β¦ ((π β (β€ βm π) β¦ (πβπ))β(π¦ β π β¦ (πΊβπ₯)))) = (π₯ β (β€ βm π) β¦ (β¦π / π¦β¦πΊβπ₯))) |
55 | | simpr 485 |
. . . . . . . 8
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β π) β π β π) |
56 | | simpl3 1193 |
. . . . . . . 8
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β π) β βπ¦ β π πΊ β (mzPolyβπ)) |
57 | | nfcsb1v 3918 |
. . . . . . . . . 10
β’
β²π¦β¦π / π¦β¦πΊ |
58 | 57 | nfel1 2919 |
. . . . . . . . 9
β’
β²π¦β¦π / π¦β¦πΊ β (mzPolyβπ) |
59 | | csbeq1a 3907 |
. . . . . . . . . 10
β’ (π¦ = π β πΊ = β¦π / π¦β¦πΊ) |
60 | 59 | eleq1d 2818 |
. . . . . . . . 9
β’ (π¦ = π β (πΊ β (mzPolyβπ) β β¦π / π¦β¦πΊ β (mzPolyβπ))) |
61 | 58, 60 | rspc 3600 |
. . . . . . . 8
β’ (π β π β (βπ¦ β π πΊ β (mzPolyβπ) β β¦π / π¦β¦πΊ β (mzPolyβπ))) |
62 | 55, 56, 61 | sylc 65 |
. . . . . . 7
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β π) β β¦π / π¦β¦πΊ β (mzPolyβπ)) |
63 | | mzpf 41464 |
. . . . . . 7
β’
(β¦π /
π¦β¦πΊ β (mzPolyβπ) β β¦π / π¦β¦πΊ:(β€ βm π)βΆβ€) |
64 | 62, 63 | syl 17 |
. . . . . 6
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β π) β β¦π / π¦β¦πΊ:(β€ βm π)βΆβ€) |
65 | 64 | feqmptd 6960 |
. . . . 5
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β π) β β¦π / π¦β¦πΊ = (π₯ β (β€ βm π) β¦ (β¦π / π¦β¦πΊβπ₯))) |
66 | 54, 65 | eqtr4d 2775 |
. . . 4
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β π) β (π₯ β (β€ βm π) β¦ ((π β (β€ βm π) β¦ (πβπ))β(π¦ β π β¦ (πΊβπ₯)))) = β¦π / π¦β¦πΊ) |
67 | 66, 62 | eqeltrd 2833 |
. . 3
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ π β π) β (π₯ β (β€ βm π) β¦ ((π β (β€ βm π) β¦ (πβπ))β(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) |
68 | | simp2l 1199 |
. . . . . 6
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) β π:(β€ βm π)βΆβ€) |
69 | 68 | ffnd 6718 |
. . . . 5
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) β π Fn (β€ βm π)) |
70 | | simp3l 1201 |
. . . . . 6
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) β π:(β€ βm π)βΆβ€) |
71 | 70 | ffnd 6718 |
. . . . 5
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) β π Fn (β€ βm π)) |
72 | | simp13 1205 |
. . . . 5
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) β βπ¦ β π πΊ β (mzPolyβπ)) |
73 | | simp12 1204 |
. . . . 5
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) β π β V) |
74 | | simplll 773 |
. . . . . . 7
β’ ((((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ (βπ¦ β π πΊ β (mzPolyβπ) β§ π β V)) β§ π₯ β (β€ βm π)) β π Fn (β€ βm π)) |
75 | | simpllr 774 |
. . . . . . 7
β’ ((((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ (βπ¦ β π πΊ β (mzPolyβπ) β§ π β V)) β§ π₯ β (β€ βm π)) β π Fn (β€ βm π)) |
76 | | ovexd 7443 |
. . . . . . 7
β’ ((((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ (βπ¦ β π πΊ β (mzPolyβπ) β§ π β V)) β§ π₯ β (β€ βm π)) β (β€
βm π)
β V) |
77 | | simpr 485 |
. . . . . . . . . 10
β’ ((((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ (βπ¦ β π πΊ β (mzPolyβπ) β§ π β V)) β§ π₯ β (β€ βm π)) β π₯ β (β€ βm π)) |
78 | | simplrl 775 |
. . . . . . . . . 10
β’ ((((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ (βπ¦ β π πΊ β (mzPolyβπ) β§ π β V)) β§ π₯ β (β€ βm π)) β βπ¦ β π πΊ β (mzPolyβπ)) |
79 | 77, 78, 12 | sylc 65 |
. . . . . . . . 9
β’ ((((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ (βπ¦ β π πΊ β (mzPolyβπ) β§ π β V)) β§ π₯ β (β€ βm π)) β βπ¦ β π (πΊβπ₯) β β€) |
80 | 79, 15 | sylib 217 |
. . . . . . . 8
β’ ((((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ (βπ¦ β π πΊ β (mzPolyβπ) β§ π β V)) β§ π₯ β (β€ βm π)) β (π¦ β π β¦ (πΊβπ₯)):πβΆβ€) |
81 | | simplrr 776 |
. . . . . . . . 9
β’ ((((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ (βπ¦ β π πΊ β (mzPolyβπ) β§ π β V)) β§ π₯ β (β€ βm π)) β π β V) |
82 | 18, 81, 20 | sylancr 587 |
. . . . . . . 8
β’ ((((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ (βπ¦ β π πΊ β (mzPolyβπ) β§ π β V)) β§ π₯ β (β€ βm π)) β ((π¦ β π β¦ (πΊβπ₯)) β (β€ βm π) β (π¦ β π β¦ (πΊβπ₯)):πβΆβ€)) |
83 | 80, 82 | mpbird 256 |
. . . . . . 7
β’ ((((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ (βπ¦ β π πΊ β (mzPolyβπ) β§ π β V)) β§ π₯ β (β€ βm π)) β (π¦ β π β¦ (πΊβπ₯)) β (β€ βm π)) |
84 | | fnfvof 7686 |
. . . . . . 7
β’ (((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ ((β€
βm π)
β V β§ (π¦ β
π β¦ (πΊβπ₯)) β (β€ βm π))) β ((π βf + π)β(π¦ β π β¦ (πΊβπ₯))) = ((πβ(π¦ β π β¦ (πΊβπ₯))) + (πβ(π¦ β π β¦ (πΊβπ₯))))) |
85 | 74, 75, 76, 83, 84 | syl22anc 837 |
. . . . . 6
β’ ((((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ (βπ¦ β π πΊ β (mzPolyβπ) β§ π β V)) β§ π₯ β (β€ βm π)) β ((π βf + π)β(π¦ β π β¦ (πΊβπ₯))) = ((πβ(π¦ β π β¦ (πΊβπ₯))) + (πβ(π¦ β π β¦ (πΊβπ₯))))) |
86 | 85 | mpteq2dva 5248 |
. . . . 5
β’ (((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ (βπ¦ β π πΊ β (mzPolyβπ) β§ π β V)) β (π₯ β (β€ βm π) β¦ ((π βf + π)β(π¦ β π β¦ (πΊβπ₯)))) = (π₯ β (β€ βm π) β¦ ((πβ(π¦ β π β¦ (πΊβπ₯))) + (πβ(π¦ β π β¦ (πΊβπ₯)))))) |
87 | 69, 71, 72, 73, 86 | syl22anc 837 |
. . . 4
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) β (π₯ β (β€ βm π) β¦ ((π βf + π)β(π¦ β π β¦ (πΊβπ₯)))) = (π₯ β (β€ βm π) β¦ ((πβ(π¦ β π β¦ (πΊβπ₯))) + (πβ(π¦ β π β¦ (πΊβπ₯)))))) |
88 | | simp2r 1200 |
. . . . 5
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) β (π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) |
89 | | simp3r 1202 |
. . . . 5
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) β (π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) |
90 | | mzpaddmpt 41469 |
. . . . 5
β’ (((π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ) β§ (π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) β (π₯ β (β€ βm π) β¦ ((πβ(π¦ β π β¦ (πΊβπ₯))) + (πβ(π¦ β π β¦ (πΊβπ₯))))) β (mzPolyβπ)) |
91 | 88, 89, 90 | syl2anc 584 |
. . . 4
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) β (π₯ β (β€ βm π) β¦ ((πβ(π¦ β π β¦ (πΊβπ₯))) + (πβ(π¦ β π β¦ (πΊβπ₯))))) β (mzPolyβπ)) |
92 | 87, 91 | eqeltrd 2833 |
. . 3
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) β (π₯ β (β€ βm π) β¦ ((π βf + π)β(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) |
93 | | fnfvof 7686 |
. . . . . . 7
β’ (((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ ((β€
βm π)
β V β§ (π¦ β
π β¦ (πΊβπ₯)) β (β€ βm π))) β ((π βf Β· π)β(π¦ β π β¦ (πΊβπ₯))) = ((πβ(π¦ β π β¦ (πΊβπ₯))) Β· (πβ(π¦ β π β¦ (πΊβπ₯))))) |
94 | 74, 75, 76, 83, 93 | syl22anc 837 |
. . . . . 6
β’ ((((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ (βπ¦ β π πΊ β (mzPolyβπ) β§ π β V)) β§ π₯ β (β€ βm π)) β ((π βf Β· π)β(π¦ β π β¦ (πΊβπ₯))) = ((πβ(π¦ β π β¦ (πΊβπ₯))) Β· (πβ(π¦ β π β¦ (πΊβπ₯))))) |
95 | 94 | mpteq2dva 5248 |
. . . . 5
β’ (((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ (βπ¦ β π πΊ β (mzPolyβπ) β§ π β V)) β (π₯ β (β€ βm π) β¦ ((π βf Β· π)β(π¦ β π β¦ (πΊβπ₯)))) = (π₯ β (β€ βm π) β¦ ((πβ(π¦ β π β¦ (πΊβπ₯))) Β· (πβ(π¦ β π β¦ (πΊβπ₯)))))) |
96 | 69, 71, 72, 73, 95 | syl22anc 837 |
. . . 4
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) β (π₯ β (β€ βm π) β¦ ((π βf Β· π)β(π¦ β π β¦ (πΊβπ₯)))) = (π₯ β (β€ βm π) β¦ ((πβ(π¦ β π β¦ (πΊβπ₯))) Β· (πβ(π¦ β π β¦ (πΊβπ₯)))))) |
97 | | mzpmulmpt 41470 |
. . . . 5
β’ (((π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ) β§ (π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) β (π₯ β (β€ βm π) β¦ ((πβ(π¦ β π β¦ (πΊβπ₯))) Β· (πβ(π¦ β π β¦ (πΊβπ₯))))) β (mzPolyβπ)) |
98 | 88, 89, 97 | syl2anc 584 |
. . . 4
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) β (π₯ β (β€ βm π) β¦ ((πβ(π¦ β π β¦ (πΊβπ₯))) Β· (πβ(π¦ β π β¦ (πΊβπ₯))))) β (mzPolyβπ)) |
99 | 96, 98 | eqeltrd 2833 |
. . 3
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) β§ (π:(β€ βm π)βΆβ€ β§ (π₯ β (β€
βm π)
β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) β (π₯ β (β€ βm π) β¦ ((π βf Β· π)β(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) |
100 | | fveq1 6890 |
. . . . 5
β’ (π = ((β€ βm
π) Γ {π}) β (πβ(π¦ β π β¦ (πΊβπ₯))) = (((β€ βm π) Γ {π})β(π¦ β π β¦ (πΊβπ₯)))) |
101 | 100 | mpteq2dv 5250 |
. . . 4
β’ (π = ((β€ βm
π) Γ {π}) β (π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) = (π₯ β (β€ βm π) β¦ (((β€
βm π)
Γ {π})β(π¦ β π β¦ (πΊβπ₯))))) |
102 | 101 | eleq1d 2818 |
. . 3
β’ (π = ((β€ βm
π) Γ {π}) β ((π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ (((β€
βm π)
Γ {π})β(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) |
103 | | fveq1 6890 |
. . . . 5
β’ (π = (π β (β€ βm π) β¦ (πβπ)) β (πβ(π¦ β π β¦ (πΊβπ₯))) = ((π β (β€ βm π) β¦ (πβπ))β(π¦ β π β¦ (πΊβπ₯)))) |
104 | 103 | mpteq2dv 5250 |
. . . 4
β’ (π = (π β (β€ βm π) β¦ (πβπ)) β (π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) = (π₯ β (β€ βm π) β¦ ((π β (β€ βm π) β¦ (πβπ))β(π¦ β π β¦ (πΊβπ₯))))) |
105 | 104 | eleq1d 2818 |
. . 3
β’ (π = (π β (β€ βm π) β¦ (πβπ)) β ((π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ ((π β (β€ βm π) β¦ (πβπ))β(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) |
106 | | fveq1 6890 |
. . . . 5
β’ (π = π β (πβ(π¦ β π β¦ (πΊβπ₯))) = (πβ(π¦ β π β¦ (πΊβπ₯)))) |
107 | 106 | mpteq2dv 5250 |
. . . 4
β’ (π = π β (π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) = (π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯))))) |
108 | 107 | eleq1d 2818 |
. . 3
β’ (π = π β ((π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) |
109 | | fveq1 6890 |
. . . . 5
β’ (π = π β (πβ(π¦ β π β¦ (πΊβπ₯))) = (πβ(π¦ β π β¦ (πΊβπ₯)))) |
110 | 109 | mpteq2dv 5250 |
. . . 4
β’ (π = π β (π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) = (π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯))))) |
111 | 110 | eleq1d 2818 |
. . 3
β’ (π = π β ((π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) |
112 | | fveq1 6890 |
. . . . 5
β’ (π = (π βf + π) β (πβ(π¦ β π β¦ (πΊβπ₯))) = ((π βf + π)β(π¦ β π β¦ (πΊβπ₯)))) |
113 | 112 | mpteq2dv 5250 |
. . . 4
β’ (π = (π βf + π) β (π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) = (π₯ β (β€ βm π) β¦ ((π βf + π)β(π¦ β π β¦ (πΊβπ₯))))) |
114 | 113 | eleq1d 2818 |
. . 3
β’ (π = (π βf + π) β ((π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ ((π βf + π)β(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) |
115 | | fveq1 6890 |
. . . . 5
β’ (π = (π βf Β· π) β (πβ(π¦ β π β¦ (πΊβπ₯))) = ((π βf Β· π)β(π¦ β π β¦ (πΊβπ₯)))) |
116 | 115 | mpteq2dv 5250 |
. . . 4
β’ (π = (π βf Β· π) β (π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) = (π₯ β (β€ βm π) β¦ ((π βf Β· π)β(π¦ β π β¦ (πΊβπ₯))))) |
117 | 116 | eleq1d 2818 |
. . 3
β’ (π = (π βf Β· π) β ((π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ ((π βf Β· π)β(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) |
118 | | fveq1 6890 |
. . . . 5
β’ (π = πΉ β (πβ(π¦ β π β¦ (πΊβπ₯))) = (πΉβ(π¦ β π β¦ (πΊβπ₯)))) |
119 | 118 | mpteq2dv 5250 |
. . . 4
β’ (π = πΉ β (π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) = (π₯ β (β€ βm π) β¦ (πΉβ(π¦ β π β¦ (πΊβπ₯))))) |
120 | 119 | eleq1d 2818 |
. . 3
β’ (π = πΉ β ((π₯ β (β€ βm π) β¦ (πβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ (πΉβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ))) |
121 | 30, 67, 92, 99, 102, 105, 108, 111, 114, 117, 120 | mzpindd 41474 |
. 2
β’ (((π β V β§ π β V β§ βπ¦ β π πΊ β (mzPolyβπ)) β§ πΉ β (mzPolyβπ)) β (π₯ β (β€ βm π) β¦ (πΉβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) |
122 | 1, 3, 4, 5, 121 | syl31anc 1373 |
1
β’ ((π β V β§ πΉ β (mzPolyβπ) β§ βπ¦ β π πΊ β (mzPolyβπ)) β (π₯ β (β€ βm π) β¦ (πΉβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) |