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

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