Theorem matvsca2

Description: Scalar multiplication in the matrix ring is cell-wise. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	matvsca2.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	matvsca2.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	matvsca2.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	matvsca2.v	⊢ · = ( ·𝑠 ‘ 𝐴 )
	matvsca2.t	⊢ × = ( .r ‘ 𝑅 )
	matvsca2.c	⊢ 𝐶 = ( 𝑁 × 𝑁 )
Assertion	matvsca2	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) = ( ( 𝐶 × { 𝑋 } ) ∘f × 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		matvsca2.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		matvsca2.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		matvsca2.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		matvsca2.v	⊢ · = ( ·𝑠 ‘ 𝐴 )
5		matvsca2.t	⊢ × = ( .r ‘ 𝑅 )
6		matvsca2.c	⊢ 𝐶 = ( 𝑁 × 𝑁 )
7	1 2	matrcl	⊢ ( 𝑌 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
8	7	adantl	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
9		eqid	⊢ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
10	1 9	matvsca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( ·𝑠 ‘ 𝐴 ) )
11	8 10	syl	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( ·𝑠 ‘ 𝐴 ) )
12	11 4	eqtr4di	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = · )
13	12	oveqd	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) 𝑌 ) = ( 𝑋 · 𝑌 ) )
14		eqid	⊢ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) )
15	8	simpld	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑁 ∈ Fin )
16		xpfi	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑁 × 𝑁 ) ∈ Fin )
17	15 15 16	syl2anc	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 × 𝑁 ) ∈ Fin )
18		simpl	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐾 )
19		simpr	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
20	1 9	matbas	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ 𝐴 ) )
21	8 20	syl	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ 𝐴 ) )
22	21 2	eqtr4di	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = 𝐵 )
23	19 22	eleqtrrd	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
24		eqid	⊢ ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) )
25	9 14 3 17 18 23 24 5	frlmvscafval	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) 𝑌 ) = ( ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∘f × 𝑌 ) )
26	6	xpeq1i	⊢ ( 𝐶 × { 𝑋 } ) = ( ( 𝑁 × 𝑁 ) × { 𝑋 } )
27	26	oveq1i	⊢ ( ( 𝐶 × { 𝑋 } ) ∘f × 𝑌 ) = ( ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∘f × 𝑌 )
28	25 27	eqtr4di	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) 𝑌 ) = ( ( 𝐶 × { 𝑋 } ) ∘f × 𝑌 ) )
29	13 28	eqtr3d	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) = ( ( 𝐶 × { 𝑋 } ) ∘f × 𝑌 ) )