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	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
6	2 5	ply1bas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
7	1	fveq2i	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
8	6 7	eqtr4i	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑀 )
9	8	a1i	⊢ ( ⊤ → ( Base ‘ 𝑃 ) = ( Base ‘ 𝑀 ) )
10		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
11	2 1 10	ply1plusg	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑀 )
12	11	a1i	⊢ ( ⊤ → ( +g ‘ 𝑃 ) = ( +g ‘ 𝑀 ) )
13	12	oveqdr	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) )
14	4 9 13	grpidpropd	⊢ ( ⊤ → ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑀 ) )
15	14	mptru	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑀 )
16	3 15	eqtri	⊢ 0 = ( 0g ‘ 𝑀 )