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

Metamath Proof Explorer

Theorem psrvscaval

Description: The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014)

Ref Expression
Hypotheses psrvsca.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psrvsca.n ⊢ ∙ = ( ·𝑠 ‘ 𝑆 )
psrvsca.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
psrvsca.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
psrvsca.m ⊢ · = ( .r ‘ 𝑅 )
psrvsca.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
psrvsca.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
psrvsca.y ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
psrvscaval.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
Assertion psrvscaval ( 𝜑 → ( ( 𝑋 ∙ 𝐹 ) ‘ 𝑌 ) = ( 𝑋 · ( 𝐹 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 psrvsca.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrvsca.n ⊢ ∙ = ( ·𝑠 ‘ 𝑆 )
3 psrvsca.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
4 psrvsca.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
5 psrvsca.m ⊢ · = ( .r ‘ 𝑅 )
6 psrvsca.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
7 psrvsca.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
8 psrvsca.y ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
9 psrvscaval.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
10 1 2 3 4 5 6 7 8 psrvsca ⊢ ( 𝜑 → ( 𝑋 ∙ 𝐹 ) = ( ( 𝐷 × { 𝑋 } ) ∘f · 𝐹 ) )
11 10 fveq1d ⊢ ( 𝜑 → ( ( 𝑋 ∙ 𝐹 ) ‘ 𝑌 ) = ( ( ( 𝐷 × { 𝑋 } ) ∘f · 𝐹 ) ‘ 𝑌 ) )
12 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
13 6 12 rabex2 ⊢ 𝐷 ∈ V
14 13 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
15 1 3 6 4 8 psrelbas ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝐾 )
16 15 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
17 eqidd ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑌 ) )
18 14 7 16 17 ofc1 ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐷 ) → ( ( ( 𝐷 × { 𝑋 } ) ∘f · 𝐹 ) ‘ 𝑌 ) = ( 𝑋 · ( 𝐹 ‘ 𝑌 ) ) )
19 9 18 mpdan ⊢ ( 𝜑 → ( ( ( 𝐷 × { 𝑋 } ) ∘f · 𝐹 ) ‘ 𝑌 ) = ( 𝑋 · ( 𝐹 ‘ 𝑌 ) ) )
20 11 19 eqtrd ⊢ ( 𝜑 → ( ( 𝑋 ∙ 𝐹 ) ‘ 𝑌 ) = ( 𝑋 · ( 𝐹 ‘ 𝑌 ) ) )