Metamath Proof Explorer


Theorem mplneg

Description: The negative function on multivariate polynomials. (Contributed by SN, 25-May-2024)

Ref Expression
Hypotheses mplneg.p P = I mPoly R
mplneg.b B = Base P
mplneg.n N = inv g R
mplneg.m M = inv g P
mplneg.i φ I V
mplneg.r φ R Grp
mplneg.x φ X B
Assertion mplneg φ M X = N X

Proof

Step Hyp Ref Expression
1 mplneg.p P = I mPoly R
2 mplneg.b B = Base P
3 mplneg.n N = inv g R
4 mplneg.m M = inv g P
5 mplneg.i φ I V
6 mplneg.r φ R Grp
7 mplneg.x φ X B
8 eqid I mPwSer R = I mPwSer R
9 8 1 2 5 6 mplsubg φ B SubGrp I mPwSer R
10 1 8 2 mplval2 P = I mPwSer R 𝑠 B
11 eqid inv g I mPwSer R = inv g I mPwSer R
12 10 11 4 subginv B SubGrp I mPwSer R X B inv g I mPwSer R X = M X
13 9 7 12 syl2anc φ inv g I mPwSer R X = M X
14 eqid f 0 I | f -1 Fin = f 0 I | f -1 Fin
15 eqid Base I mPwSer R = Base I mPwSer R
16 1 8 2 15 mplbasss B Base I mPwSer R
17 16 sseli X B X Base I mPwSer R
18 7 17 syl φ X Base I mPwSer R
19 8 5 6 14 3 15 11 18 psrneg φ inv g I mPwSer R X = N X
20 13 19 eqtr3d φ M X = N X