mavmuldm

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

	Ref	Expression
Hypotheses	mavmuldm.b	$⊢ B = {Base}_{R}$
	mavmuldm.c	$⊢ C = B^{(M \times N)}$
	mavmuldm.d	$⊢ D = B^{N}$
	mavmuldm.t	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨M, N⟩$
Assertion	mavmuldm	$⊢ (R \in V \land M \in Fin \land N \in Fin) \to dom \underset{˙}{\cdot} = C \times D$

Proof

Step	Hyp	Ref	Expression
1		mavmuldm.b	$⊢ B = {Base}_{R}$
2		mavmuldm.c	$⊢ C = B^{(M \times N)}$
3		mavmuldm.d	$⊢ D = B^{N}$
4		mavmuldm.t	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨M, N⟩$
5		eqid	$⊢ \cdot_{R} = \cdot_{R}$
6		simp1	$⊢ (R \in V \land M \in Fin \land N \in Fin) \to R \in V$
7		simp2	$⊢ (R \in V \land M \in Fin \land N \in Fin) \to M \in Fin$
8		simp3	$⊢ (R \in V \land M \in Fin \land N \in Fin) \to N \in Fin$
9	4 1 5 6 7 8	mvmulfval	$⊢ (R \in V \land M \in Fin \land N \in Fin) \to \underset{˙}{\cdot} = (x \in (B^{(M \times N)}), y \in (B^{N}) ⟼ (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} y (j))))$
10	9	dmeqd	$⊢ (R \in V \land M \in Fin \land N \in Fin) \to dom \underset{˙}{\cdot} = dom (x \in (B^{(M \times N)}), y \in (B^{N}) ⟼ (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} y (j))))$
11		mptexg	$⊢ M \in Fin \to (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} y (j))) \in V$
12	11	3ad2ant2	$⊢ (R \in V \land M \in Fin \land N \in Fin) \to (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} y (j))) \in V$
13	12	a1d	$⊢ (R \in V \land M \in Fin \land N \in Fin) \to ((x \in (B^{(M \times N)}) \land y \in (B^{N})) \to (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} y (j))) \in V)$
14	13	ralrimivv	$⊢ (R \in V \land M \in Fin \land N \in Fin) \to \forall x \in (B^{(M \times N)}) \forall y \in (B^{N}) (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} y (j))) \in V$
15		eqid	$⊢ (x \in (B^{(M \times N)}), y \in (B^{N}) ⟼ (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} y (j)))) = (x \in (B^{(M \times N)}), y \in (B^{N}) ⟼ (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} y (j))))$
16	15	dmmpoga	$⊢ \forall x \in (B^{(M \times N)}) \forall y \in (B^{N}) (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} y (j))) \in V \to dom (x \in (B^{(M \times N)}), y \in (B^{N}) ⟼ (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} y (j)))) = (B^{(M \times N)}) \times (B^{N})$
17	14 16	syl	$⊢ (R \in V \land M \in Fin \land N \in Fin) \to dom (x \in (B^{(M \times N)}), y \in (B^{N}) ⟼ (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \cdot_{R} y (j)))) = (B^{(M \times N)}) \times (B^{N})$
18	2	eqcomi	$⊢ B^{(M \times N)} = C$
19	18	a1i	$⊢ (R \in V \land M \in Fin \land N \in Fin) \to B^{(M \times N)} = C$
20	3	a1i	$⊢ (R \in V \land M \in Fin \land N \in Fin) \to D = B^{N}$
21	20	eqcomd	$⊢ (R \in V \land M \in Fin \land N \in Fin) \to B^{N} = D$
22	19 21	xpeq12d	$⊢ (R \in V \land M \in Fin \land N \in Fin) \to (B^{(M \times N)}) \times (B^{N}) = C \times D$
23	10 17 22	3eqtrd	$⊢ (R \in V \land M \in Fin \land N \in Fin) \to dom \underset{˙}{\cdot} = C \times D$

Metamath Proof Explorer

Theorem mavmuldm

Proof