Step |
Hyp |
Ref |
Expression |
1 |
|
elfvex |
|- ( A e. ( mzPoly ` V ) -> V e. _V ) |
2 |
1
|
adantr |
|- ( ( A e. ( mzPoly ` V ) /\ B e. ( mzPoly ` V ) ) -> V e. _V ) |
3 |
|
mzpincl |
|- ( V e. _V -> ( mzPoly ` V ) e. ( mzPolyCld ` V ) ) |
4 |
2 3
|
syl |
|- ( ( A e. ( mzPoly ` V ) /\ B e. ( mzPoly ` V ) ) -> ( mzPoly ` V ) e. ( mzPolyCld ` V ) ) |
5 |
|
mzpcl34 |
|- ( ( ( mzPoly ` V ) e. ( mzPolyCld ` V ) /\ A e. ( mzPoly ` V ) /\ B e. ( mzPoly ` V ) ) -> ( ( A oF + B ) e. ( mzPoly ` V ) /\ ( A oF x. B ) e. ( mzPoly ` V ) ) ) |
6 |
5
|
3expib |
|- ( ( mzPoly ` V ) e. ( mzPolyCld ` V ) -> ( ( A e. ( mzPoly ` V ) /\ B e. ( mzPoly ` V ) ) -> ( ( A oF + B ) e. ( mzPoly ` V ) /\ ( A oF x. B ) e. ( mzPoly ` V ) ) ) ) |
7 |
4 6
|
mpcom |
|- ( ( A e. ( mzPoly ` V ) /\ B e. ( mzPoly ` V ) ) -> ( ( A oF + B ) e. ( mzPoly ` V ) /\ ( A oF x. B ) e. ( mzPoly ` V ) ) ) |
8 |
7
|
simprd |
|- ( ( A e. ( mzPoly ` V ) /\ B e. ( mzPoly ` V ) ) -> ( A oF x. B ) e. ( mzPoly ` V ) ) |