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

Metamath Proof Explorer

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 ‘ 𝑆 ) )