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 syl5eq φ 0 ˙ = D × O