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 ) ) )