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

Metamath Proof Explorer

Theorem prdsvscafval

Description: Scalar multiplication of a single coordinate in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015)

Ref Expression
Hypotheses prdsbasmpt.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
prdsbasmpt.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
prdsvscaval.t ⊢ · = ( ·𝑠 ‘ 𝑌 )
prdsvscaval.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
prdsvscaval.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
prdsvscaval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
prdsvscaval.r ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
prdsvscaval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐾 )
prdsvscaval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
prdsvscafval.j ⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
Assertion prdsvscafval ( 𝜑 → ( ( 𝐹 · 𝐺 ) ‘ 𝐽 ) = ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝐽 ) ) ( 𝐺 ‘ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 prdsbasmpt.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdsbasmpt.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 prdsvscaval.t ⊢ · = ( ·𝑠 ‘ 𝑌 )
4 prdsvscaval.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
5 prdsvscaval.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
6 prdsvscaval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
7 prdsvscaval.r ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
8 prdsvscaval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐾 )
9 prdsvscaval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
10 prdsvscafval.j ⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
11 1 2 3 4 5 6 7 8 9 prdsvscaval ⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )
12 2fveq3 ⊢ ( 𝑥 = 𝐽 → ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) = ( ·𝑠 ‘ ( 𝑅 ‘ 𝐽 ) ) )
13 eqidd ⊢ ( 𝑥 = 𝐽 → 𝐹 = 𝐹 )
14 fveq2 ⊢ ( 𝑥 = 𝐽 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝐽 ) )
15 12 13 14 oveq123d ⊢ ( 𝑥 = 𝐽 → ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) = ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝐽 ) ) ( 𝐺 ‘ 𝐽 ) ) )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐽 ) → ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) = ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝐽 ) ) ( 𝐺 ‘ 𝐽 ) ) )
17 ovexd ⊢ ( 𝜑 → ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝐽 ) ) ( 𝐺 ‘ 𝐽 ) ) ∈ V )
18 11 16 10 17 fvmptd ⊢ ( 𝜑 → ( ( 𝐹 · 𝐺 ) ‘ 𝐽 ) = ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝐽 ) ) ( 𝐺 ‘ 𝐽 ) ) )