plydivlem3

Description: Lemma for plydivex . Base case of induction. (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Hypotheses	plydiv.pl	$⊢ (φ \land (x \in S \land y \in S)) \to x + y \in S$
	plydiv.tm	$⊢ (φ \land (x \in S \land y \in S)) \to x y \in S$
	plydiv.rc	$⊢ (φ \land (x \in S \land x \neq 0)) \to \frac{1}{x} \in S$
	plydiv.m1	$⊢ φ \to - 1 \in S$
	plydiv.f	$⊢ φ \to F \in Poly (S)$
	plydiv.g	$⊢ φ \to G \in Poly (S)$
	plydiv.z	$⊢ φ \to G \neq 0_{𝑝}$
	plydiv.r	$⊢ R = F -_{f} (G \times_{f} q)$
	plydiv.0	$⊢ φ \to (F = 0_{𝑝} \lor \deg (F) - \deg (G) < 0)$
Assertion	plydivlem3	$⊢ φ \to \exists q \in Poly (S) (R = 0_{𝑝} \lor \deg (R) < \deg (G))$

Proof

Step	Hyp	Ref	Expression
1		plydiv.pl	$⊢ (φ \land (x \in S \land y \in S)) \to x + y \in S$
2		plydiv.tm	$⊢ (φ \land (x \in S \land y \in S)) \to x y \in S$
3		plydiv.rc	$⊢ (φ \land (x \in S \land x \neq 0)) \to \frac{1}{x} \in S$
4		plydiv.m1	$⊢ φ \to - 1 \in S$
5		plydiv.f	$⊢ φ \to F \in Poly (S)$
6		plydiv.g	$⊢ φ \to G \in Poly (S)$
7		plydiv.z	$⊢ φ \to G \neq 0_{𝑝}$
8		plydiv.r	$⊢ R = F -_{f} (G \times_{f} q)$
9		plydiv.0	$⊢ φ \to (F = 0_{𝑝} \lor \deg (F) - \deg (G) < 0)$
10		plybss	$⊢ F \in Poly (S) \to S \subseteq ℂ$
11		ply0	$⊢ S \subseteq ℂ \to 0_{𝑝} \in Poly (S)$
12	5 10 11	3syl	$⊢ φ \to 0_{𝑝} \in Poly (S)$
13		cnex	$⊢ ℂ \in V$
14	13	a1i	$⊢ φ \to ℂ \in V$
15		plyf	$⊢ F \in Poly (S) \to F : ℂ ⟶ ℂ$
16		ffn	$⊢ F : ℂ ⟶ ℂ \to F Fn ℂ$
17	5 15 16	3syl	$⊢ φ \to F Fn ℂ$
18		plyf	$⊢ G \in Poly (S) \to G : ℂ ⟶ ℂ$
19		ffn	$⊢ G : ℂ ⟶ ℂ \to G Fn ℂ$
20	6 18 19	3syl	$⊢ φ \to G Fn ℂ$
21		plyf	$⊢ 0_{𝑝} \in Poly (S) \to 0_{𝑝} : ℂ ⟶ ℂ$
22		ffn	$⊢ 0_{𝑝} : ℂ ⟶ ℂ \to 0_{𝑝} Fn ℂ$
23	12 21 22	3syl	$⊢ φ \to 0_{𝑝} Fn ℂ$
24		inidm	$⊢ ℂ \cap ℂ = ℂ$
25	20 23 14 14 24	offn	$⊢ φ \to (G \times_{f} 0_{𝑝}) Fn ℂ$
26		eqidd	$⊢ (φ \land z \in ℂ) \to F (z) = F (z)$
27		eqidd	$⊢ (φ \land z \in ℂ) \to G (z) = G (z)$
28		0pval	$⊢ z \in ℂ \to 0_{𝑝} (z) = 0$
29	28	adantl	$⊢ (φ \land z \in ℂ) \to 0_{𝑝} (z) = 0$
30	20 23 14 14 24 27 29	ofval	$⊢ (φ \land z \in ℂ) \to (G \times_{f} 0_{𝑝}) (z) = G (z) \cdot 0$
31	6 18	syl	$⊢ φ \to G : ℂ ⟶ ℂ$
32	31	ffvelcdmda	$⊢ (φ \land z \in ℂ) \to G (z) \in ℂ$
33	32	mul01d	$⊢ (φ \land z \in ℂ) \to G (z) \cdot 0 = 0$
34	30 33	eqtrd	$⊢ (φ \land z \in ℂ) \to (G \times_{f} 0_{𝑝}) (z) = 0$
35	5 15	syl	$⊢ φ \to F : ℂ ⟶ ℂ$
36	35	ffvelcdmda	$⊢ (φ \land z \in ℂ) \to F (z) \in ℂ$
37	36	subid1d	$⊢ (φ \land z \in ℂ) \to F (z) - 0 = F (z)$
38	14 17 25 17 26 34 37	offveq	$⊢ φ \to F -_{f} (G \times_{f} 0_{𝑝}) = F$
39	38	eqeq1d	$⊢ φ \to (F -_{f} (G \times_{f} 0_{𝑝}) = 0_{𝑝} \leftrightarrow F = 0_{𝑝})$
40	38	fveq2d	$⊢ φ \to \deg (F -_{f} (G \times_{f} 0_{𝑝})) = \deg (F)$
41		dgrcl	$⊢ G \in Poly (S) \to \deg (G) \in ℕ_{0}$
42	6 41	syl	$⊢ φ \to \deg (G) \in ℕ_{0}$
43	42	nn0red	$⊢ φ \to \deg (G) \in ℝ$
44	43	recnd	$⊢ φ \to \deg (G) \in ℂ$
45	44	addlidd	$⊢ φ \to 0 + \deg (G) = \deg (G)$
46	45	eqcomd	$⊢ φ \to \deg (G) = 0 + \deg (G)$
47	40 46	breq12d	$⊢ φ \to (\deg (F -_{f} (G \times_{f} 0_{𝑝})) < \deg (G) \leftrightarrow \deg (F) < 0 + \deg (G))$
48		dgrcl	$⊢ F \in Poly (S) \to \deg (F) \in ℕ_{0}$
49	5 48	syl	$⊢ φ \to \deg (F) \in ℕ_{0}$
50	49	nn0red	$⊢ φ \to \deg (F) \in ℝ$
51		0red	$⊢ φ \to 0 \in ℝ$
52	50 43 51	ltsubaddd	$⊢ φ \to (\deg (F) - \deg (G) < 0 \leftrightarrow \deg (F) < 0 + \deg (G))$
53	47 52	bitr4d	$⊢ φ \to (\deg (F -_{f} (G \times_{f} 0_{𝑝})) < \deg (G) \leftrightarrow \deg (F) - \deg (G) < 0)$
54	39 53	orbi12d	$⊢ φ \to ((F -_{f} (G \times_{f} 0_{𝑝}) = 0_{𝑝} \lor \deg (F -_{f} (G \times_{f} 0_{𝑝})) < \deg (G)) \leftrightarrow (F = 0_{𝑝} \lor \deg (F) - \deg (G) < 0))$
55	9 54	mpbird	$⊢ φ \to (F -_{f} (G \times_{f} 0_{𝑝}) = 0_{𝑝} \lor \deg (F -_{f} (G \times_{f} 0_{𝑝})) < \deg (G))$
56		oveq2	$⊢ q = 0_{𝑝} \to G \times_{f} q = G \times_{f} 0_{𝑝}$
57	56	oveq2d	$⊢ q = 0_{𝑝} \to F -_{f} (G \times_{f} q) = F -_{f} (G \times_{f} 0_{𝑝})$
58	8 57	eqtrid	$⊢ q = 0_{𝑝} \to R = F -_{f} (G \times_{f} 0_{𝑝})$
59	58	eqeq1d	$⊢ q = 0_{𝑝} \to (R = 0_{𝑝} \leftrightarrow F -_{f} (G \times_{f} 0_{𝑝}) = 0_{𝑝})$
60	58	fveq2d	$⊢ q = 0_{𝑝} \to \deg (R) = \deg (F -_{f} (G \times_{f} 0_{𝑝}))$
61	60	breq1d	$⊢ q = 0_{𝑝} \to (\deg (R) < \deg (G) \leftrightarrow \deg (F -_{f} (G \times_{f} 0_{𝑝})) < \deg (G))$
62	59 61	orbi12d	$⊢ q = 0_{𝑝} \to ((R = 0_{𝑝} \lor \deg (R) < \deg (G)) \leftrightarrow (F -_{f} (G \times_{f} 0_{𝑝}) = 0_{𝑝} \lor \deg (F -_{f} (G \times_{f} 0_{𝑝})) < \deg (G)))$
63	62	rspcev	$⊢ (0_{𝑝} \in Poly (S) \land (F -_{f} (G \times_{f} 0_{𝑝}) = 0_{𝑝} \lor \deg (F -_{f} (G \times_{f} 0_{𝑝})) < \deg (G))) \to \exists q \in Poly (S) (R = 0_{𝑝} \lor \deg (R) < \deg (G))$
64	12 55 63	syl2anc	$⊢ φ \to \exists q \in Poly (S) (R = 0_{𝑝} \lor \deg (R) < \deg (G))$

Metamath Proof Explorer

Theorem plydivlem3

Proof