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 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
plydiv.tm 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
plydiv.rc 
|- ( ( ph /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S )
plydiv.m1 
|- ( ph -> -u 1 e. S )
plydiv.f 
|- ( ph -> F e. ( Poly ` S ) )
plydiv.g 
|- ( ph -> G e. ( Poly ` S ) )
plydiv.z 
|- ( ph -> G =/= 0p )
plydiv.r 
|- R = ( F oF - ( G oF x. q ) )
Assertion plydivlem2 
|- ( ( ph /\ q e. ( Poly ` S ) ) -> R e. ( Poly ` S ) )

Proof

Step Hyp Ref Expression
1 plydiv.pl 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
2 plydiv.tm 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
3 plydiv.rc 
 |-  ( ( ph /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S )
4 plydiv.m1 
 |-  ( ph -> -u 1 e. S )
5 plydiv.f 
 |-  ( ph -> F e. ( Poly ` S ) )
6 plydiv.g 
 |-  ( ph -> G e. ( Poly ` S ) )
7 plydiv.z 
 |-  ( ph -> G =/= 0p )
8 plydiv.r 
 |-  R = ( F oF - ( G oF x. q ) )
9 5 adantr 
 |-  ( ( ph /\ q e. ( Poly ` S ) ) -> F e. ( Poly ` S ) )
10 6 adantr 
 |-  ( ( ph /\ q e. ( Poly ` S ) ) -> G e. ( Poly ` S ) )
11 simpr 
 |-  ( ( ph /\ q e. ( Poly ` S ) ) -> q e. ( Poly ` S ) )
12 1 adantlr 
 |-  ( ( ( ph /\ q e. ( Poly ` S ) ) /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
13 2 adantlr 
 |-  ( ( ( ph /\ q e. ( Poly ` S ) ) /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
14 10 11 12 13 plymul 
 |-  ( ( ph /\ q e. ( Poly ` S ) ) -> ( G oF x. q ) e. ( Poly ` S ) )
15 4 adantr 
 |-  ( ( ph /\ q e. ( Poly ` S ) ) -> -u 1 e. S )
16 9 14 12 13 15 plysub 
 |-  ( ( ph /\ q e. ( Poly ` S ) ) -> ( F oF - ( G oF x. q ) ) e. ( Poly ` S ) )
17 8 16 eqeltrid 
 |-  ( ( ph /\ q e. ( Poly ` S ) ) -> R e. ( Poly ` S ) )