Metamath Proof Explorer


Theorem plymul0or

Description: Polynomial multiplication has no zero divisors. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Assertion plymul0or
|- ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( F oF x. G ) = 0p <-> ( F = 0p \/ G = 0p ) ) )

Proof

Step Hyp Ref Expression
1 dgrcl
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
2 dgrcl
 |-  ( G e. ( Poly ` S ) -> ( deg ` G ) e. NN0 )
3 nn0addcl
 |-  ( ( ( deg ` F ) e. NN0 /\ ( deg ` G ) e. NN0 ) -> ( ( deg ` F ) + ( deg ` G ) ) e. NN0 )
4 1 2 3 syl2an
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( deg ` F ) + ( deg ` G ) ) e. NN0 )
5 c0ex
 |-  0 e. _V
6 5 fvconst2
 |-  ( ( ( deg ` F ) + ( deg ` G ) ) e. NN0 -> ( ( NN0 X. { 0 } ) ` ( ( deg ` F ) + ( deg ` G ) ) ) = 0 )
7 4 6 syl
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( NN0 X. { 0 } ) ` ( ( deg ` F ) + ( deg ` G ) ) ) = 0 )
8 fveq2
 |-  ( ( F oF x. G ) = 0p -> ( coeff ` ( F oF x. G ) ) = ( coeff ` 0p ) )
9 coe0
 |-  ( coeff ` 0p ) = ( NN0 X. { 0 } )
10 8 9 eqtrdi
 |-  ( ( F oF x. G ) = 0p -> ( coeff ` ( F oF x. G ) ) = ( NN0 X. { 0 } ) )
11 10 fveq1d
 |-  ( ( F oF x. G ) = 0p -> ( ( coeff ` ( F oF x. G ) ) ` ( ( deg ` F ) + ( deg ` G ) ) ) = ( ( NN0 X. { 0 } ) ` ( ( deg ` F ) + ( deg ` G ) ) ) )
12 11 eqeq1d
 |-  ( ( F oF x. G ) = 0p -> ( ( ( coeff ` ( F oF x. G ) ) ` ( ( deg ` F ) + ( deg ` G ) ) ) = 0 <-> ( ( NN0 X. { 0 } ) ` ( ( deg ` F ) + ( deg ` G ) ) ) = 0 ) )
13 7 12 syl5ibrcom
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( F oF x. G ) = 0p -> ( ( coeff ` ( F oF x. G ) ) ` ( ( deg ` F ) + ( deg ` G ) ) ) = 0 ) )
14 eqid
 |-  ( coeff ` F ) = ( coeff ` F )
15 eqid
 |-  ( coeff ` G ) = ( coeff ` G )
16 eqid
 |-  ( deg ` F ) = ( deg ` F )
17 eqid
 |-  ( deg ` G ) = ( deg ` G )
18 14 15 16 17 coemulhi
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( coeff ` ( F oF x. G ) ) ` ( ( deg ` F ) + ( deg ` G ) ) ) = ( ( ( coeff ` F ) ` ( deg ` F ) ) x. ( ( coeff ` G ) ` ( deg ` G ) ) ) )
19 18 eqeq1d
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( ( coeff ` ( F oF x. G ) ) ` ( ( deg ` F ) + ( deg ` G ) ) ) = 0 <-> ( ( ( coeff ` F ) ` ( deg ` F ) ) x. ( ( coeff ` G ) ` ( deg ` G ) ) ) = 0 ) )
20 14 coef3
 |-  ( F e. ( Poly ` S ) -> ( coeff ` F ) : NN0 --> CC )
21 20 adantr
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( coeff ` F ) : NN0 --> CC )
22 1 adantr
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( deg ` F ) e. NN0 )
23 21 22 ffvelrnd
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( coeff ` F ) ` ( deg ` F ) ) e. CC )
24 15 coef3
 |-  ( G e. ( Poly ` S ) -> ( coeff ` G ) : NN0 --> CC )
25 24 adantl
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( coeff ` G ) : NN0 --> CC )
26 2 adantl
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( deg ` G ) e. NN0 )
27 25 26 ffvelrnd
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( coeff ` G ) ` ( deg ` G ) ) e. CC )
28 23 27 mul0ord
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( ( ( coeff ` F ) ` ( deg ` F ) ) x. ( ( coeff ` G ) ` ( deg ` G ) ) ) = 0 <-> ( ( ( coeff ` F ) ` ( deg ` F ) ) = 0 \/ ( ( coeff ` G ) ` ( deg ` G ) ) = 0 ) ) )
29 19 28 bitrd
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( ( coeff ` ( F oF x. G ) ) ` ( ( deg ` F ) + ( deg ` G ) ) ) = 0 <-> ( ( ( coeff ` F ) ` ( deg ` F ) ) = 0 \/ ( ( coeff ` G ) ` ( deg ` G ) ) = 0 ) ) )
30 13 29 sylibd
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( F oF x. G ) = 0p -> ( ( ( coeff ` F ) ` ( deg ` F ) ) = 0 \/ ( ( coeff ` G ) ` ( deg ` G ) ) = 0 ) ) )
31 16 14 dgreq0
 |-  ( F e. ( Poly ` S ) -> ( F = 0p <-> ( ( coeff ` F ) ` ( deg ` F ) ) = 0 ) )
