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

Metamath Proof Explorer

Theorem pwsvscafval

Description: Scalar multiplication in a structure power is pointwise. (Contributed by Mario Carneiro, 11-Jan-2015)

Ref Expression
Hypotheses pwsvscaval.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
pwsvscaval.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
pwsvscaval.s ⊢ · = ( ·𝑠 ‘ 𝑅 )
pwsvscaval.t ⊢ ∙ = ( ·𝑠 ‘ 𝑌 )
pwsvscaval.f ⊢ 𝐹 = ( Scalar ‘ 𝑅 )
pwsvscaval.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
pwsvscaval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
pwsvscaval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
pwsvscaval.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
pwsvscaval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion pwsvscafval ( 𝜑 → ( 𝐴 ∙ 𝑋 ) = ( ( 𝐼 × { 𝐴 } ) ∘f · 𝑋 ) )

Proof

Step Hyp Ref Expression
1 pwsvscaval.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2 pwsvscaval.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 pwsvscaval.s ⊢ · = ( ·𝑠 ‘ 𝑅 )
4 pwsvscaval.t ⊢ ∙ = ( ·𝑠 ‘ 𝑌 )
5 pwsvscaval.f ⊢ 𝐹 = ( Scalar ‘ 𝑅 )
6 pwsvscaval.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
7 pwsvscaval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
8 pwsvscaval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
9 pwsvscaval.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
10 pwsvscaval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
11 1 5 pwsval ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑌 = ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) )
12 7 8 11 syl2anc ⊢ ( 𝜑 → 𝑌 = ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) )
13 12 fveq2d ⊢ ( 𝜑 → ( ·𝑠 ‘ 𝑌 ) = ( ·𝑠 ‘ ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) ) )
14 4 13 eqtrid ⊢ ( 𝜑 → ∙ = ( ·𝑠 ‘ ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) ) )
15 14 oveqd ⊢ ( 𝜑 → ( 𝐴 ∙ 𝑋 ) = ( 𝐴 ( ·𝑠 ‘ ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) ) 𝑋 ) )
16 eqid ⊢ ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) = ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) )
17 eqid ⊢ ( Base ‘ ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) ) = ( Base ‘ ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) )
18 eqid ⊢ ( ·𝑠 ‘ ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) ) = ( ·𝑠 ‘ ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) )
19 5 fvexi ⊢ 𝐹 ∈ V
20 19 a1i ⊢ ( 𝜑 → 𝐹 ∈ V )
21 fnconstg ⊢ ( 𝑅 ∈ 𝑉 → ( 𝐼 × { 𝑅 } ) Fn 𝐼 )
22 7 21 syl ⊢ ( 𝜑 → ( 𝐼 × { 𝑅 } ) Fn 𝐼 )
23 12 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) ) )
24 2 23 eqtrid ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) ) )
25 10 24 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) ) )
26 16 17 18 6 20 8 22 9 25 prdsvscaval ⊢ ( 𝜑 → ( 𝐴 ( ·𝑠 ‘ ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) ) 𝑋 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝐴 ( ·𝑠 ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑋 ‘ 𝑥 ) ) ) )
27 fvconst2g ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) = 𝑅 )
28 7 27 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) = 𝑅 )
29 28 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ·𝑠 ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) = ( ·𝑠 ‘ 𝑅 ) )
30 29 3 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ·𝑠 ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) = · )
31 30 oveqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐴 ( ·𝑠 ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑋 ‘ 𝑥 ) ) = ( 𝐴 · ( 𝑋 ‘ 𝑥 ) ) )
32 31 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝐴 ( ·𝑠 ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑋 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝐴 · ( 𝑋 ‘ 𝑥 ) ) ) )
33 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐴 ∈ 𝐾 )
34 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑥 ) ∈ V )
35 fconstmpt ⊢ ( 𝐼 × { 𝐴 } ) = ( 𝑥 ∈ 𝐼 ↦ 𝐴 )
36 35 a1i ⊢ ( 𝜑 → ( 𝐼 × { 𝐴 } ) = ( 𝑥 ∈ 𝐼 ↦ 𝐴 ) )
37 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
38 1 37 2 7 8 10 pwselbas ⊢ ( 𝜑 → 𝑋 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
39 38 feqmptd ⊢ ( 𝜑 → 𝑋 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑥 ) ) )
40 8 33 34 36 39 offval2 ⊢ ( 𝜑 → ( ( 𝐼 × { 𝐴 } ) ∘f · 𝑋 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝐴 · ( 𝑋 ‘ 𝑥 ) ) ) )
41 32 40 eqtr4d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝐴 ( ·𝑠 ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑋 ‘ 𝑥 ) ) ) = ( ( 𝐼 × { 𝐴 } ) ∘f · 𝑋 ) )
42 15 26 41 3eqtrd ⊢ ( 𝜑 → ( 𝐴 ∙ 𝑋 ) = ( ( 𝐼 × { 𝐴 } ) ∘f · 𝑋 ) )