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 = ( invg ` R )
mplneg.m 
|- M = ( invg ` P )
mplneg.i 
|- ( ph -> I e. V )
mplneg.r 
|- ( ph -> R e. Grp )
mplneg.x 
|- ( ph -> X e. B )
Assertion mplneg 
|- ( ph -> ( M ` X ) = ( N o. X ) )

Proof

Step Hyp Ref Expression
1 mplneg.p 
 |-  P = ( I mPoly R )
2 mplneg.b 
 |-  B = ( Base ` P )
3 mplneg.n 
 |-  N = ( invg ` R )
4 mplneg.m 
 |-  M = ( invg ` P )
5 mplneg.i 
 |-  ( ph -> I e. V )
6 mplneg.r 
 |-  ( ph -> R e. Grp )
7 mplneg.x 
 |-  ( ph -> X e. B )
8 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
9 8 1 2 5 6 mplsubg 
 |-  ( ph -> B e. ( SubGrp ` ( I mPwSer R ) ) )
10 1 8 2 mplval2 
 |-  P = ( ( I mPwSer R ) |`s B )
11 eqid 
 |-  ( invg ` ( I mPwSer R ) ) = ( invg ` ( I mPwSer R ) )
12 10 11 4 subginv 
 |-  ( ( B e. ( SubGrp ` ( I mPwSer R ) ) /\ X e. B ) -> ( ( invg ` ( I mPwSer R ) ) ` X ) = ( M ` X ) )
13 9 7 12 syl2anc 
 |-  ( ph -> ( ( invg ` ( I mPwSer R ) ) ` X ) = ( M ` X ) )
14 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
15 eqid 
 |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
16 1 8 2 15 mplbasss 
 |-  B C_ ( Base ` ( I mPwSer R ) )
17 16 sseli 
 |-  ( X e. B -> X e. ( Base ` ( I mPwSer R ) ) )
18 7 17 syl 
 |-  ( ph -> X e. ( Base ` ( I mPwSer R ) ) )
19 8 5 6 14 3 15 11 18 psrneg 
 |-  ( ph -> ( ( invg ` ( I mPwSer R ) ) ` X ) = ( N o. X ) )
20 13 19 eqtr3d 
 |-  ( ph -> ( M ` X ) = ( N o. X ) )