plydivlem2

	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)$
Assertion	plydivlem2	$⊢ (φ \land q \in Poly (S)) \to R \in Poly (S)$

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	5	adantr	$⊢ (φ \land q \in Poly (S)) \to F \in Poly (S)$
10	6	adantr	$⊢ (φ \land q \in Poly (S)) \to G \in Poly (S)$
11		simpr	$⊢ (φ \land q \in Poly (S)) \to q \in Poly (S)$
12	1	adantlr	$⊢ ((φ \land q \in Poly (S)) \land (x \in S \land y \in S)) \to x + y \in S$
13	2	adantlr	$⊢ ((φ \land q \in Poly (S)) \land (x \in S \land y \in S)) \to x y \in S$
14	10 11 12 13	plymul	$⊢ (φ \land q \in Poly (S)) \to G \times_{f} q \in Poly (S)$
15	4	adantr	$⊢ (φ \land q \in Poly (S)) \to - 1 \in S$
16	9 14 12 13 15	plysub	$⊢ (φ \land q \in Poly (S)) \to F -_{f} (G \times_{f} q) \in Poly (S)$
17	8 16	eqeltrid	$⊢ (φ \land q \in Poly (S)) \to R \in Poly (S)$

Metamath Proof Explorer