mamudm

Description: The domain of the matrix multiplication function. (Contributed by AV, 10-Feb-2019)

	Ref	Expression
Hypotheses	mamudm.e	$⊢ E = R freeLMod (M \times N)$
	mamudm.b	$⊢ B = {Base}_{E}$
	mamudm.f	$⊢ F = R freeLMod (N \times P)$
	mamudm.c	$⊢ C = {Base}_{F}$
	mamudm.m	$⊢ \underset{˙}{\times} = R maMul ⟨M, N, P⟩$
Assertion	mamudm	$⊢ (R \in V \land (M \in Fin \land N \in Fin \land P \in Fin)) \to dom \underset{˙}{\times} = B \times C$

Proof

Step	Hyp	Ref	Expression
1		mamudm.e	$⊢ E = R freeLMod (M \times N)$
2		mamudm.b	$⊢ B = {Base}_{E}$
3		mamudm.f	$⊢ F = R freeLMod (N \times P)$
4		mamudm.c	$⊢ C = {Base}_{F}$
5		mamudm.m	$⊢ \underset{˙}{\times} = R maMul ⟨M, N, P⟩$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7		eqid	$⊢ \cdot_{R} = \cdot_{R}$
8		simpl	$⊢ (R \in V \land (M \in Fin \land N \in Fin \land P \in Fin)) \to R \in V$
9		simpr1	$⊢ (R \in V \land (M \in Fin \land N \in Fin \land P \in Fin)) \to M \in Fin$
10		simpr2	$⊢ (R \in V \land (M \in Fin \land N \in Fin \land P \in Fin)) \to N \in Fin$
11		simpr3	$⊢ (R \in V \land (M \in Fin \land N \in Fin \land P \in Fin)) \to P \in Fin$
12	5 6 7 8 9 10 11	mamufval	$⊢ (R \in V \land (M \in Fin \land N \in Fin \land P \in Fin)) \to \underset{˙}{\times} = (x \in ({Base}_{R}^{(M \times N)}), y \in ({Base}_{R}^{(N \times P)}) ⟼ (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} (j y k))))$
13	12	dmeqd	$⊢ (R \in V \land (M \in Fin \land N \in Fin \land P \in Fin)) \to dom \underset{˙}{\times} = dom (x \in ({Base}_{R}^{(M \times N)}), y \in ({Base}_{R}^{(N \times P)}) ⟼ (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} (j y k))))$
14		mpoexga	$⊢ (M \in Fin \land P \in Fin) \to (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} (j y k))) \in V$
15	14	3adant2	$⊢ (M \in Fin \land N \in Fin \land P \in Fin) \to (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} (j y k))) \in V$
16	15	adantl	$⊢ (R \in V \land (M \in Fin \land N \in Fin \land P \in Fin)) \to (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} (j y k))) \in V$
17	16	a1d	$⊢ (R \in V \land (M \in Fin \land N \in Fin \land P \in Fin)) \to ((x \in ({Base}_{R}^{(M \times N)}) \land y \in ({Base}_{R}^{(N \times P)})) \to (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} (j y k))) \in V)$
18	17	ralrimivv	$⊢ (R \in V \land (M \in Fin \land N \in Fin \land P \in Fin)) \to \forall x \in ({Base}_{R}^{(M \times N)}) \forall y \in ({Base}_{R}^{(N \times P)}) (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} (j y k))) \in V$
19		eqid	$⊢ (x \in ({Base}_{R}^{(M \times N)}), y \in ({Base}_{R}^{(N \times P)}) ⟼ (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} (j y k)))) = (x \in ({Base}_{R}^{(M \times N)}), y \in ({Base}_{R}^{(N \times P)}) ⟼ (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} (j y k))))$
20	19	dmmpoga	$⊢ \forall x \in ({Base}_{R}^{(M \times N)}) \forall y \in ({Base}_{R}^{(N \times P)}) (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} (j y k))) \in V \to dom (x \in ({Base}_{R}^{(M \times N)}), y \in ({Base}_{R}^{(N \times P)}) ⟼ (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} (j y k)))) = ({Base}_{R}^{(M \times N)}) \times ({Base}_{R}^{(N \times P)})$
21	18 20	syl	$⊢ (R \in V \land (M \in Fin \land N \in Fin \land P \in Fin)) \to dom (x \in ({Base}_{R}^{(M \times N)}), y \in ({Base}_{R}^{(N \times P)}) ⟼ (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} (j y k)))) = ({Base}_{R}^{(M \times N)}) \times ({Base}_{R}^{(N \times P)})$
22		xpfi	$⊢ (M \in Fin \land N \in Fin) \to M \times N \in Fin$
23	22	3adant3	$⊢ (M \in Fin \land N \in Fin \land P \in Fin) \to M \times N \in Fin$
24	1 6	frlmfibas	$⊢ (R \in V \land M \times N \in Fin) \to {Base}_{R}^{(M \times N)} = {Base}_{E}$
25	23 24	sylan2	$⊢ (R \in V \land (M \in Fin \land N \in Fin \land P \in Fin)) \to {Base}_{R}^{(M \times N)} = {Base}_{E}$
26	25 2	eqtr4di	$⊢ (R \in V \land (M \in Fin \land N \in Fin \land P \in Fin)) \to {Base}_{R}^{(M \times N)} = B$
27		xpfi	$⊢ (N \in Fin \land P \in Fin) \to N \times P \in Fin$
28	27	3adant1	$⊢ (M \in Fin \land N \in Fin \land P \in Fin) \to N \times P \in Fin$
29	3 6	frlmfibas	$⊢ (R \in V \land N \times P \in Fin) \to {Base}_{R}^{(N \times P)} = {Base}_{F}$
30	28 29	sylan2	$⊢ (R \in V \land (M \in Fin \land N \in Fin \land P \in Fin)) \to {Base}_{R}^{(N \times P)} = {Base}_{F}$
31	30 4	eqtr4di	$⊢ (R \in V \land (M \in Fin \land N \in Fin \land P \in Fin)) \to {Base}_{R}^{(N \times P)} = C$
32	26 31	xpeq12d	$⊢ (R \in V \land (M \in Fin \land N \in Fin \land P \in Fin)) \to ({Base}_{R}^{(M \times N)}) \times ({Base}_{R}^{(N \times P)}) = B \times C$
33	13 21 32	3eqtrd	$⊢ (R \in V \land (M \in Fin \land N \in Fin \land P \in Fin)) \to dom \underset{˙}{\times} = B \times C$

Metamath Proof Explorer

Theorem mamudm

Proof