Theorem r1pid

Description: Express the original polynomial F as F = ( q x. G ) + r using the quotient and remainder functions for q and r . (Contributed by Mario Carneiro, 5-Jun-2015)

	Ref	Expression
Hypotheses	r1pid.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	r1pid.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	r1pid.c	⊢ 𝐶 = ( Unic1p ‘ 𝑅 )
	r1pid.q	⊢ 𝑄 = ( quot1p ‘ 𝑅 )
	r1pid.e	⊢ 𝐸 = ( rem1p ‘ 𝑅 )
	r1pid.t	⊢ · = ( .r ‘ 𝑃 )
	r1pid.m	⊢ + = ( +g ‘ 𝑃 )
Assertion	r1pid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → 𝐹 = ( ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) + ( 𝐹 𝐸 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		r1pid.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		r1pid.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		r1pid.c	⊢ 𝐶 = ( Unic1p ‘ 𝑅 )
4		r1pid.q	⊢ 𝑄 = ( quot1p ‘ 𝑅 )
5		r1pid.e	⊢ 𝐸 = ( rem1p ‘ 𝑅 )
6		r1pid.t	⊢ · = ( .r ‘ 𝑃 )
7		r1pid.m	⊢ + = ( +g ‘ 𝑃 )
8	1 2 3	uc1pcl	⊢ ( 𝐺 ∈ 𝐶 → 𝐺 ∈ 𝐵 )
9		eqid	⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
10	5 1 2 4 6 9	r1pval	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 𝐸 𝐺 ) = ( 𝐹 ( -g ‘ 𝑃 ) ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) )
11	8 10	sylan2	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( 𝐹 𝐸 𝐺 ) = ( 𝐹 ( -g ‘ 𝑃 ) ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) )
12	11	3adant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( 𝐹 𝐸 𝐺 ) = ( 𝐹 ( -g ‘ 𝑃 ) ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) )
13	12	oveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) + ( 𝐹 𝐸 𝐺 ) ) = ( ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) + ( 𝐹 ( -g ‘ 𝑃 ) ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) ) )
14	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
15	14	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → 𝑃 ∈ Ring )
16		ringabl	⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ Abel )
17	15 16	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → 𝑃 ∈ Abel )
18	4 1 2 3	q1pcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( 𝐹 𝑄 𝐺 ) ∈ 𝐵 )
19	8	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → 𝐺 ∈ 𝐵 )
20	2 6	ringcl	⊢ ( ( 𝑃 ∈ Ring ∧ ( 𝐹 𝑄 𝐺 ) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ∈ 𝐵 )
21	15 18 19 20	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ∈ 𝐵 )
22		ringgrp	⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ Grp )
23	15 22	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → 𝑃 ∈ Grp )
24		simp2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → 𝐹 ∈ 𝐵 )
25	2 9	grpsubcl	⊢ ( ( 𝑃 ∈ Grp ∧ 𝐹 ∈ 𝐵 ∧ ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ∈ 𝐵 ) → ( 𝐹 ( -g ‘ 𝑃 ) ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) ∈ 𝐵 )
26	23 24 21 25	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( 𝐹 ( -g ‘ 𝑃 ) ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) ∈ 𝐵 )
27	2 7	ablcom	⊢ ( ( 𝑃 ∈ Abel ∧ ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ∈ 𝐵 ∧ ( 𝐹 ( -g ‘ 𝑃 ) ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) ∈ 𝐵 ) → ( ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) + ( 𝐹 ( -g ‘ 𝑃 ) ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) ) = ( ( 𝐹 ( -g ‘ 𝑃 ) ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) + ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) )
28	17 21 26 27	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) + ( 𝐹 ( -g ‘ 𝑃 ) ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) ) = ( ( 𝐹 ( -g ‘ 𝑃 ) ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) + ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) )
29	2 7 9	grpnpcan	⊢ ( ( 𝑃 ∈ Grp ∧ 𝐹 ∈ 𝐵 ∧ ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ∈ 𝐵 ) → ( ( 𝐹 ( -g ‘ 𝑃 ) ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) + ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) = 𝐹 )
30	23 24 21 29	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( ( 𝐹 ( -g ‘ 𝑃 ) ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) + ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) = 𝐹 )
31	13 28 30	3eqtrrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → 𝐹 = ( ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) + ( 𝐹 𝐸 𝐺 ) ) )