Metamath Proof Explorer

Theorem psrmonmul2

Description: The product of two power series monomials adds the exponent vectors together. Here, the function G is a monomial builder, which maps a bag of variables with the monic monomial with only those variables. (Contributed by Thierry Arnoux, 16-Mar-2026)

Ref Expression
Hypotheses psrmon.s 
|- S = ( I mPwSer R )
psrmon.b 
|- B = ( Base ` S )
psrmon.z 
|- .0. = ( 0g ` R )
psrmon.o 
|- .1. = ( 1r ` R )
psrmon.d 
|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
psrmon.i 
|- ( ph -> I e. W )
psrmon.r 
|- ( ph -> R e. Ring )
psrmon.x 
|- ( ph -> X e. D )
psrmonmul.t 
|- .x. = ( .r ` S )
psrmonmul.y 
|- ( ph -> Y e. D )
psrmonmul.g 
|- G = ( y e. D |-> ( z e. D |-> if ( z = y , .1. , .0. ) ) )
Assertion psrmonmul2 
|- ( ph -> ( ( G ` X ) .x. ( G ` Y ) ) = ( G ` ( X oF + Y ) ) )

Proof

Step Hyp Ref Expression
1 psrmon.s 
 |-  S = ( I mPwSer R )
2 psrmon.b 
 |-  B = ( Base ` S )
3 psrmon.z 
 |-  .0. = ( 0g ` R )
4 psrmon.o 
 |-  .1. = ( 1r ` R )
5 psrmon.d 
 |-  D = { h e. ( NN0 ^m I ) | h finSupp 0 }
6 psrmon.i 
 |-  ( ph -> I e. W )
7 psrmon.r 
 |-  ( ph -> R e. Ring )
8 psrmon.x 
 |-  ( ph -> X e. D )
9 psrmonmul.t 
 |-  .x. = ( .r ` S )
10 psrmonmul.y 
 |-  ( ph -> Y e. D )
11 psrmonmul.g 
 |-  G = ( y e. D |-> ( z e. D |-> if ( z = y , .1. , .0. ) ) )
12 1 2 3 4 5 6 7 8 9 10 psrmonmul 
 |-  ( ph -> ( ( z e. D |-> if ( z = X , .1. , .0. ) ) .x. ( z e. D |-> if ( z = Y , .1. , .0. ) ) ) = ( z e. D |-> if ( z = ( X oF + Y ) , .1. , .0. ) ) )
13 eqeq2 
 |-  ( y = X -> ( z = y <-> z = X ) )
14 13 ifbid 
 |-  ( y = X -> if ( z = y , .1. , .0. ) = if ( z = X , .1. , .0. ) )
15 14 mpteq2dv 
 |-  ( y = X -> ( z e. D |-> if ( z = y , .1. , .0. ) ) = ( z e. D |-> if ( z = X , .1. , .0. ) ) )
16 ovex 
 |-  ( NN0 ^m I ) e. _V
17 5 16 rabex2 
 |-  D e. _V
18 17 a1i 
 |-  ( ph -> D e. _V )
19 18 mptexd 
 |-  ( ph -> ( z e. D |-> if ( z = X , .1. , .0. ) ) e. _V )
20 11 15 8 19 fvmptd3 
 |-  ( ph -> ( G ` X ) = ( z e. D |-> if ( z = X , .1. , .0. ) ) )
21 eqeq2 
 |-  ( y = Y -> ( z = y <-> z = Y ) )
22 21 ifbid 
 |-  ( y = Y -> if ( z = y , .1. , .0. ) = if ( z = Y , .1. , .0. ) )
23 22 mpteq2dv 
 |-  ( y = Y -> ( z e. D |-> if ( z = y , .1. , .0. ) ) = ( z e. D |-> if ( z = Y , .1. , .0. ) ) )
24 18 mptexd 
 |-  ( ph -> ( z e. D |-> if ( z = Y , .1. , .0. ) ) e. _V )
25 11 23 10 24 fvmptd3 
 |-  ( ph -> ( G ` Y ) = ( z e. D |-> if ( z = Y , .1. , .0. ) ) )
26 20 25 oveq12d 
 |-  ( ph -> ( ( G ` X ) .x. ( G ` Y ) ) = ( ( z e. D |-> if ( z = X , .1. , .0. ) ) .x. ( z e. D |-> if ( z = Y , .1. , .0. ) ) ) )
27 eqeq2 
 |-  ( y = ( X oF + Y ) -> ( z = y <-> z = ( X oF + Y ) ) )
28 27 ifbid 
 |-  ( y = ( X oF + Y ) -> if ( z = y , .1. , .0. ) = if ( z = ( X oF + Y ) , .1. , .0. ) )
29 28 mpteq2dv 
 |-  ( y = ( X oF + Y ) -> ( z e. D |-> if ( z = y , .1. , .0. ) ) = ( z e. D |-> if ( z = ( X oF + Y ) , .1. , .0. ) ) )
30 5 psrbasfsupp 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
31 30 psrbagaddcl 
 |-  ( ( X e. D /\ Y e. D ) -> ( X oF + Y ) e. D )
32 8 10 31 syl2anc 
 |-  ( ph -> ( X oF + Y ) e. D )
33 18 mptexd 
 |-  ( ph -> ( z e. D |-> if ( z = ( X oF + Y ) , .1. , .0. ) ) e. _V )
34 11 29 32 33 fvmptd3 
 |-  ( ph -> ( G ` ( X oF + Y ) ) = ( z e. D |-> if ( z = ( X oF + Y ) , .1. , .0. ) ) )
35 12 26 34 3eqtr4d 
 |-  ( ph -> ( ( G ` X ) .x. ( G ` Y ) ) = ( G ` ( X oF + Y ) ) )