Theorem ply1mpl0

Description: The univariate polynomial ring has the same zero as the corresponding multivariate polynomial ring. (Contributed by Stefan O'Rear, 23-Mar-2015) (Revised by Mario Carneiro, 3-Oct-2015)

	Ref	Expression
Hypotheses	ply1mpl0.m	|- M = ( 1o mPoly R )
	ply1mpl0.p	|- P = ( Poly1 ` R )
	ply1mpl0.z	|- .0. = ( 0g ` P )
Assertion	ply1mpl0	|- .0. = ( 0g ` M )

Proof

Step	Hyp	Ref	Expression
1		ply1mpl0.m	|- M = ( 1o mPoly R )
2		ply1mpl0.p	|- P = ( Poly1 ` R )
3		ply1mpl0.z	|- .0. = ( 0g ` P )
4		eqidd	|- ( T. -> ( Base ` P ) = ( Base ` P ) )
5		eqid	|- ( PwSer1 ` R ) = ( PwSer1 ` R )
6		eqid	|- ( Base ` P ) = ( Base ` P )
7	2 5 6	ply1bas	|- ( Base ` P ) = ( Base ` ( 1o mPoly R ) )
8	1	fveq2i	|- ( Base ` M ) = ( Base ` ( 1o mPoly R ) )
9	7 8	eqtr4i	|- ( Base ` P ) = ( Base ` M )
10	9	a1i	|- ( T. -> ( Base ` P ) = ( Base ` M ) )
11		eqid	|- ( +g ` P ) = ( +g ` P )
12	2 1 11	ply1plusg	|- ( +g ` P ) = ( +g ` M )
13	12	a1i	|- ( T. -> ( +g ` P ) = ( +g ` M ) )
14	13	oveqdr	|- ( ( T. /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( x ( +g ` P ) y ) = ( x ( +g ` M ) y ) )
15	4 10 14	grpidpropd	|- ( T. -> ( 0g ` P ) = ( 0g ` M ) )
16	15	mptru	|- ( 0g ` P ) = ( 0g ` M )
17	3 16	eqtri	|- .0. = ( 0g ` M )