Theorem plydivlem1

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 )
Assertion	plydivlem1	|- ( ph -> 0 e. 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		1pneg1e0	|- ( 1 + -u 1 ) = 0
6		neg1mulneg1e1	|- ( -u 1 x. -u 1 ) = 1
7	2 4 4	caovcld	|- ( ph -> ( -u 1 x. -u 1 ) e. S )
8	6 7	eqeltrrid	|- ( ph -> 1 e. S )
9	1 8 4	caovcld	|- ( ph -> ( 1 + -u 1 ) e. S )
10	5 9	eqeltrrid	|- ( ph -> 0 e. S )