32 31 adantr
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F = 0p <-> ( ( coeff ` F ) ` ( deg ` F ) ) = 0 ) )
33 17 15 dgreq0
 |-  ( G e. ( Poly ` S ) -> ( G = 0p <-> ( ( coeff ` G ) ` ( deg ` G ) ) = 0 ) )
34 33 adantl
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( G = 0p <-> ( ( coeff ` G ) ` ( deg ` G ) ) = 0 ) )
35 32 34 orbi12d
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( F = 0p \/ G = 0p ) <-> ( ( ( coeff ` F ) ` ( deg ` F ) ) = 0 \/ ( ( coeff ` G ) ` ( deg ` G ) ) = 0 ) ) )
36 30 35 sylibrd
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( F oF x. G ) = 0p -> ( F = 0p \/ G = 0p ) ) )
37 cnex
 |-  CC e. _V
38 37 a1i
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> CC e. _V )
39 plyf
 |-  ( G e. ( Poly ` S ) -> G : CC --> CC )
40 39 adantl
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> G : CC --> CC )
41 0cnd
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> 0 e. CC )
42 mul02
 |-  ( x e. CC -> ( 0 x. x ) = 0 )
43 42 adantl
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ x e. CC ) -> ( 0 x. x ) = 0 )
44 38 40 41 41 43 caofid2
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( CC X. { 0 } ) oF x. G ) = ( CC X. { 0 } ) )
45 id
 |-  ( F = 0p -> F = 0p )
46 df-0p
 |-  0p = ( CC X. { 0 } )
47 45 46 eqtrdi
 |-  ( F = 0p -> F = ( CC X. { 0 } ) )
48 47 oveq1d
 |-  ( F = 0p -> ( F oF x. G ) = ( ( CC X. { 0 } ) oF x. G ) )
49 48 eqeq1d
 |-  ( F = 0p -> ( ( F oF x. G ) = ( CC X. { 0 } ) <-> ( ( CC X. { 0 } ) oF x. G ) = ( CC X. { 0 } ) ) )
50 44 49 syl5ibrcom
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F = 0p -> ( F oF x. G ) = ( CC X. { 0 } ) ) )
51 plyf
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
52 51 adantr
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> F : CC --> CC )
53 mul01
 |-  ( x e. CC -> ( x x. 0 ) = 0 )
54 53 adantl
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ x e. CC ) -> ( x x. 0 ) = 0 )
55 38 52 41 41 54 caofid1
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F oF x. ( CC X. { 0 } ) ) = ( CC X. { 0 } ) )
56 id
 |-  ( G = 0p -> G = 0p )
57 56 46 eqtrdi
 |-  ( G = 0p -> G = ( CC X. { 0 } ) )
58 57 oveq2d
 |-  ( G = 0p -> ( F oF x. G ) = ( F oF x. ( CC X. { 0 } ) ) )
59 58 eqeq1d
 |-  ( G = 0p -> ( ( F oF x. G ) = ( CC X. { 0 } ) <-> ( F oF x. ( CC X. { 0 } ) ) = ( CC X. { 0 } ) ) )
60 55 59 syl5ibrcom
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( G = 0p -> ( F oF x. G ) = ( CC X. { 0 } ) ) )
61 50 60 jaod
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( F = 0p \/ G = 0p ) -> ( F oF x. G ) = ( CC X. { 0 } ) ) )
62 46 eqeq2i
 |-  ( ( F oF x. G ) = 0p <-> ( F oF x. G ) = ( CC X. { 0 } ) )
63 61 62 syl6ibr
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( F = 0p \/ G = 0p ) -> ( F oF x. G ) = 0p ) )
64 36 63 impbid
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( F oF x. G ) = 0p <-> ( F = 0p \/ G = 0p ) ) )