matmulcell

Description: Multiplication in the matrix ring for a single cell of a matrix. (Contributed by AV, 17-Nov-2019) (Revised by AV, 3-Jul-2022)

	Ref	Expression
Hypotheses	matmulcell.a	$⊢ A = N Mat R$
	matmulcell.b	$⊢ B = {Base}_{A}$
	matmulcell.m	$⊢ \underset{˙}{\times} = \cdot_{A}$
Assertion	matmulcell	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to I (X \underset{˙}{\times} Y) J = \underset{j \in N}{\sum_{R}} ((I X j) \cdot_{R} (j Y J))$

Proof

Step	Hyp	Ref	Expression
1		matmulcell.a	$⊢ A = N Mat R$
2		matmulcell.b	$⊢ B = {Base}_{A}$
3		matmulcell.m	$⊢ \underset{˙}{\times} = \cdot_{A}$
4	1 2	matrcl	$⊢ X \in B \to (N \in Fin \land R \in V)$
5		eqid	$⊢ R maMul ⟨N, N, N⟩ = R maMul ⟨N, N, N⟩$
6	1 5	matmulr	$⊢ (N \in Fin \land R \in V) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
7	6 3	syl6reqr	$⊢ (N \in Fin \land R \in V) \to \underset{˙}{\times} = R maMul ⟨N, N, N⟩$
8	7	a1d	$⊢ (N \in Fin \land R \in V) \to (R \in Ring \to \underset{˙}{\times} = R maMul ⟨N, N, N⟩)$
9	4 8	syl	$⊢ X \in B \to (R \in Ring \to \underset{˙}{\times} = R maMul ⟨N, N, N⟩)$
10	9	adantr	$⊢ (X \in B \land Y \in B) \to (R \in Ring \to \underset{˙}{\times} = R maMul ⟨N, N, N⟩)$
11	10	impcom	$⊢ (R \in Ring \land (X \in B \land Y \in B)) \to \underset{˙}{\times} = R maMul ⟨N, N, N⟩$
12	11	3adant3	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to \underset{˙}{\times} = R maMul ⟨N, N, N⟩$
13	12	oveqd	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to X \underset{˙}{\times} Y = X (R maMul ⟨N, N, N⟩) Y$
14	13	oveqd	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to I (X \underset{˙}{\times} Y) J = I (X (R maMul ⟨N, N, N⟩) Y) J$
15		eqid	$⊢ {Base}_{R} = {Base}_{R}$
16		eqid	$⊢ \cdot_{R} = \cdot_{R}$
17		simp1	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to R \in Ring$
18	4	simpld	$⊢ X \in B \to N \in Fin$
19	18	adantr	$⊢ (X \in B \land Y \in B) \to N \in Fin$
20	19	3ad2ant2	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to N \in Fin$
21	1 15 2	matbas2i	$⊢ X \in B \to X \in ({Base}_{R}^{(N \times N)})$
22	21	adantr	$⊢ (X \in B \land Y \in B) \to X \in ({Base}_{R}^{(N \times N)})$
23	22	3ad2ant2	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to X \in ({Base}_{R}^{(N \times N)})$
24	1 15 2	matbas2i	$⊢ Y \in B \to Y \in ({Base}_{R}^{(N \times N)})$
25	24	adantl	$⊢ (X \in B \land Y \in B) \to Y \in ({Base}_{R}^{(N \times N)})$
26	25	3ad2ant2	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to Y \in ({Base}_{R}^{(N \times N)})$
27		simp3l	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to I \in N$
28		simp3r	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to J \in N$
29	5 15 16 17 20 20 20 23 26 27 28	mamufv	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to I (X (R maMul ⟨N, N, N⟩) Y) J = \underset{j \in N}{\sum_{R}} ((I X j) \cdot_{R} (j Y J))$
30	14 29	eqtrd	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to I (X \underset{˙}{\times} Y) J = \underset{j \in N}{\sum_{R}} ((I X j) \cdot_{R} (j Y J))$

Metamath Proof Explorer

Theorem matmulcell

Proof