Metamath Proof Explorer

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 ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → 𝐹 = ( ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) + ( 𝐹 𝐸 𝐺 ) ) )