mavmulcl

Description: Multiplication of an NxN matrix with an N-dimensional vector results in an N-dimensional vector. (Contributed by AV, 6-Dec-2018) (Revised by AV, 23-Feb-2019) (Proof shortened by AV, 23-Jul-2019)

	Ref	Expression
Hypotheses	mavmulcl.a	$⊢ A = N Mat R$
	mavmulcl.m	$⊢ \underset{˙}{\times} = R maVecMul ⟨N, N⟩$
	mavmulcl.b	$⊢ B = {Base}_{R}$
	mavmulcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mavmulcl.r	$⊢ φ \to R \in Ring$
	mavmulcl.n	$⊢ φ \to N \in Fin$
	mavmulcl.x	$⊢ φ \to X \in {Base}_{A}$
	mavmulcl.y	$⊢ φ \to Y \in (B^{N})$
Assertion	mavmulcl	$⊢ φ \to X \underset{˙}{\times} Y \in (B^{N})$

Proof

Step	Hyp	Ref	Expression
1		mavmulcl.a	$⊢ A = N Mat R$
2		mavmulcl.m	$⊢ \underset{˙}{\times} = R maVecMul ⟨N, N⟩$
3		mavmulcl.b	$⊢ B = {Base}_{R}$
4		mavmulcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		mavmulcl.r	$⊢ φ \to R \in Ring$
6		mavmulcl.n	$⊢ φ \to N \in Fin$
7		mavmulcl.x	$⊢ φ \to X \in {Base}_{A}$
8		mavmulcl.y	$⊢ φ \to Y \in (B^{N})$
9	1 2 3 4 5 6 7 8	mavmulval	$⊢ φ \to X \underset{˙}{\times} Y = (i \in N ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j)))$
10		ringcmn	$⊢ R \in Ring \to R \in CMnd$
11	5 10	syl	$⊢ φ \to R \in CMnd$
12	11	adantr	$⊢ (φ \land i \in N) \to R \in CMnd$
13	6	adantr	$⊢ (φ \land i \in N) \to N \in Fin$
14	5	ad2antrr	$⊢ ((φ \land i \in N) \land j \in N) \to R \in Ring$
15	1 3	matbas2	$⊢ (N \in Fin \land R \in Ring) \to B^{(N \times N)} = {Base}_{A}$
16	6 5 15	syl2anc	$⊢ φ \to B^{(N \times N)} = {Base}_{A}$
17	7 16	eleqtrrd	$⊢ φ \to X \in (B^{(N \times N)})$
18		elmapi	$⊢ X \in (B^{(N \times N)}) \to X : N \times N ⟶ B$
19	17 18	syl	$⊢ φ \to X : N \times N ⟶ B$
20	19	ad2antrr	$⊢ ((φ \land i \in N) \land j \in N) \to X : N \times N ⟶ B$
21		simpr	$⊢ (φ \land i \in N) \to i \in N$
22	21	adantr	$⊢ ((φ \land i \in N) \land j \in N) \to i \in N$
23		simpr	$⊢ ((φ \land i \in N) \land j \in N) \to j \in N$
24	20 22 23	fovcdmd	$⊢ ((φ \land i \in N) \land j \in N) \to i X j \in B$
25		elmapi	$⊢ Y \in (B^{N}) \to Y : N ⟶ B$
26	8 25	syl	$⊢ φ \to Y : N ⟶ B$
27	26	ad2antrr	$⊢ ((φ \land i \in N) \land j \in N) \to Y : N ⟶ B$
28	27 23	ffvelcdmd	$⊢ ((φ \land i \in N) \land j \in N) \to Y (j) \in B$
29	3 4	ringcl	$⊢ (R \in Ring \land i X j \in B \land Y (j) \in B) \to (i X j) \underset{˙}{\cdot} Y (j) \in B$
30	14 24 28 29	syl3anc	$⊢ ((φ \land i \in N) \land j \in N) \to (i X j) \underset{˙}{\cdot} Y (j) \in B$
31	30	ralrimiva	$⊢ (φ \land i \in N) \to \forall j \in N (i X j) \underset{˙}{\cdot} Y (j) \in B$
32	3 12 13 31	gsummptcl	$⊢ (φ \land i \in N) \to \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j)) \in B$
33	32	ralrimiva	$⊢ φ \to \forall i \in N \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j)) \in B$
34		eqid	$⊢ (i \in N ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j))) = (i \in N ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j)))$
35	34	fmpt	$⊢ \forall i \in N \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j)) \in B \leftrightarrow (i \in N ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j))) : N ⟶ B$
36	3	fvexi	$⊢ B \in V$
37		elmapg	$⊢ (B \in V \land N \in Fin) \to ((i \in N ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j))) \in (B^{N}) \leftrightarrow (i \in N ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j))) : N ⟶ B)$
38	36 6 37	sylancr	$⊢ φ \to ((i \in N ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j))) \in (B^{N}) \leftrightarrow (i \in N ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j))) : N ⟶ B)$
39	35 38	bitr4id	$⊢ φ \to (\forall i \in N \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j)) \in B \leftrightarrow (i \in N ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j))) \in (B^{N}))$
40	33 39	mpbid	$⊢ φ \to (i \in N ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j))) \in (B^{N})$
41	9 40	eqeltrd	$⊢ φ \to X \underset{˙}{\times} Y \in (B^{N})$

Metamath Proof Explorer

Theorem mavmulcl

Proof