matvsca2

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

	Ref	Expression
Hypotheses	matvsca2.a	$⊢ A = N Mat R$
	matvsca2.b	$⊢ B = {Base}_{A}$
	matvsca2.k	$⊢ K = {Base}_{R}$
	matvsca2.v	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
	matvsca2.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
	matvsca2.c	$⊢ C = N \times N$
Assertion	matvsca2	$⊢ (X \in K \land Y \in B) \to X \underset{˙}{\cdot} Y = (C \times \{X\}) {\underset{˙}{\times}}_{f} Y$

Proof

Step	Hyp	Ref	Expression
1		matvsca2.a	$⊢ A = N Mat R$
2		matvsca2.b	$⊢ B = {Base}_{A}$
3		matvsca2.k	$⊢ K = {Base}_{R}$
4		matvsca2.v	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
5		matvsca2.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
6		matvsca2.c	$⊢ C = N \times N$
7	1 2	matrcl	$⊢ Y \in B \to (N \in Fin \land R \in V)$
8	7	adantl	$⊢ (X \in K \land Y \in B) \to (N \in Fin \land R \in V)$
9		eqid	$⊢ R freeLMod (N \times N) = R freeLMod (N \times N)$
10	1 9	matvsca	$⊢ (N \in Fin \land R \in V) \to \cdot_{(R freeLMod (N \times N))} = \cdot_{A}$
11	8 10	syl	$⊢ (X \in K \land Y \in B) \to \cdot_{(R freeLMod (N \times N))} = \cdot_{A}$
12	11 4	eqtr4di	$⊢ (X \in K \land Y \in B) \to \cdot_{(R freeLMod (N \times N))} = \underset{˙}{\cdot}$
13	12	oveqd	$⊢ (X \in K \land Y \in B) \to X \cdot_{(R freeLMod (N \times N))} Y = X \underset{˙}{\cdot} Y$
14		eqid	$⊢ {Base}_{(R freeLMod (N \times N))} = {Base}_{(R freeLMod (N \times N))}$
15	8	simpld	$⊢ (X \in K \land Y \in B) \to N \in Fin$
16		xpfi	$⊢ (N \in Fin \land N \in Fin) \to N \times N \in Fin$
17	15 15 16	syl2anc	$⊢ (X \in K \land Y \in B) \to N \times N \in Fin$
18		simpl	$⊢ (X \in K \land Y \in B) \to X \in K$
19		simpr	$⊢ (X \in K \land Y \in B) \to Y \in B$
20	1 9	matbas	$⊢ (N \in Fin \land R \in V) \to {Base}_{(R freeLMod (N \times N))} = {Base}_{A}$
21	8 20	syl	$⊢ (X \in K \land Y \in B) \to {Base}_{(R freeLMod (N \times N))} = {Base}_{A}$
22	21 2	eqtr4di	$⊢ (X \in K \land Y \in B) \to {Base}_{(R freeLMod (N \times N))} = B$
23	19 22	eleqtrrd	$⊢ (X \in K \land Y \in B) \to Y \in {Base}_{(R freeLMod (N \times N))}$
24		eqid	$⊢ \cdot_{(R freeLMod (N \times N))} = \cdot_{(R freeLMod (N \times N))}$
25	9 14 3 17 18 23 24 5	frlmvscafval	$⊢ (X \in K \land Y \in B) \to X \cdot_{(R freeLMod (N \times N))} Y = ((N \times N) \times \{X\}) {\underset{˙}{\times}}_{f} Y$
26	6	xpeq1i	$⊢ C \times \{X\} = (N \times N) \times \{X\}$
27	26	oveq1i	$⊢ (C \times \{X\}) {\underset{˙}{\times}}_{f} Y = ((N \times N) \times \{X\}) {\underset{˙}{\times}}_{f} Y$
28	25 27	eqtr4di	$⊢ (X \in K \land Y \in B) \to X \cdot_{(R freeLMod (N \times N))} Y = (C \times \{X\}) {\underset{˙}{\times}}_{f} Y$
29	13 28	eqtr3d	$⊢ (X \in K \land Y \in B) \to X \underset{˙}{\cdot} Y = (C \times \{X\}) {\underset{˙}{\times}}_{f} Y$

Metamath Proof Explorer

Theorem matvsca2

Proof