Metamath Proof Explorer

Theorem ply1mulrtss

Description: The roots of a factor F are also roots of the product of polynomials ( F .x. G ) . (Contributed by Thierry Arnoux, 8-Jun-2025)

Ref Expression
Hypotheses ply1dg1rt.p 
|- P = ( Poly1 ` R )
ply1dg1rt.u 
|- U = ( Base ` P )
ply1dg1rt.o 
|- O = ( eval1 ` R )
ply1dg1rt.d 
|- D = ( deg1 ` R )
ply1dg1rt.0 
|- .0. = ( 0g ` R )
ply1mulrtss.r 
|- ( ph -> R e. CRing )
ply1mulrtss.f 
|- ( ph -> F e. U )
ply1mulrtss.g 
|- ( ph -> G e. U )
ply1mulrtss.1 
|- .x. = ( .r ` P )
Assertion ply1mulrtss 
|- ( ph -> ( `' ( O ` F ) " { .0. } ) C_ ( `' ( O ` ( F .x. G ) ) " { .0. } ) )

Proof

Step Hyp Ref Expression
1 ply1dg1rt.p 
 |-  P = ( Poly1 ` R )
2 ply1dg1rt.u 
 |-  U = ( Base ` P )
3 ply1dg1rt.o 
 |-  O = ( eval1 ` R )
4 ply1dg1rt.d 
 |-  D = ( deg1 ` R )
