This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝜑 → 0 = ( 𝐷 × { 𝑂 } ) )