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 ⊢ P = I mPoly R
mpl0.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
mpl0.o ⊢ O = 0 R
mpl0.z ⊢ 0 ˙ = 0 P
mpl0.i ⊢ φ → I ∈ W
mpl0.r ⊢ φ → R ∈ Grp
Assertion mpl0 ⊢ φ → 0 ˙ = D × O

Proof

Step Hyp Ref Expression
1 mpl0.p ⊢ P = I mPoly R
2 mpl0.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
3 mpl0.o ⊢ O = 0 R
4 mpl0.z ⊢ 0 ˙ = 0 P
5 mpl0.i ⊢ φ → I ∈ W
6 mpl0.r ⊢ φ → R ∈ Grp
7 eqid ⊢ I mPwSer R = I mPwSer R
8 eqid ⊢ Base P = Base P
9 7 1 8 5 6 mplsubg ⊢ φ → Base P ∈ SubGrp ⁡ I mPwSer R
10 1 7 8 mplval2 ⊢ P = I mPwSer R ↾ 𝑠 Base P
11 eqid ⊢ 0 I mPwSer R = 0 I mPwSer R
12 10 11 subg0 ⊢ Base P ∈ SubGrp ⁡ I mPwSer R → 0 I mPwSer R = 0 P
13 9 12 syl ⊢ φ → 0 I mPwSer R = 0 P
14 7 5 6 2 3 11 psr0 ⊢ φ → 0 I mPwSer R = D × O
15 13 14 eqtr3d ⊢ φ → 0 P = D × O
16 4 15 eqtrid ⊢ φ → 0 ˙ = D × O