Theorem plydivlem2

Description: Lemma for plydivalg . (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Hypotheses	plydiv.pl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
	plydiv.tm	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
	plydiv.rc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0 ) ) → ( 1 / 𝑥 ) ∈ 𝑆 )
	plydiv.m1	⊢ ( 𝜑 → - 1 ∈ 𝑆 )
	plydiv.f	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
	plydiv.g	⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
	plydiv.z	⊢ ( 𝜑 → 𝐺 ≠ 0𝑝 )
	plydiv.r	⊢ 𝑅 = ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑞 ) )
Assertion	plydivlem2	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( Poly ‘ 𝑆 ) ) → 𝑅 ∈ ( Poly ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		plydiv.pl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
2		plydiv.tm	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
3		plydiv.rc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0 ) ) → ( 1 / 𝑥 ) ∈ 𝑆 )
4		plydiv.m1	⊢ ( 𝜑 → - 1 ∈ 𝑆 )
5		plydiv.f	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
6		plydiv.g	⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
7		plydiv.z	⊢ ( 𝜑 → 𝐺 ≠ 0𝑝 )
8		plydiv.r	⊢ 𝑅 = ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑞 ) )
9	5	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
10	6	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( Poly ‘ 𝑆 ) ) → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( Poly ‘ 𝑆 ) ) → 𝑞 ∈ ( Poly ‘ 𝑆 ) )
12	1	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
13	2	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
14	10 11 12 13	plymul	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐺 ∘f · 𝑞 ) ∈ ( Poly ‘ 𝑆 ) )
15	4	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( Poly ‘ 𝑆 ) ) → - 1 ∈ 𝑆 )
16	9 14 12 13 15	plysub	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ∈ ( Poly ‘ 𝑆 ) )
17	8 16	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( Poly ‘ 𝑆 ) ) → 𝑅 ∈ ( Poly ‘ 𝑆 ) )