Theorem pwsmulrval

Description: Value of multiplication in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015)

	Ref	Expression
Hypotheses	pwsplusgval.y	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
	pwsplusgval.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	pwsplusgval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	pwsplusgval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	pwsplusgval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	pwsplusgval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
	pwsmulrval.a	⊢ · = ( .r ‘ 𝑅 )
	pwsmulrval.p	⊢ ∙ = ( .r ‘ 𝑌 )
Assertion	pwsmulrval	⊢ ( 𝜑 → ( 𝐹 ∙ 𝐺 ) = ( 𝐹 ∘f · 𝐺 ) )

Proof

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