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

Metamath Proof Explorer

Theorem psrvsca

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 ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion psrvsca ( 𝜑 → ( 𝑋 ∙ 𝐹 ) = ( ( 𝐷 × { 𝑋 } ) ∘f · 𝐹 ) )

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 sneq ⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
10 9 xpeq2d ⊢ ( 𝑥 = 𝑋 → ( 𝐷 × { 𝑥 } ) = ( 𝐷 × { 𝑋 } ) )
11 10 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐷 × { 𝑥 } ) ∘f · 𝑓 ) = ( ( 𝐷 × { 𝑋 } ) ∘f · 𝑓 ) )
12 oveq2 ⊢ ( 𝑓 = 𝐹 → ( ( 𝐷 × { 𝑋 } ) ∘f · 𝑓 ) = ( ( 𝐷 × { 𝑋 } ) ∘f · 𝐹 ) )
13 1 2 3 4 5 6 psrvscafval ⊢ ∙ = ( 𝑥 ∈ 𝐾 , 𝑓 ∈ 𝐵 ↦ ( ( 𝐷 × { 𝑥 } ) ∘f · 𝑓 ) )
14 ovex ⊢ ( ( 𝐷 × { 𝑋 } ) ∘f · 𝐹 ) ∈ V
15 11 12 13 14 ovmpo ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝐹 ∈ 𝐵 ) → ( 𝑋 ∙ 𝐹 ) = ( ( 𝐷 × { 𝑋 } ) ∘f · 𝐹 ) )
16 7 8 15 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∙ 𝐹 ) = ( ( 𝐷 × { 𝑋 } ) ∘f · 𝐹 ) )