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 · 𝑋 ) )