Step | Hyp | Ref
| Expression |
1 | | oveq2 7419 |
. . . 4
β’ (π£ = π β (β€ βm π£) = (β€ βm
π)) |
2 | 1 | oveq2d 7427 |
. . 3
β’ (π£ = π β (β€ βm (β€
βm π£)) =
(β€ βm (β€ βm π))) |
3 | | fveq2 6891 |
. . 3
β’ (π£ = π β (mzPolyCldβπ£) = (mzPolyCldβπ)) |
4 | 2, 3 | eleq12d 2827 |
. 2
β’ (π£ = π β ((β€ βm
(β€ βm π£)) β (mzPolyCldβπ£) β (β€ βm (β€
βm π))
β (mzPolyCldβπ))) |
5 | | ssid 4004 |
. . 3
β’ (β€
βm (β€ βm π£)) β (β€ βm
(β€ βm π£)) |
6 | | ovex 7444 |
. . . . . . 7
β’ (β€
βm π£)
β V |
7 | | zex 12569 |
. . . . . . 7
β’ β€
β V |
8 | 6, 7 | constmap 41533 |
. . . . . 6
β’ (π β β€ β ((β€
βm π£)
Γ {π}) β
(β€ βm (β€ βm π£))) |
9 | 8 | rgen 3063 |
. . . . 5
β’
βπ β
β€ ((β€ βm π£) Γ {π}) β (β€ βm
(β€ βm π£)) |
10 | | vex 3478 |
. . . . . . . . . . 11
β’ π£ β V |
11 | 7, 10 | elmap 8867 |
. . . . . . . . . 10
β’ (π β (β€
βm π£)
β π:π£βΆβ€) |
12 | | ffvelcdm 7083 |
. . . . . . . . . 10
β’ ((π:π£βΆβ€ β§ π β π£) β (πβπ) β β€) |
13 | 11, 12 | sylanb 581 |
. . . . . . . . 9
β’ ((π β (β€
βm π£) β§
π β π£) β (πβπ) β β€) |
14 | 13 | ancoms 459 |
. . . . . . . 8
β’ ((π β π£ β§ π β (β€ βm π£)) β (πβπ) β β€) |
15 | 14 | fmpttd 7116 |
. . . . . . 7
β’ (π β π£ β (π β (β€ βm π£) β¦ (πβπ)):(β€ βm π£)βΆβ€) |
16 | 7, 6 | elmap 8867 |
. . . . . . 7
β’ ((π β (β€
βm π£)
β¦ (πβπ)) β (β€
βm (β€ βm π£)) β (π β (β€ βm π£) β¦ (πβπ)):(β€ βm π£)βΆβ€) |
17 | 15, 16 | sylibr 233 |
. . . . . 6
β’ (π β π£ β (π β (β€ βm π£) β¦ (πβπ)) β (β€ βm
(β€ βm π£))) |
18 | 17 | rgen 3063 |
. . . . 5
β’
βπ β
π£ (π β (β€ βm π£) β¦ (πβπ)) β (β€ βm
(β€ βm π£)) |
19 | 9, 18 | pm3.2i 471 |
. . . 4
β’
(βπ β
β€ ((β€ βm π£) Γ {π}) β (β€ βm
(β€ βm π£)) β§ βπ β π£ (π β (β€ βm π£) β¦ (πβπ)) β (β€ βm
(β€ βm π£))) |
20 | | zaddcl 12604 |
. . . . . . . . 9
β’ ((π β β€ β§ π β β€) β (π + π) β β€) |
21 | 20 | adantl 482 |
. . . . . . . 8
β’ (((π:(β€ βm
π£)βΆβ€ β§
π:(β€
βm π£)βΆβ€) β§ (π β β€ β§ π β β€)) β (π + π) β β€) |
22 | | simpl 483 |
. . . . . . . 8
β’ ((π:(β€ βm
π£)βΆβ€ β§
π:(β€
βm π£)βΆβ€) β π:(β€ βm π£)βΆβ€) |
23 | | simpr 485 |
. . . . . . . 8
β’ ((π:(β€ βm
π£)βΆβ€ β§
π:(β€
βm π£)βΆβ€) β π:(β€ βm π£)βΆβ€) |
24 | | ovexd 7446 |
. . . . . . . 8
β’ ((π:(β€ βm
π£)βΆβ€ β§
π:(β€
βm π£)βΆβ€) β (β€
βm π£)
β V) |
25 | | inidm 4218 |
. . . . . . . 8
β’ ((β€
βm π£) β©
(β€ βm π£)) = (β€ βm π£) |
26 | 21, 22, 23, 24, 24, 25 | off 7690 |
. . . . . . 7
β’ ((π:(β€ βm
π£)βΆβ€ β§
π:(β€
βm π£)βΆβ€) β (π βf + π):(β€ βm π£)βΆβ€) |
27 | | zmulcl 12613 |
. . . . . . . . 9
β’ ((π β β€ β§ π β β€) β (π Β· π) β β€) |
28 | 27 | adantl 482 |
. . . . . . . 8
β’ (((π:(β€ βm
π£)βΆβ€ β§
π:(β€
βm π£)βΆβ€) β§ (π β β€ β§ π β β€)) β (π Β· π) β β€) |
29 | 28, 22, 23, 24, 24, 25 | off 7690 |
. . . . . . 7
β’ ((π:(β€ βm
π£)βΆβ€ β§
π:(β€
βm π£)βΆβ€) β (π βf Β· π):(β€ βm
π£)βΆβ€) |
30 | 26, 29 | jca 512 |
. . . . . 6
β’ ((π:(β€ βm
π£)βΆβ€ β§
π:(β€
βm π£)βΆβ€) β ((π βf + π):(β€ βm π£)βΆβ€ β§ (π βf Β·
π):(β€
βm π£)βΆβ€)) |
31 | 7, 6 | elmap 8867 |
. . . . . . 7
β’ (π β (β€
βm (β€ βm π£)) β π:(β€ βm π£)βΆβ€) |
32 | 7, 6 | elmap 8867 |
. . . . . . 7
β’ (π β (β€
βm (β€ βm π£)) β π:(β€ βm π£)βΆβ€) |
33 | 31, 32 | anbi12i 627 |
. . . . . 6
β’ ((π β (β€
βm (β€ βm π£)) β§ π β (β€ βm (β€
βm π£)))
β (π:(β€
βm π£)βΆβ€ β§ π:(β€ βm π£)βΆβ€)) |
34 | 7, 6 | elmap 8867 |
. . . . . . 7
β’ ((π βf + π) β (β€
βm (β€ βm π£)) β (π βf + π):(β€ βm π£)βΆβ€) |
35 | 7, 6 | elmap 8867 |
. . . . . . 7
β’ ((π βf Β·
π) β (β€
βm (β€ βm π£)) β (π βf Β· π):(β€ βm
π£)βΆβ€) |
36 | 34, 35 | anbi12i 627 |
. . . . . 6
β’ (((π βf + π) β (β€
βm (β€ βm π£)) β§ (π βf Β· π) β (β€
βm (β€ βm π£))) β ((π βf + π):(β€ βm π£)βΆβ€ β§ (π βf Β·
π):(β€
βm π£)βΆβ€)) |
37 | 30, 33, 36 | 3imtr4i 291 |
. . . . 5
β’ ((π β (β€
βm (β€ βm π£)) β§ π β (β€ βm (β€
βm π£)))
β ((π
βf + π)
β (β€ βm (β€ βm π£)) β§ (π βf Β· π) β (β€
βm (β€ βm π£)))) |
38 | 37 | rgen2 3197 |
. . . 4
β’
βπ β
(β€ βm (β€ βm π£))βπ β (β€ βm (β€
βm π£))((π βf + π) β (β€ βm (β€
βm π£))
β§ (π
βf Β· π) β (β€ βm (β€
βm π£))) |
39 | 19, 38 | pm3.2i 471 |
. . 3
β’
((βπ β
β€ ((β€ βm π£) Γ {π}) β (β€ βm
(β€ βm π£)) β§ βπ β π£ (π β (β€ βm π£) β¦ (πβπ)) β (β€ βm
(β€ βm π£))) β§ βπ β (β€ βm (β€
βm π£))βπ β (β€ βm (β€
βm π£))((π βf + π) β (β€ βm (β€
βm π£))
β§ (π
βf Β· π) β (β€ βm (β€
βm π£)))) |
40 | | elmzpcl 41546 |
. . . 4
β’ (π£ β V β ((β€
βm (β€ βm π£)) β (mzPolyCldβπ£) β ((β€ βm
(β€ βm π£)) β (β€ βm
(β€ βm π£)) β§ ((βπ β β€ ((β€ βm
π£) Γ {π}) β (β€
βm (β€ βm π£)) β§ βπ β π£ (π β (β€ βm π£) β¦ (πβπ)) β (β€ βm
(β€ βm π£))) β§ βπ β (β€ βm (β€
βm π£))βπ β (β€ βm (β€
βm π£))((π βf + π) β (β€ βm (β€
βm π£))
β§ (π
βf Β· π) β (β€ βm (β€
βm π£))))))) |
41 | 10, 40 | ax-mp 5 |
. . 3
β’ ((β€
βm (β€ βm π£)) β (mzPolyCldβπ£) β ((β€ βm
(β€ βm π£)) β (β€ βm
(β€ βm π£)) β§ ((βπ β β€ ((β€ βm
π£) Γ {π}) β (β€
βm (β€ βm π£)) β§ βπ β π£ (π β (β€ βm π£) β¦ (πβπ)) β (β€ βm
(β€ βm π£))) β§ βπ β (β€ βm (β€
βm π£))βπ β (β€ βm (β€
βm π£))((π βf + π) β (β€ βm (β€
βm π£))
β§ (π
βf Β· π) β (β€ βm (β€
βm π£)))))) |
42 | 5, 39, 41 | mpbir2an 709 |
. 2
β’ (β€
βm (β€ βm π£)) β (mzPolyCldβπ£) |
43 | 4, 42 | vtoclg 3556 |
1
β’ (π β V β (β€
βm (β€ βm π)) β (mzPolyCldβπ)) |