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

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 ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psrmon.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
psrmon.z ⊢ 0 = ( 0g ‘ 𝑅 )
psrmon.o ⊢ 1 = ( 1r ‘ 𝑅 )
psrmon.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
psrmon.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
psrmon.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
psrmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
psrmonmul.t ⊢ · = ( .r ‘ 𝑆 )
psrmonmul.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
psrmonmul.g ⊢ 𝐺 = ( 𝑦 ∈ 𝐷 ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) )
Assertion psrmonmul2 ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) · ( 𝐺 ‘ 𝑌 ) ) = ( 𝐺 ‘ ( 𝑋 ∘f + 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 psrmon.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrmon.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 psrmon.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 psrmon.o ⊢ 1 = ( 1r ‘ 𝑅 )
5 psrmon.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
6 psrmon.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
7 psrmon.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
8 psrmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
9 psrmonmul.t ⊢ · = ( .r ‘ 𝑆 )
10 psrmonmul.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
11 psrmonmul.g ⊢ 𝐺 = ( 𝑦 ∈ 𝐷 ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) )
12 1 2 3 4 5 6 7 8 9 10 psrmonmul ⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑋 , 1 , 0 ) ) · ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑌 , 1 , 0 ) ) ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ) )
13 eqeq2 ⊢ ( 𝑦 = 𝑋 → ( 𝑧 = 𝑦 ↔ 𝑧 = 𝑋 ) )
14 13 ifbid ⊢ ( 𝑦 = 𝑋 → if ( 𝑧 = 𝑦 , 1 , 0 ) = if ( 𝑧 = 𝑋 , 1 , 0 ) )
15 14 mpteq2dv ⊢ ( 𝑦 = 𝑋 → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑋 , 1 , 0 ) ) )
16 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
17 5 16 rabex2 ⊢ 𝐷 ∈ V
18 17 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
19 18 mptexd ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑋 , 1 , 0 ) ) ∈ V )
20 11 15 8 19 fvmptd3 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑋 , 1 , 0 ) ) )
21 eqeq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑧 = 𝑦 ↔ 𝑧 = 𝑌 ) )
22 21 ifbid ⊢ ( 𝑦 = 𝑌 → if ( 𝑧 = 𝑦 , 1 , 0 ) = if ( 𝑧 = 𝑌 , 1 , 0 ) )
23 22 mpteq2dv ⊢ ( 𝑦 = 𝑌 → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑌 , 1 , 0 ) ) )
24 18 mptexd ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑌 , 1 , 0 ) ) ∈ V )
25 11 23 10 24 fvmptd3 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑌 , 1 , 0 ) ) )
26 20 25 oveq12d ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) · ( 𝐺 ‘ 𝑌 ) ) = ( ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑋 , 1 , 0 ) ) · ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑌 , 1 , 0 ) ) ) )
27 eqeq2 ⊢ ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) → ( 𝑧 = 𝑦 ↔ 𝑧 = ( 𝑋 ∘f + 𝑌 ) ) )
28 27 ifbid ⊢ ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) → if ( 𝑧 = 𝑦 , 1 , 0 ) = if ( 𝑧 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) )
29 28 mpteq2dv ⊢ ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ) )
30 5 psrbasfsupp ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
31 30 psrbagaddcl ⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) → ( 𝑋 ∘f + 𝑌 ) ∈ 𝐷 )
32 8 10 31 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∘f + 𝑌 ) ∈ 𝐷 )
33 18 mptexd ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ) ∈ V )
34 11 29 32 33 fvmptd3 ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝑋 ∘f + 𝑌 ) ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ) )
35 12 26 34 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) · ( 𝐺 ‘ 𝑌 ) ) = ( 𝐺 ‘ ( 𝑋 ∘f + 𝑌 ) ) )