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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ply1dg1rt.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
ply1dg1rt.o ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
ply1dg1rt.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
ply1dg1rt.0 ⊢ 0 = ( 0g ‘ 𝑅 )
ply1mulrtss.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
ply1mulrtss.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑈 )
ply1mulrtss.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑈 )
ply1mulrtss.1 ⊢ · = ( .r ‘ 𝑃 )
Assertion ply1mulrtss ( 𝜑 → ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ⊆ ( ◡ ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) “ { 0 } ) )

Proof

Step Hyp Ref Expression
1 ply1dg1rt.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ply1dg1rt.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
3 ply1dg1rt.o ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
4 ply1dg1rt.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
5 ply1dg1rt.0 ⊢ 0 = ( 0g ‘ 𝑅 )
6 ply1mulrtss.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
7 ply1mulrtss.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑈 )
8 ply1mulrtss.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑈 )
9 ply1mulrtss.1 ⊢ · = ( .r ‘ 𝑃 )
10 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 3 1 2 6 10 7 evl1fvf ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐹 ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
12 11 ffnd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐹 ) Fn ( Base ‘ 𝑅 ) )
13 fniniseg2 ⊢ ( ( 𝑂 ‘ 𝐹 ) Fn ( Base ‘ 𝑅 ) → ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) = { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑥 ) = 0 } )
14 12 13 syl ⊢ ( 𝜑 → ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) = { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑥 ) = 0 } )
15 14 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ↔ 𝑥 ∈ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑥 ) = 0 } ) )
16 15 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ) → 𝑥 ∈ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑥 ) = 0 } )
17 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑥 ) = 0 } ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑥 ) = 0 ) )
18 16 17 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑥 ) = 0 ) )
19 18 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
20 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ) → 𝑅 ∈ CRing )
21 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ) → 𝐹 ∈ 𝑈 )
22 18 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑥 ) = 0 )
23 21 22 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ) → ( 𝐹 ∈ 𝑈 ∧ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑥 ) = 0 ) )
24 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ) → 𝐺 ∈ 𝑈 )
25 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ) → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) )
26 24 25 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ) → ( 𝐺 ∈ 𝑈 ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) ) )
27 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
28 3 1 10 2 20 19 23 26 9 27 evl1muld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ) → ( ( 𝐹 · 𝐺 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) ‘ 𝑥 ) = ( 0 ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) ) ) )
29 28 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ) → ( ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) ‘ 𝑥 ) = ( 0 ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) ) )
30 20 crngringd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ) → 𝑅 ∈ Ring )
31 3 1 10 2 20 19 24 fveval1fvcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ) → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
32 10 27 5 30 31 ringlzd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ) → ( 0 ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) ) = 0 )
33 29 32 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ) → ( ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) ‘ 𝑥 ) = 0 )
34 19 33 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) ‘ 𝑥 ) = 0 ) )
35 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) ‘ 𝑥 ) = 0 } ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) ‘ 𝑥 ) = 0 ) )
36 1 ply1crng ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
37 6 36 syl ⊢ ( 𝜑 → 𝑃 ∈ CRing )
38 37 crngringd ⊢ ( 𝜑 → 𝑃 ∈ Ring )
39 2 9 38 7 8 ringcld ⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) ∈ 𝑈 )
40 3 1 2 6 10 39 evl1fvf ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
41 40 ffnd ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) Fn ( Base ‘ 𝑅 ) )
42 fniniseg2 ⊢ ( ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) Fn ( Base ‘ 𝑅 ) → ( ◡ ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) “ { 0 } ) = { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) ‘ 𝑥 ) = 0 } )
43 41 42 syl ⊢ ( 𝜑 → ( ◡ ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) “ { 0 } ) = { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) ‘ 𝑥 ) = 0 } )
44 43 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) “ { 0 } ) ↔ 𝑥 ∈ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) ‘ 𝑥 ) = 0 } ) )
45 44 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) ‘ 𝑥 ) = 0 } ) → 𝑥 ∈ ( ◡ ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) “ { 0 } ) )
46 35 45 sylan2br ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) ‘ 𝑥 ) = 0 ) ) → 𝑥 ∈ ( ◡ ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) “ { 0 } ) )
47 34 46 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ) → 𝑥 ∈ ( ◡ ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) “ { 0 } ) )
48 47 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) → 𝑥 ∈ ( ◡ ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) “ { 0 } ) ) )
49 48 ssrdv ⊢ ( 𝜑 → ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 0 } ) ⊆ ( ◡ ( 𝑂 ‘ ( 𝐹 · 𝐺 ) ) “ { 0 } ) )