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 = {Poly}_{1} (R)$
	ply1dg1rt.u	$⊢ U = {Base}_{P}$
	ply1dg1rt.o	$⊢ O = {eval}_{1} (R)$
	ply1dg1rt.d	$⊢ D = \deg_{1} (R)$
	ply1dg1rt.0	$⊢ \underset{˙}{0} = 0_{R}$
	ply1mulrtss.r	$⊢ φ \to R \in CRing$
	ply1mulrtss.f	$⊢ φ \to F \in U$
	ply1mulrtss.g	$⊢ φ \to G \in U$
	ply1mulrtss.1	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
Assertion	ply1mulrtss	$⊢ φ \to {O (F)}^{-1} [\{\underset{˙}{0}\}] \subseteq {O (F \underset{˙}{\cdot} G)}^{-1} [\{\underset{˙}{0}\}]$

Proof

Step	Hyp	Ref	Expression
1		ply1dg1rt.p	$⊢ P = {Poly}_{1} (R)$
2		ply1dg1rt.u	$⊢ U = {Base}_{P}$
3		ply1dg1rt.o	$⊢ O = {eval}_{1} (R)$
4		ply1dg1rt.d	$⊢ D = \deg_{1} (R)$
5		ply1dg1rt.0	$⊢ \underset{˙}{0} = 0_{R}$
6		ply1mulrtss.r	$⊢ φ \to R \in CRing$
7		ply1mulrtss.f	$⊢ φ \to F \in U$
8		ply1mulrtss.g	$⊢ φ \to G \in U$
9		ply1mulrtss.1	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
10		eqid	$⊢ {Base}_{R} = {Base}_{R}$
11	3 1 2 6 10 7	evl1fvf	$⊢ φ \to O (F) : {Base}_{R} ⟶ {Base}_{R}$
12	11	ffnd	$⊢ φ \to O (F) Fn {Base}_{R}$
13		fniniseg2	$⊢ O (F) Fn {Base}_{R} \to {O (F)}^{-1} [\{\underset{˙}{0}\}] = \{x \in {Base}_{R} \| O (F) (x) = \underset{˙}{0}\}$
14	12 13	syl	$⊢ φ \to {O (F)}^{-1} [\{\underset{˙}{0}\}] = \{x \in {Base}_{R} \| O (F) (x) = \underset{˙}{0}\}$
15	14	eleq2d	$⊢ φ \to (x \in {O (F)}^{-1} [\{\underset{˙}{0}\}] \leftrightarrow x \in \{x \in {Base}_{R} \| O (F) (x) = \underset{˙}{0}\})$
16	15	biimpa	$⊢ (φ \land x \in {O (F)}^{-1} [\{\underset{˙}{0}\}]) \to x \in \{x \in {Base}_{R} \| O (F) (x) = \underset{˙}{0}\}$
17		rabid	$⊢ x \in \{x \in {Base}_{R} \| O (F) (x) = \underset{˙}{0}\} \leftrightarrow (x \in {Base}_{R} \land O (F) (x) = \underset{˙}{0})$
18	16 17	sylib	$⊢ (φ \land x \in {O (F)}^{-1} [\{\underset{˙}{0}\}]) \to (x \in {Base}_{R} \land O (F) (x) = \underset{˙}{0})$
19	18	simpld	$⊢ (φ \land x \in {O (F)}^{-1} [\{\underset{˙}{0}\}]) \to x \in {Base}_{R}$
20	6	adantr	$⊢ (φ \land x \in {O (F)}^{-1} [\{\underset{˙}{0}\}]) \to R \in CRing$
21	7	adantr	$⊢ (φ \land x \in {O (F)}^{-1} [\{\underset{˙}{0}\}]) \to F \in U$
22	18	simprd	$⊢ (φ \land x \in {O (F)}^{-1} [\{\underset{˙}{0}\}]) \to O (F) (x) = \underset{˙}{0}$
23	21 22	jca	$⊢ (φ \land x \in {O (F)}^{-1} [\{\underset{˙}{0}\}]) \to (F \in U \land O (F) (x) = \underset{˙}{0})$
24	8	adantr	$⊢ (φ \land x \in {O (F)}^{-1} [\{\underset{˙}{0}\}]) \to G \in U$
25		eqidd	$⊢ (φ \land x \in {O (F)}^{-1} [\{\underset{˙}{0}\}]) \to O (G) (x) = O (G) (x)$
26	24 25	jca	$⊢ (φ \land x \in {O (F)}^{-1} [\{\underset{˙}{0}\}]) \to (G \in U \land O (G) (x) = O (G) (x))$
27		eqid	$⊢ \cdot_{R} = \cdot_{R}$
28	3 1 10 2 20 19 23 26 9 27	evl1muld	$⊢ (φ \land x \in {O (F)}^{-1} [\{\underset{˙}{0}\}]) \to (F \underset{˙}{\cdot} G \in U \land O (F \underset{˙}{\cdot} G) (x) = \underset{˙}{0} \cdot_{R} O (G) (x))$
29	28	simprd	$⊢ (φ \land x \in {O (F)}^{-1} [\{\underset{˙}{0}\}]) \to O (F \underset{˙}{\cdot} G) (x) = \underset{˙}{0} \cdot_{R} O (G) (x)$
30	20	crngringd	$⊢ (φ \land x \in {O (F)}^{-1} [\{\underset{˙}{0}\}]) \to R \in Ring$
31	3 1 10 2 20 19 24	fveval1fvcl	$⊢ (φ \land x \in {O (F)}^{-1} [\{\underset{˙}{0}\}]) \to O (G) (x) \in {Base}_{R}$
32	10 27 5 30 31	ringlzd	$⊢ (φ \land x \in {O (F)}^{-1} [\{\underset{˙}{0}\}]) \to \underset{˙}{0} \cdot_{R} O (G) (x) = \underset{˙}{0}$
33	29 32	eqtrd	$⊢ (φ \land x \in {O (F)}^{-1} [\{\underset{˙}{0}\}]) \to O (F \underset{˙}{\cdot} G) (x) = \underset{˙}{0}$
34	19 33	jca	$⊢ (φ \land x \in {O (F)}^{-1} [\{\underset{˙}{0}\}]) \to (x \in {Base}_{R} \land O (F \underset{˙}{\cdot} G) (x) = \underset{˙}{0})$
35		rabid	$⊢ x \in \{x \in {Base}_{R} \| O (F \underset{˙}{\cdot} G) (x) = \underset{˙}{0}\} \leftrightarrow (x \in {Base}_{R} \land O (F \underset{˙}{\cdot} G) (x) = \underset{˙}{0})$
36	1	ply1crng	$⊢ R \in CRing \to P \in CRing$
37	6 36	syl	$⊢ φ \to P \in CRing$
38	37	crngringd	$⊢ φ \to P \in Ring$
39	2 9 38 7 8	ringcld	$⊢ φ \to F \underset{˙}{\cdot} G \in U$
40	3 1 2 6 10 39	evl1fvf	$⊢ φ \to O (F \underset{˙}{\cdot} G) : {Base}_{R} ⟶ {Base}_{R}$
41	40	ffnd	$⊢ φ \to O (F \underset{˙}{\cdot} G) Fn {Base}_{R}$
42		fniniseg2	$⊢ O (F \underset{˙}{\cdot} G) Fn {Base}_{R} \to {O (F \underset{˙}{\cdot} G)}^{-1} [\{\underset{˙}{0}\}] = \{x \in {Base}_{R} \| O (F \underset{˙}{\cdot} G) (x) = \underset{˙}{0}\}$
43	41 42	syl	$⊢ φ \to {O (F \underset{˙}{\cdot} G)}^{-1} [\{\underset{˙}{0}\}] = \{x \in {Base}_{R} \| O (F \underset{˙}{\cdot} G) (x) = \underset{˙}{0}\}$
44	43	eleq2d	$⊢ φ \to (x \in {O (F \underset{˙}{\cdot} G)}^{-1} [\{\underset{˙}{0}\}] \leftrightarrow x \in \{x \in {Base}_{R} \| O (F \underset{˙}{\cdot} G) (x) = \underset{˙}{0}\})$
45	44	biimpar	$⊢ (φ \land x \in \{x \in {Base}_{R} \| O (F \underset{˙}{\cdot} G) (x) = \underset{˙}{0}\}) \to x \in {O (F \underset{˙}{\cdot} G)}^{-1} [\{\underset{˙}{0}\}]$
46	35 45	sylan2br	$⊢ (φ \land (x \in {Base}_{R} \land O (F \underset{˙}{\cdot} G) (x) = \underset{˙}{0})) \to x \in {O (F \underset{˙}{\cdot} G)}^{-1} [\{\underset{˙}{0}\}]$
47	34 46	syldan	$⊢ (φ \land x \in {O (F)}^{-1} [\{\underset{˙}{0}\}]) \to x \in {O (F \underset{˙}{\cdot} G)}^{-1} [\{\underset{˙}{0}\}]$
48	47	ex	$⊢ φ \to (x \in {O (F)}^{-1} [\{\underset{˙}{0}\}] \to x \in {O (F \underset{˙}{\cdot} G)}^{-1} [\{\underset{˙}{0}\}])$
49	48	ssrdv	$⊢ φ \to {O (F)}^{-1} [\{\underset{˙}{0}\}] \subseteq {O (F \underset{˙}{\cdot} G)}^{-1} [\{\underset{˙}{0}\}]$

Metamath Proof Explorer

Theorem ply1mulrtss

Proof