Theorem frlmvscaval

Description: Coordinates of a scalar multiple with respect to a basis in a free module. (Contributed by Stefan O'Rear, 3-Feb-2015)

	Ref	Expression
Hypotheses	frlmvscaval.y	⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
	frlmvscaval.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	frlmvscaval.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	frlmvscaval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	frlmvscaval.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
	frlmvscaval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	frlmvscaval.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
	frlmvscaval.v	⊢ ∙ = ( ·𝑠 ‘ 𝑌 )
	frlmvscaval.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	frlmvscaval	⊢ ( 𝜑 → ( ( 𝐴 ∙ 𝑋 ) ‘ 𝐽 ) = ( 𝐴 · ( 𝑋 ‘ 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		frlmvscaval.y	⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
2		frlmvscaval.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
3		frlmvscaval.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		frlmvscaval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5		frlmvscaval.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
6		frlmvscaval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7		frlmvscaval.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
8		frlmvscaval.v	⊢ ∙ = ( ·𝑠 ‘ 𝑌 )
9		frlmvscaval.t	⊢ · = ( .r ‘ 𝑅 )
10	1 2 3 4 5 6 8 9	frlmvscafval	⊢ ( 𝜑 → ( 𝐴 ∙ 𝑋 ) = ( ( 𝐼 × { 𝐴 } ) ∘f · 𝑋 ) )
11	10	fveq1d	⊢ ( 𝜑 → ( ( 𝐴 ∙ 𝑋 ) ‘ 𝐽 ) = ( ( ( 𝐼 × { 𝐴 } ) ∘f · 𝑋 ) ‘ 𝐽 ) )
12		fnconstg	⊢ ( 𝐴 ∈ 𝐾 → ( 𝐼 × { 𝐴 } ) Fn 𝐼 )
13	5 12	syl	⊢ ( 𝜑 → ( 𝐼 × { 𝐴 } ) Fn 𝐼 )
14	1 3 2	frlmbasf	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 : 𝐼 ⟶ 𝐾 )
15	4 6 14	syl2anc	⊢ ( 𝜑 → 𝑋 : 𝐼 ⟶ 𝐾 )
16	15	ffnd	⊢ ( 𝜑 → 𝑋 Fn 𝐼 )
17		fnfvof	⊢ ( ( ( ( 𝐼 × { 𝐴 } ) Fn 𝐼 ∧ 𝑋 Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) ) → ( ( ( 𝐼 × { 𝐴 } ) ∘f · 𝑋 ) ‘ 𝐽 ) = ( ( ( 𝐼 × { 𝐴 } ) ‘ 𝐽 ) · ( 𝑋 ‘ 𝐽 ) ) )
18	13 16 4 7 17	syl22anc	⊢ ( 𝜑 → ( ( ( 𝐼 × { 𝐴 } ) ∘f · 𝑋 ) ‘ 𝐽 ) = ( ( ( 𝐼 × { 𝐴 } ) ‘ 𝐽 ) · ( 𝑋 ‘ 𝐽 ) ) )
19		fvconst2g	⊢ ( ( 𝐴 ∈ 𝐾 ∧ 𝐽 ∈ 𝐼 ) → ( ( 𝐼 × { 𝐴 } ) ‘ 𝐽 ) = 𝐴 )
20	5 7 19	syl2anc	⊢ ( 𝜑 → ( ( 𝐼 × { 𝐴 } ) ‘ 𝐽 ) = 𝐴 )
21	20	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐼 × { 𝐴 } ) ‘ 𝐽 ) · ( 𝑋 ‘ 𝐽 ) ) = ( 𝐴 · ( 𝑋 ‘ 𝐽 ) ) )
22	11 18 21	3eqtrd	⊢ ( 𝜑 → ( ( 𝐴 ∙ 𝑋 ) ‘ 𝐽 ) = ( 𝐴 · ( 𝑋 ‘ 𝐽 ) ) )