matvscacell

Description: Scalar multiplication in the matrix ring is cell-wise. (Contributed by AV, 7-Aug-2019)

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

Proof

Step	Hyp	Ref	Expression
1		matplusgcell.a	$⊢ A = N Mat R$
2		matplusgcell.b	$⊢ B = {Base}_{A}$
3		matvscacell.k	$⊢ K = {Base}_{R}$
4		matvscacell.v	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
5		matvscacell.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
6		eqid	$⊢ N \times N = N \times N$
7	1 2 3 4 5 6	matvsca2	$⊢ (X \in K \land Y \in B) \to X \underset{˙}{\cdot} Y = ((N \times N) \times \{X\}) {\underset{˙}{\times}}_{f} Y$
8	7	oveqd	$⊢ (X \in K \land Y \in B) \to I (X \underset{˙}{\cdot} Y) J = I (((N \times N) \times \{X\}) {\underset{˙}{\times}}_{f} Y) J$
9	8	3ad2ant2	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land (I \in N \land J \in N)) \to I (X \underset{˙}{\cdot} Y) J = I (((N \times N) \times \{X\}) {\underset{˙}{\times}}_{f} Y) J$
10		df-ov	$⊢ I (((N \times N) \times \{X\}) {\underset{˙}{\times}}_{f} Y) J = (((N \times N) \times \{X\}) {\underset{˙}{\times}}_{f} Y) (⟨I, J⟩)$
11	10	a1i	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land (I \in N \land J \in N)) \to I (((N \times N) \times \{X\}) {\underset{˙}{\times}}_{f} Y) J = (((N \times N) \times \{X\}) {\underset{˙}{\times}}_{f} Y) (⟨I, J⟩)$
12		opelxpi	$⊢ (I \in N \land J \in N) \to ⟨I, J⟩ \in (N \times N)$
13	12	3ad2ant3	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land (I \in N \land J \in N)) \to ⟨I, J⟩ \in (N \times N)$
14	1 2	matrcl	$⊢ Y \in B \to (N \in Fin \land R \in V)$
15	14	simpld	$⊢ Y \in B \to N \in Fin$
16	15	adantl	$⊢ (X \in K \land Y \in B) \to N \in Fin$
17	16	3ad2ant2	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land (I \in N \land J \in N)) \to N \in Fin$
18		xpfi	$⊢ (N \in Fin \land N \in Fin) \to N \times N \in Fin$
19	17 17 18	syl2anc	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land (I \in N \land J \in N)) \to N \times N \in Fin$
20		simp2l	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land (I \in N \land J \in N)) \to X \in K$
21	2	eleq2i	$⊢ Y \in B \leftrightarrow Y \in {Base}_{A}$
22	21	bilani	$⊢ (X \in K \land Y \in B) \to Y \in {Base}_{A}$
23	22	3ad2ant2	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land (I \in N \land J \in N)) \to Y \in {Base}_{A}$
24		simp1	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land (I \in N \land J \in N)) \to R \in Ring$
25		eqid	$⊢ {Base}_{R} = {Base}_{R}$
26	1 25	matbas2	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{R}^{(N \times N)} = {Base}_{A}$
27	17 24 26	syl2anc	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land (I \in N \land J \in N)) \to {Base}_{R}^{(N \times N)} = {Base}_{A}$
28	23 27	eleqtrrd	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land (I \in N \land J \in N)) \to Y \in ({Base}_{R}^{(N \times N)})$
29		elmapfn	$⊢ Y \in ({Base}_{R}^{(N \times N)}) \to Y Fn (N \times N)$
30	28 29	syl	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land (I \in N \land J \in N)) \to Y Fn (N \times N)$
31		df-ov	$⊢ I Y J = Y (⟨I, J⟩)$
32	31	eqcomi	$⊢ Y (⟨I, J⟩) = I Y J$
33	32	a1i	$⊢ ((R \in Ring \land (X \in K \land Y \in B) \land (I \in N \land J \in N)) \land ⟨I, J⟩ \in (N \times N)) \to Y (⟨I, J⟩) = I Y J$
34	19 20 30 33	ofc1	$⊢ ((R \in Ring \land (X \in K \land Y \in B) \land (I \in N \land J \in N)) \land ⟨I, J⟩ \in (N \times N)) \to (((N \times N) \times \{X\}) {\underset{˙}{\times}}_{f} Y) (⟨I, J⟩) = X \underset{˙}{\times} (I Y J)$
35	13 34	mpdan	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land (I \in N \land J \in N)) \to (((N \times N) \times \{X\}) {\underset{˙}{\times}}_{f} Y) (⟨I, J⟩) = X \underset{˙}{\times} (I Y J)$
36	9 11 35	3eqtrd	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land (I \in N \land J \in N)) \to I (X \underset{˙}{\cdot} Y) J = X \underset{˙}{\times} (I Y J)$

Metamath Proof Explorer

Theorem matvscacell

Proof