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	|- ( Base ` P ) = ( Base ` P )
6	2 5	ply1bas	|- ( Base ` P ) = ( Base ` ( 1o mPoly R ) )
7	1	fveq2i	|- ( Base ` M ) = ( Base ` ( 1o mPoly R ) )
8	6 7	eqtr4i	|- ( Base ` P ) = ( Base ` M )
9	8	a1i	|- ( T. -> ( Base ` P ) = ( Base ` M ) )
10		eqid	|- ( +g ` P ) = ( +g ` P )
11	2 1 10	ply1plusg	|- ( +g ` P ) = ( +g ` M )
12	11	a1i	|- ( T. -> ( +g ` P ) = ( +g ` M ) )
13	12	oveqdr	|- ( ( T. /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( x ( +g ` P ) y ) = ( x ( +g ` M ) y ) )
14	4 9 13	grpidpropd	|- ( T. -> ( 0g ` P ) = ( 0g ` M ) )
15	14	mptru	|- ( 0g ` P ) = ( 0g ` M )
16	3 15	eqtri	|- .0. = ( 0g ` M )