Metamath Proof Explorer

Theorem mzpmulmpt

Description: Product of polynomial functions is polynomial. Maps-to version of mzpmulmpt . (Contributed by Stefan O'Rear, 5-Oct-2014)

Ref Expression
Assertion mzpmulmpt 
|- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( A x. B ) ) e. ( mzPoly ` V ) )

Proof

Step Hyp Ref Expression
1 mzpf 
 |-  ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> A ) : ( ZZ ^m V ) --> ZZ )
2 1 ffnd 
 |-  ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> A ) Fn ( ZZ ^m V ) )
3 mzpf 
 |-  ( ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> B ) : ( ZZ ^m V ) --> ZZ )
4 3 ffnd 
 |-  ( ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> B ) Fn ( ZZ ^m V ) )
5 ovex 
 |-  ( ZZ ^m V ) e. _V
6 ofmpteq 
 |-  ( ( ( ZZ ^m V ) e. _V /\ ( x e. ( ZZ ^m V ) |-> A ) Fn ( ZZ ^m V ) /\ ( x e. ( ZZ ^m V ) |-> B ) Fn ( ZZ ^m V ) ) -> ( ( x e. ( ZZ ^m V ) |-> A ) oF x. ( x e. ( ZZ ^m V ) |-> B ) ) = ( x e. ( ZZ ^m V ) |-> ( A x. B ) ) )
7 5 6 mp3an1 
 |-  ( ( ( x e. ( ZZ ^m V ) |-> A ) Fn ( ZZ ^m V ) /\ ( x e. ( ZZ ^m V ) |-> B ) Fn ( ZZ ^m V ) ) -> ( ( x e. ( ZZ ^m V ) |-> A ) oF x. ( x e. ( ZZ ^m V ) |-> B ) ) = ( x e. ( ZZ ^m V ) |-> ( A x. B ) ) )
8 2 4 7 syl2an 
 |-  ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) -> ( ( x e. ( ZZ ^m V ) |-> A ) oF x. ( x e. ( ZZ ^m V ) |-> B ) ) = ( x e. ( ZZ ^m V ) |-> ( A x. B ) ) )
9 mzpmul 
 |-  ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) -> ( ( x e. ( ZZ ^m V ) |-> A ) oF x. ( x e. ( ZZ ^m V ) |-> B ) ) e. ( mzPoly ` V ) )
10 8 9 eqeltrrd 
 |-  ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( A x. B ) ) e. ( mzPoly ` V ) )