5 ply1dg1rt.0 
 |-  .0. = ( 0g ` R )
6 ply1mulrtss.r 
 |-  ( ph -> R e. CRing )
7 ply1mulrtss.f 
 |-  ( ph -> F e. U )
8 ply1mulrtss.g 
 |-  ( ph -> G e. U )
9 ply1mulrtss.1 
 |-  .x. = ( .r ` P )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 3 1 2 6 10 7 evl1fvf 
 |-  ( ph -> ( O ` F ) : ( Base ` R ) --> ( Base ` R ) )
12 11 ffnd 
 |-  ( ph -> ( O ` F ) Fn ( Base ` R ) )
13 fniniseg2 
 |-  ( ( O ` F ) Fn ( Base ` R ) -> ( `' ( O ` F ) " { .0. } ) = { x e. ( Base ` R ) | ( ( O ` F ) ` x ) = .0. } )
14 12 13 syl 
 |-  ( ph -> ( `' ( O ` F ) " { .0. } ) = { x e. ( Base ` R ) | ( ( O ` F ) ` x ) = .0. } )
15 14 eleq2d 
 |-  ( ph -> ( x e. ( `' ( O ` F ) " { .0. } ) <-> x e. { x e. ( Base ` R ) | ( ( O ` F ) ` x ) = .0. } ) )
16 15 biimpa 
 |-  ( ( ph /\ x e. ( `' ( O ` F ) " { .0. } ) ) -> x e. { x e. ( Base ` R ) | ( ( O ` F ) ` x ) = .0. } )
17 rabid 
 |-  ( x e. { x e. ( Base ` R ) | ( ( O ` F ) ` x ) = .0. } <-> ( x e. ( Base ` R ) /\ ( ( O ` F ) ` x ) = .0. ) )
18 16 17 sylib 
 |-  ( ( ph /\ x e. ( `' ( O ` F ) " { .0. } ) ) -> ( x e. ( Base ` R ) /\ ( ( O ` F ) ` x ) = .0. ) )
19 18 simpld 
 |-  ( ( ph /\ x e. ( `' ( O ` F ) " { .0. } ) ) -> x e. ( Base ` R ) )
20 6 adantr 
 |-  ( ( ph /\ x e. ( `' ( O ` F ) " { .0. } ) ) -> R e. CRing )
21 7 adantr 
 |-  ( ( ph /\ x e. ( `' ( O ` F ) " { .0. } ) ) -> F e. U )
22 18 simprd 
 |-  ( ( ph /\ x e. ( `' ( O ` F ) " { .0. } ) ) -> ( ( O ` F ) ` x ) = .0. )
23 21 22 jca 
 |-  ( ( ph /\ x e. ( `' ( O ` F ) " { .0. } ) ) -> ( F e. U /\ ( ( O ` F ) ` x ) = .0. ) )
24 8 adantr 
 |-  ( ( ph /\ x e. ( `' ( O ` F ) " { .0. } ) ) -> G e. U )
25 eqidd 
 |-  ( ( ph /\ x e. ( `' ( O ` F ) " { .0. } ) ) -> ( ( O ` G ) ` x ) = ( ( O ` G ) ` x ) )
26 24 25 jca 
 |-  ( ( ph /\ x e. ( `' ( O ` F ) " { .0. } ) ) -> ( G e. U /\ ( ( O ` G ) ` x ) = ( ( O ` G ) ` x ) ) )
27 eqid 
 |-  ( .r ` R ) = ( .r ` R )
28 3 1 10 2 20 19 23 26 9 27 evl1muld 
 |-  ( ( ph /\ x e. ( `' ( O ` F ) " { .0. } ) ) -> ( ( F .x. G ) e. U /\ ( ( O ` ( F .x. G ) ) ` x ) = ( .0. ( .r ` R ) ( ( O ` G ) ` x ) ) ) )
29 28 simprd 
 |-  ( ( ph /\ x e. ( `' ( O ` F ) " { .0. } ) ) -> ( ( O ` ( F .x. G ) ) ` x ) = ( .0. ( .r ` R ) ( ( O ` G ) ` x ) ) )
30 20 crngringd 
 |-  ( ( ph /\ x e. ( `' ( O ` F ) " { .0. } ) ) -> R e. Ring )
31 3 1 10 2 20 19 24 fveval1fvcl 
 |-  ( ( ph /\ x e. ( `' ( O ` F ) " { .0. } ) ) -> ( ( O ` G ) ` x ) e. ( Base ` R ) )
32 10 27 5 30 31 ringlzd 
 |-  ( ( ph /\ x e. ( `' ( O ` F ) " { .0. } ) ) -> ( .0. ( .r ` R ) ( ( O ` G ) ` x ) ) = .0. )
33 29 32 eqtrd 
 |-  ( ( ph /\ x e. ( `' ( O ` F ) " { .0. } ) ) -> ( ( O ` ( F .x. G ) ) ` x ) = .0. )
34 19 33 jca 
 |-  ( ( ph /\ x e. ( `' ( O ` F ) " { .0. } ) ) -> ( x e. ( Base ` R ) /\ ( ( O ` ( F .x. G ) ) ` x ) = .0. ) )
35 rabid 
 |-  ( x e. { x e. ( Base ` R ) | ( ( O ` ( F .x. G ) ) ` x ) = .0. } <-> ( x e. ( Base ` R ) /\ ( ( O ` ( F .x. G ) ) ` x ) = .0. ) )
36 1 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
37 6 36 syl 
 |-  ( ph -> P e. CRing )
38 37 crngringd 
 |-  ( ph -> P e. Ring )
39 2 9 38 7 8 ringcld 
 |-  ( ph -> ( F .x. G ) e. U )
40 3 1 2 6 10 39 evl1fvf 
 |-  ( ph -> ( O ` ( F .x. G ) ) : ( Base ` R ) --> ( Base ` R ) )
41 40 ffnd 
 |-  ( ph -> ( O ` ( F .x. G ) ) Fn ( Base ` R ) )
42 fniniseg2 
 |-  ( ( O ` ( F .x. G ) ) Fn ( Base ` R ) -> ( `' ( O ` ( F .x. G ) ) " { .0. } ) = { x e. ( Base ` R ) | ( ( O ` ( F .x. G ) ) ` x ) = .0. } )
43 41 42 syl 
 |-  ( ph -> ( `' ( O ` ( F .x. G ) ) " { .0. } ) = { x e. ( Base ` R ) | ( ( O ` ( F .x. G ) ) ` x ) = .0. } )
44 43 eleq2d 
 |-  ( ph -> ( x e. ( `' ( O ` ( F .x. G ) ) " { .0. } ) <-> x e. { x e. ( Base ` R ) | ( ( O ` ( F .x. G ) ) ` x ) = .0. } ) )
45 44 biimpar 
 |-  ( ( ph /\ x e. { x e. ( Base ` R ) | ( ( O ` ( F .x. G ) ) ` x ) = .0. } ) -> x e. ( `' ( O ` ( F .x. G ) ) " { .0. } ) )
46 35 45 sylan2br 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ ( ( O ` ( F .x. G ) ) ` x ) = .0. ) ) -> x e. ( `' ( O ` ( F .x. G ) ) " { .0. } ) )
47 34 46 syldan 
 |-  ( ( ph /\ x e. ( `' ( O ` F ) " { .0. } ) ) -> x e. ( `' ( O ` ( F .x. G ) ) " { .0. } ) )
48 47 ex 
 |-  ( ph -> ( x e. ( `' ( O ` F ) " { .0. } ) -> x e. ( `' ( O ` ( F .x. G ) ) " { .0. } ) ) )
49 48 ssrdv 
 |-  ( ph -> ( `' ( O ` F ) " { .0. } ) C_ ( `' ( O ` ( F .x. G ) ) " { .0. } ) )