This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ply1divalg

Description: The division algorithm for univariate polynomials over a ring. For polynomials F , G such that G =/= 0 and the leading coefficient of G is a unit, there are unique polynomials q and r = F - ( G x. q ) such that the degree of r is less than the degree of G . (Contributed by Stefan O'Rear, 27-Mar-2015)

Ref Expression
Hypotheses ply1divalg.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ply1divalg.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
ply1divalg.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
ply1divalg.m ⊢ − = ( -g ‘ 𝑃 )
ply1divalg.z ⊢ 0 = ( 0g ‘ 𝑃 )
ply1divalg.t ⊢ ∙ = ( .r ‘ 𝑃 )
ply1divalg.r1 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
ply1divalg.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
ply1divalg.g1 ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
ply1divalg.g2 ⊢ ( 𝜑 → 𝐺 ≠ 0 )
ply1divalg.g3 ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ 𝑈 )
ply1divalg.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
Assertion ply1divalg ( 𝜑 → ∃! 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 ply1divalg.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ply1divalg.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
3 ply1divalg.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
4 ply1divalg.m ⊢ − = ( -g ‘ 𝑃 )
5 ply1divalg.z ⊢ 0 = ( 0g ‘ 𝑃 )
6 ply1divalg.t ⊢ ∙ = ( .r ‘ 𝑃 )
7 ply1divalg.r1 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
8 ply1divalg.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
9 ply1divalg.g1 ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
10 ply1divalg.g2 ⊢ ( 𝜑 → 𝐺 ≠ 0 )
11 ply1divalg.g3 ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ 𝑈 )
12 ply1divalg.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
13 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
14 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
15 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
16 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
17 12 16 14 ringinvcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ) ∈ ( Base ‘ 𝑅 ) )
18 7 11 17 syl2anc ⊢ ( 𝜑 → ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ) ∈ ( Base ‘ 𝑅 ) )
19 12 16 15 13 unitrinv ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ 𝑈 ) → ( ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ) ) = ( 1r ‘ 𝑅 ) )
20 7 11 19 syl2anc ⊢ ( 𝜑 → ( ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ) ) = ( 1r ‘ 𝑅 ) )
21 1 2 3 4 5 6 7 8 9 10 13 14 15 18 20 ply1divex ⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) )
22 eqid ⊢ ( RLReg ‘ 𝑅 ) = ( RLReg ‘ 𝑅 )
23 22 12 unitrrg ⊢ ( 𝑅 ∈ Ring → 𝑈 ⊆ ( RLReg ‘ 𝑅 ) )
24 7 23 syl ⊢ ( 𝜑 → 𝑈 ⊆ ( RLReg ‘ 𝑅 ) )
25 24 11 sseldd ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ ( RLReg ‘ 𝑅 ) )
26 1 2 3 4 5 6 7 8 9 10 25 22 ply1divmo ⊢ ( 𝜑 → ∃* 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) )
27 reu5 ⊢ ( ∃! 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ( ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ∧ ∃* 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
28 21 26 27 sylanbrc ⊢ ( 𝜑 → ∃! 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) )