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	syl5eq	⊢ ( 𝜑 → ∙ = ( ·𝑠 ‘ ( 𝐹 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	syl5eq	⊢ ( 𝜑 → 𝐵 = ( 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 · 𝑋 ) )