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	⊢ 𝑀 = ( 1o mPoly 𝑅 )
	ply1mpl0.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1mpl0.z	⊢ 0 = ( 0g ‘ 𝑃 )
Assertion	ply1mpl0	⊢ 0 = ( 0g ‘ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		ply1mpl0.m	⊢ 𝑀 = ( 1o mPoly 𝑅 )
2		ply1mpl0.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		ply1mpl0.z	⊢ 0 = ( 0g ‘ 𝑃 )
4		eqidd	⊢ ( ⊤ → ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 ) )
5		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
6		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
7	2 5 6	ply1bas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
8	1	fveq2i	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
9	7 8	eqtr4i	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑀 )
10	9	a1i	⊢ ( ⊤ → ( Base ‘ 𝑃 ) = ( Base ‘ 𝑀 ) )
11		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
12	2 1 11	ply1plusg	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑀 )
13	12	a1i	⊢ ( ⊤ → ( +g ‘ 𝑃 ) = ( +g ‘ 𝑀 ) )
14	13	oveqdr	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) )
15	4 10 14	grpidpropd	⊢ ( ⊤ → ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑀 ) )
16	15	mptru	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑀 )
17	3 16	eqtri	⊢ 0 = ( 0g ‘ 𝑀 )