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	⊢ ( 𝜑 → ∃! 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) )