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