r1pcl

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

	Ref	Expression
Hypotheses	r1pval.e	$⊢ E = {rem}_{1p} (R)$
	r1pval.p	$⊢ P = {Poly}_{1} (R)$
	r1pval.b	$⊢ B = {Base}_{P}$
	r1pcl.c	$⊢ C = {Unic}_{1p} (R)$
Assertion	r1pcl	$⊢ (R \in Ring \land F \in B \land G \in C) \to F E G \in B$

Proof

Step	Hyp	Ref	Expression
1		r1pval.e	$⊢ E = {rem}_{1p} (R)$
2		r1pval.p	$⊢ P = {Poly}_{1} (R)$
3		r1pval.b	$⊢ B = {Base}_{P}$
4		r1pcl.c	$⊢ C = {Unic}_{1p} (R)$
5		simp2	$⊢ (R \in Ring \land F \in B \land G \in C) \to F \in B$
6	2 3 4	uc1pcl	$⊢ G \in C \to G \in B$
7	6	3ad2ant3	$⊢ (R \in Ring \land F \in B \land G \in C) \to G \in B$
8		eqid	$⊢ {quot}_{1p} (R) = {quot}_{1p} (R)$
9		eqid	$⊢ \cdot_{P} = \cdot_{P}$
10		eqid	$⊢ -_{P} = -_{P}$
11	1 2 3 8 9 10	r1pval	$⊢ (F \in B \land G \in B) \to F E G = F -_{P} ((F {quot}_{1p} (R) G) \cdot_{P} G)$
12	5 7 11	syl2anc	$⊢ (R \in Ring \land F \in B \land G \in C) \to F E G = F -_{P} ((F {quot}_{1p} (R) G) \cdot_{P} G)$
13	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
14	13	3ad2ant1	$⊢ (R \in Ring \land F \in B \land G \in C) \to P \in Ring$
15		ringgrp	$⊢ P \in Ring \to P \in Grp$
16	14 15	syl	$⊢ (R \in Ring \land F \in B \land G \in C) \to P \in Grp$
17	8 2 3 4	q1pcl	$⊢ (R \in Ring \land F \in B \land G \in C) \to F {quot}_{1p} (R) G \in B$
18	3 9	ringcl	$⊢ (P \in Ring \land F {quot}_{1p} (R) G \in B \land G \in B) \to (F {quot}_{1p} (R) G) \cdot_{P} G \in B$
19	14 17 7 18	syl3anc	$⊢ (R \in Ring \land F \in B \land G \in C) \to (F {quot}_{1p} (R) G) \cdot_{P} G \in B$
20	3 10	grpsubcl	$⊢ (P \in Grp \land F \in B \land (F {quot}_{1p} (R) G) \cdot_{P} G \in B) \to F -_{P} ((F {quot}_{1p} (R) G) \cdot_{P} G) \in B$
21	16 5 19 20	syl3anc	$⊢ (R \in Ring \land F \in B \land G \in C) \to F -_{P} ((F {quot}_{1p} (R) G) \cdot_{P} G) \in B$
22	12 21	eqeltrd	$⊢ (R \in Ring \land F \in B \land G \in C) \to F E G \in B$

Metamath Proof Explorer

Theorem r1pcl

Proof