Step | Hyp | Ref
| Expression |
1 | | elfvex 6881 |
. . 3
β’ (πΉ β (mzPolyβπ) β π β V) |
2 | 1 | 3anim1i 1153 |
. 2
β’ ((πΉ β (mzPolyβπ) β§ (π β (β€ βm π) β§ π β (β€ βm π)) β§ (π β β€ β§ βπ β π π β₯ ((πβπ) β (πβπ)))) β (π β V β§ (π β (β€ βm π) β§ π β (β€ βm π)) β§ (π β β€ β§ βπ β π π β₯ ((πβπ) β (πβπ))))) |
3 | | simp1 1137 |
. 2
β’ ((πΉ β (mzPolyβπ) β§ (π β (β€ βm π) β§ π β (β€ βm π)) β§ (π β β€ β§ βπ β π π β₯ ((πβπ) β (πβπ)))) β πΉ β (mzPolyβπ)) |
4 | | simpl3l 1229 |
. . . . 5
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ π β β€) β π β β€) |
5 | | simpr 486 |
. . . . 5
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ π β β€) β π β β€) |
6 | | congid 41338 |
. . . . 5
β’ ((π β β€ β§ π β β€) β π β₯ (π β π)) |
7 | 4, 5, 6 | syl2anc 585 |
. . . 4
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ π β β€) β π β₯ (π β π)) |
8 | | simpl2l 1227 |
. . . . . 6
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ π β β€) β π β (β€ βm π)) |
9 | | vex 3448 |
. . . . . . 7
β’ π β V |
10 | 9 | fvconst2 7154 |
. . . . . 6
β’ (π β (β€
βm π)
β (((β€ βm π) Γ {π})βπ) = π) |
11 | 8, 10 | syl 17 |
. . . . 5
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ π β β€) β (((β€
βm π)
Γ {π})βπ) = π) |
12 | | simpl2r 1228 |
. . . . . 6
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ π β β€) β π β (β€ βm π)) |
13 | 9 | fvconst2 7154 |
. . . . . 6
β’ (π β (β€
βm π)
β (((β€ βm π) Γ {π})βπ) = π) |
14 | 12, 13 | syl 17 |
. . . . 5
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ π β β€) β (((β€
βm π)
Γ {π})βπ) = π) |
15 | 11, 14 | oveq12d 7376 |
. . . 4
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ π β β€) β ((((β€
βm π)
Γ {π})βπ) β (((β€
βm π)
Γ {π})βπ)) = (π β π)) |
16 | 7, 15 | breqtrrd 5134 |
. . 3
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ π β β€) β π β₯ ((((β€ βm
π) Γ {π})βπ) β (((β€ βm
π) Γ {π})βπ))) |
17 | | simpr 486 |
. . . . 5
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ π β π) β π β π) |
18 | | simpl3r 1230 |
. . . . 5
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ π β π) β βπ β π π β₯ ((πβπ) β (πβπ))) |
19 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π β (πβπ) = (πβπ)) |
20 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π β (πβπ) = (πβπ)) |
21 | 19, 20 | oveq12d 7376 |
. . . . . . 7
β’ (π = π β ((πβπ) β (πβπ)) = ((πβπ) β (πβπ))) |
22 | 21 | breq2d 5118 |
. . . . . 6
β’ (π = π β (π β₯ ((πβπ) β (πβπ)) β π β₯ ((πβπ) β (πβπ)))) |
23 | 22 | rspcva 3578 |
. . . . 5
β’ ((π β π β§ βπ β π π β₯ ((πβπ) β (πβπ))) β π β₯ ((πβπ) β (πβπ))) |
24 | 17, 18, 23 | syl2anc 585 |
. . . 4
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ π β π) β π β₯ ((πβπ) β (πβπ))) |
25 | | simpl2l 1227 |
. . . . . 6
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ π β π) β π β (β€ βm π)) |
26 | | fveq1 6842 |
. . . . . . 7
β’ (π = π β (πβπ) = (πβπ)) |
27 | | eqid 2733 |
. . . . . . 7
β’ (π β (β€
βm π)
β¦ (πβπ)) = (π β (β€ βm π) β¦ (πβπ)) |
28 | | fvex 6856 |
. . . . . . 7
β’ (πβπ) β V |
29 | 26, 27, 28 | fvmpt 6949 |
. . . . . 6
β’ (π β (β€
βm π)
β ((π β (β€
βm π)
β¦ (πβπ))βπ) = (πβπ)) |
30 | 25, 29 | syl 17 |
. . . . 5
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ π β π) β ((π β (β€ βm π) β¦ (πβπ))βπ) = (πβπ)) |
31 | | simpl2r 1228 |
. . . . . 6
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ π β π) β π β (β€ βm π)) |
32 | | fveq1 6842 |
. . . . . . 7
β’ (π = π β (πβπ) = (πβπ)) |
33 | | fvex 6856 |
. . . . . . 7
β’ (πβπ) β V |
34 | 32, 27, 33 | fvmpt 6949 |
. . . . . 6
β’ (π β (β€
βm π)
β ((π β (β€
βm π)
β¦ (πβπ))βπ) = (πβπ)) |
35 | 31, 34 | syl 17 |
. . . . 5
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ π β π) β ((π β (β€ βm π) β¦ (πβπ))βπ) = (πβπ)) |
36 | 30, 35 | oveq12d 7376 |
. . . 4
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ π β π) β (((π β (β€ βm π) β¦ (πβπ))βπ) β ((π β (β€ βm π) β¦ (πβπ))βπ)) = ((πβπ) β (πβπ))) |
37 | 24, 36 | breqtrrd 5134 |
. . 3
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ π β π) β π β₯ (((π β (β€ βm π) β¦ (πβπ))βπ) β ((π β (β€ βm π) β¦ (πβπ))βπ))) |
38 | | simp13l 1289 |
. . . . 5
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β π β β€) |
39 | | simp2l 1200 |
. . . . . 6
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β π:(β€ βm π)βΆβ€) |
40 | | simp12l 1287 |
. . . . . 6
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β π β (β€ βm π)) |
41 | 39, 40 | ffvelcdmd 7037 |
. . . . 5
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β (πβπ) β β€) |
42 | | simp12r 1288 |
. . . . . 6
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β π β (β€ βm π)) |
43 | 39, 42 | ffvelcdmd 7037 |
. . . . 5
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β (πβπ) β β€) |
44 | | simp3l 1202 |
. . . . . 6
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β π:(β€ βm π)βΆβ€) |
45 | 44, 40 | ffvelcdmd 7037 |
. . . . 5
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β (πβπ) β β€) |
46 | 44, 42 | ffvelcdmd 7037 |
. . . . 5
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β (πβπ) β β€) |
47 | | simp2r 1201 |
. . . . 5
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β π β₯ ((πβπ) β (πβπ))) |
48 | | simp3r 1203 |
. . . . 5
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β π β₯ ((πβπ) β (πβπ))) |
49 | | congadd 41333 |
. . . . 5
β’ (((π β β€ β§ (πβπ) β β€ β§ (πβπ) β β€) β§ ((πβπ) β β€ β§ (πβπ) β β€) β§ (π β₯ ((πβπ) β (πβπ)) β§ π β₯ ((πβπ) β (πβπ)))) β π β₯ (((πβπ) + (πβπ)) β ((πβπ) + (πβπ)))) |
50 | 38, 41, 43, 45, 46, 47, 48, 49 | syl322anc 1399 |
. . . 4
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β π β₯ (((πβπ) + (πβπ)) β ((πβπ) + (πβπ)))) |
51 | 39 | ffnd 6670 |
. . . . . 6
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β π Fn (β€ βm π)) |
52 | 44 | ffnd 6670 |
. . . . . 6
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β π Fn (β€ βm π)) |
53 | | ovexd 7393 |
. . . . . 6
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β (β€ βm
π) β
V) |
54 | | fnfvof 7635 |
. . . . . 6
β’ (((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ ((β€
βm π)
β V β§ π β
(β€ βm π))) β ((π βf + π)βπ) = ((πβπ) + (πβπ))) |
55 | 51, 52, 53, 40, 54 | syl22anc 838 |
. . . . 5
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β ((π βf + π)βπ) = ((πβπ) + (πβπ))) |
56 | | fnfvof 7635 |
. . . . . 6
β’ (((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ ((β€
βm π)
β V β§ π β
(β€ βm π))) β ((π βf + π)βπ) = ((πβπ) + (πβπ))) |
57 | 51, 52, 53, 42, 56 | syl22anc 838 |
. . . . 5
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β ((π βf + π)βπ) = ((πβπ) + (πβπ))) |
58 | 55, 57 | oveq12d 7376 |
. . . 4
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β (((π βf + π)βπ) β ((π βf + π)βπ)) = (((πβπ) + (πβπ)) β ((πβπ) + (πβπ)))) |
59 | 50, 58 | breqtrrd 5134 |
. . 3
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β π β₯ (((π βf + π)βπ) β ((π βf + π)βπ))) |
60 | | congmul 41334 |
. . . . 5
β’ (((π β β€ β§ (πβπ) β β€ β§ (πβπ) β β€) β§ ((πβπ) β β€ β§ (πβπ) β β€) β§ (π β₯ ((πβπ) β (πβπ)) β§ π β₯ ((πβπ) β (πβπ)))) β π β₯ (((πβπ) Β· (πβπ)) β ((πβπ) Β· (πβπ)))) |
61 | 38, 41, 43, 45, 46, 47, 48, 60 | syl322anc 1399 |
. . . 4
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β π β₯ (((πβπ) Β· (πβπ)) β ((πβπ) Β· (πβπ)))) |
62 | | fnfvof 7635 |
. . . . . 6
β’ (((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ ((β€
βm π)
β V β§ π β
(β€ βm π))) β ((π βf Β· π)βπ) = ((πβπ) Β· (πβπ))) |
63 | 51, 52, 53, 40, 62 | syl22anc 838 |
. . . . 5
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β ((π βf Β· π)βπ) = ((πβπ) Β· (πβπ))) |
64 | | fnfvof 7635 |
. . . . . 6
β’ (((π Fn (β€ βm
π) β§ π Fn (β€ βm π)) β§ ((β€
βm π)
β V β§ π β
(β€ βm π))) β ((π βf Β· π)βπ) = ((πβπ) Β· (πβπ))) |
65 | 51, 52, 53, 42, 64 | syl22anc 838 |
. . . . 5
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β ((π βf Β· π)βπ) = ((πβπ) Β· (πβπ))) |
66 | 63, 65 | oveq12d 7376 |
. . . 4
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β (((π βf Β· π)βπ) β ((π βf Β· π)βπ)) = (((πβπ) Β· (πβπ)) β ((πβπ) Β· (πβπ)))) |
67 | 61, 66 | breqtrrd 5134 |
. . 3
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ))) β§ (π:(β€ βm π)βΆβ€ β§ π β₯ ((πβπ) β (πβπ)))) β π β₯ (((π βf Β· π)βπ) β ((π βf Β· π)βπ))) |
68 | | fveq1 6842 |
. . . . 5
β’ (π = ((β€ βm
π) Γ {π}) β (πβπ) = (((β€ βm π) Γ {π})βπ)) |
69 | | fveq1 6842 |
. . . . 5
β’ (π = ((β€ βm
π) Γ {π}) β (πβπ) = (((β€ βm π) Γ {π})βπ)) |
70 | 68, 69 | oveq12d 7376 |
. . . 4
β’ (π = ((β€ βm
π) Γ {π}) β ((πβπ) β (πβπ)) = ((((β€ βm π) Γ {π})βπ) β (((β€ βm
π) Γ {π})βπ))) |
71 | 70 | breq2d 5118 |
. . 3
β’ (π = ((β€ βm
π) Γ {π}) β (π β₯ ((πβπ) β (πβπ)) β π β₯ ((((β€ βm
π) Γ {π})βπ) β (((β€ βm
π) Γ {π})βπ)))) |
72 | | fveq1 6842 |
. . . . 5
β’ (π = (π β (β€ βm π) β¦ (πβπ)) β (πβπ) = ((π β (β€ βm π) β¦ (πβπ))βπ)) |
73 | | fveq1 6842 |
. . . . 5
β’ (π = (π β (β€ βm π) β¦ (πβπ)) β (πβπ) = ((π β (β€ βm π) β¦ (πβπ))βπ)) |
74 | 72, 73 | oveq12d 7376 |
. . . 4
β’ (π = (π β (β€ βm π) β¦ (πβπ)) β ((πβπ) β (πβπ)) = (((π β (β€ βm π) β¦ (πβπ))βπ) β ((π β (β€ βm π) β¦ (πβπ))βπ))) |
75 | 74 | breq2d 5118 |
. . 3
β’ (π = (π β (β€ βm π) β¦ (πβπ)) β (π β₯ ((πβπ) β (πβπ)) β π β₯ (((π β (β€ βm π) β¦ (πβπ))βπ) β ((π β (β€ βm π) β¦ (πβπ))βπ)))) |
76 | | fveq1 6842 |
. . . . 5
β’ (π = π β (πβπ) = (πβπ)) |
77 | | fveq1 6842 |
. . . . 5
β’ (π = π β (πβπ) = (πβπ)) |
78 | 76, 77 | oveq12d 7376 |
. . . 4
β’ (π = π β ((πβπ) β (πβπ)) = ((πβπ) β (πβπ))) |
79 | 78 | breq2d 5118 |
. . 3
β’ (π = π β (π β₯ ((πβπ) β (πβπ)) β π β₯ ((πβπ) β (πβπ)))) |
80 | | fveq1 6842 |
. . . . 5
β’ (π = π β (πβπ) = (πβπ)) |
81 | | fveq1 6842 |
. . . . 5
β’ (π = π β (πβπ) = (πβπ)) |
82 | 80, 81 | oveq12d 7376 |
. . . 4
β’ (π = π β ((πβπ) β (πβπ)) = ((πβπ) β (πβπ))) |
83 | 82 | breq2d 5118 |
. . 3
β’ (π = π β (π β₯ ((πβπ) β (πβπ)) β π β₯ ((πβπ) β (πβπ)))) |
84 | | fveq1 6842 |
. . . . 5
β’ (π = (π βf + π) β (πβπ) = ((π βf + π)βπ)) |
85 | | fveq1 6842 |
. . . . 5
β’ (π = (π βf + π) β (πβπ) = ((π βf + π)βπ)) |
86 | 84, 85 | oveq12d 7376 |
. . . 4
β’ (π = (π βf + π) β ((πβπ) β (πβπ)) = (((π βf + π)βπ) β ((π βf + π)βπ))) |
87 | 86 | breq2d 5118 |
. . 3
β’ (π = (π βf + π) β (π β₯ ((πβπ) β (πβπ)) β π β₯ (((π βf + π)βπ) β ((π βf + π)βπ)))) |
88 | | fveq1 6842 |
. . . . 5
β’ (π = (π βf Β· π) β (πβπ) = ((π βf Β· π)βπ)) |
89 | | fveq1 6842 |
. . . . 5
β’ (π = (π βf Β· π) β (πβπ) = ((π βf Β· π)βπ)) |
90 | 88, 89 | oveq12d 7376 |
. . . 4
β’ (π = (π βf Β· π) β ((πβπ) β (πβπ)) = (((π βf Β· π)βπ) β ((π βf Β· π)βπ))) |
91 | 90 | breq2d 5118 |
. . 3
β’ (π = (π βf Β· π) β (π β₯ ((πβπ) β (πβπ)) β π β₯ (((π βf Β· π)βπ) β ((π βf Β· π)βπ)))) |
92 | | fveq1 6842 |
. . . . 5
β’ (π = πΉ β (πβπ) = (πΉβπ)) |
93 | | fveq1 6842 |
. . . . 5
β’ (π = πΉ β (πβπ) = (πΉβπ)) |
94 | 92, 93 | oveq12d 7376 |
. . . 4
β’ (π = πΉ β ((πβπ) β (πβπ)) = ((πΉβπ) β (πΉβπ))) |
95 | 94 | breq2d 5118 |
. . 3
β’ (π = πΉ β (π β₯ ((πβπ) β (πβπ)) β π β₯ ((πΉβπ) β (πΉβπ)))) |
96 | 16, 37, 59, 67, 71, 75, 79, 83, 87, 91, 95 | mzpindd 41112 |
. 2
β’ (((π β V β§ (π β (β€
βm π) β§
π β (β€
βm π))
β§ (π β β€
β§ βπ β
π π β₯ ((πβπ) β (πβπ)))) β§ πΉ β (mzPolyβπ)) β π β₯ ((πΉβπ) β (πΉβπ))) |
97 | 2, 3, 96 | syl2anc 585 |
1
β’ ((πΉ β (mzPolyβπ) β§ (π β (β€ βm π) β§ π β (β€ βm π)) β§ (π β β€ β§ βπ β π π β₯ ((πβπ) β (πβπ)))) β π β₯ ((πΉβπ) β (πΉβπ))) |