Theorem mpl0

Description: The zero polynomial. (Contributed by Mario Carneiro, 9-Jan-2015)

	Ref	Expression
Hypotheses	mpl0.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mpl0.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
	mpl0.o	⊢ 𝑂 = ( 0g ‘ 𝑅 )
	mpl0.z	⊢ 0 = ( 0g ‘ 𝑃 )
	mpl0.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	mpl0.r	⊢ ( 𝜑 → 𝑅 ∈ Grp )
Assertion	mpl0	⊢ ( 𝜑 → 0 = ( 𝐷 × { 𝑂 } ) )

Proof

Step	Hyp	Ref	Expression
1		mpl0.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mpl0.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
3		mpl0.o	⊢ 𝑂 = ( 0g ‘ 𝑅 )
4		mpl0.z	⊢ 0 = ( 0g ‘ 𝑃 )
5		mpl0.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6		mpl0.r	⊢ ( 𝜑 → 𝑅 ∈ Grp )
7		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
8		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
9	7 1 8 5 6	mplsubg	⊢ ( 𝜑 → ( Base ‘ 𝑃 ) ∈ ( SubGrp ‘ ( 𝐼 mPwSer 𝑅 ) ) )
10	1 7 8	mplval2	⊢ 𝑃 = ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ 𝑃 ) )
11		eqid	⊢ ( 0g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( 0g ‘ ( 𝐼 mPwSer 𝑅 ) )
12	10 11	subg0	⊢ ( ( Base ‘ 𝑃 ) ∈ ( SubGrp ‘ ( 𝐼 mPwSer 𝑅 ) ) → ( 0g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( 0g ‘ 𝑃 ) )
13	9 12	syl	⊢ ( 𝜑 → ( 0g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( 0g ‘ 𝑃 ) )
14	7 5 6 2 3 11	psr0	⊢ ( 𝜑 → ( 0g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( 𝐷 × { 𝑂 } ) )
15	13 14	eqtr3d	⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) = ( 𝐷 × { 𝑂 } ) )
16	4 15	syl5eq	⊢ ( 𝜑 → 0 = ( 𝐷 × { 𝑂 } ) )