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 𝐷 = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ 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 𝐷 = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ 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 · 𝐹 ) )