q1pcl

Description: Closure of the quotient by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	q1pcl.q	$⊢ Q = {quot}_{1p} (R)$
	q1pcl.p	$⊢ P = {Poly}_{1} (R)$
	q1pcl.b	$⊢ B = {Base}_{P}$
	q1pcl.c	$⊢ C = {Unic}_{1p} (R)$
Assertion	q1pcl	$⊢ (R \in Ring \land F \in B \land G \in C) \to F Q G \in B$

Step	Hyp	Ref	Expression
1		q1pcl.q	$⊢ Q = {quot}_{1p} (R)$
2		q1pcl.p	$⊢ P = {Poly}_{1} (R)$
3		q1pcl.b	$⊢ B = {Base}_{P}$
4		q1pcl.c	$⊢ C = {Unic}_{1p} (R)$
5		eqid	$⊢ F Q G = F Q G$
6		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
7		eqid	$⊢ -_{P} = -_{P}$
8		eqid	$⊢ \cdot_{P} = \cdot_{P}$
9	1 2 3 6 7 8 4	q1peqb	$⊢ (R \in Ring \land F \in B \land G \in C) \to ((F Q G \in B \land \deg_{1} (R) (F -_{P} ((F Q G) \cdot_{P} G)) < \deg_{1} (R) (G)) \leftrightarrow F Q G = F Q G)$
10	5 9	mpbiri	$⊢ (R \in Ring \land F \in B \land G \in C) \to (F Q G \in B \land \deg_{1} (R) (F -_{P} ((F Q G) \cdot_{P} G)) < \deg_{1} (R) (G))$
11	10	simpld	$⊢ (R \in Ring \land F \in B \land G \in C) \to F Q G \in B$

Metamath Proof Explorer