1mavmul

Description: Multiplication of the identity NxN matrix with an N-dimensional vector results in the vector itself. (Contributed by AV, 9-Feb-2019) (Revised by AV, 23-Feb-2019)

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

Proof

Step	Hyp	Ref	Expression
1		1mavmul.a	$⊢ A = N Mat R$
2		1mavmul.b	$⊢ B = {Base}_{R}$
3		1mavmul.t	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨N, N⟩$
4		1mavmul.r	$⊢ φ \to R \in Ring$
5		1mavmul.n	$⊢ φ \to N \in Fin$
6		1mavmul.y	$⊢ φ \to Y \in (B^{N})$
7		eqid	$⊢ \cdot_{R} = \cdot_{R}$
8		eqid	$⊢ {Base}_{A} = {Base}_{A}$
9	1	fveq2i	$⊢ 1_{A} = 1_{(N Mat R)}$
10	1 8 9	mat1bas	$⊢ (R \in Ring \land N \in Fin) \to 1_{A} \in {Base}_{A}$
11	4 5 10	syl2anc	$⊢ φ \to 1_{A} \in {Base}_{A}$
12	1 3 2 7 4 5 11 6	mavmulval	$⊢ φ \to 1_{A} \underset{˙}{\cdot} Y = (i \in N ⟼ \underset{j \in N}{\sum_{R}} ((i 1_{A} j) \cdot_{R} Y (j)))$
13		eqid	$⊢ 1_{R} = 1_{R}$
14		eqid	$⊢ 0_{R} = 0_{R}$
15	1 13 14	mat1	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} = (x \in N, y \in N ⟼ if (x = y, 1_{R}, 0_{R}))$
16	5 4 15	syl2anc	$⊢ φ \to 1_{A} = (x \in N, y \in N ⟼ if (x = y, 1_{R}, 0_{R}))$
17	16	oveqdr	$⊢ (φ \land i \in N) \to i 1_{A} j = i (x \in N, y \in N ⟼ if (x = y, 1_{R}, 0_{R})) j$
18	17	oveq1d	$⊢ (φ \land i \in N) \to (i 1_{A} j) \cdot_{R} Y (j) = (i (x \in N, y \in N ⟼ if (x = y, 1_{R}, 0_{R})) j) \cdot_{R} Y (j)$
19	18	mpteq2dv	$⊢ (φ \land i \in N) \to (j \in N ⟼ (i 1_{A} j) \cdot_{R} Y (j)) = (j \in N ⟼ (i (x \in N, y \in N ⟼ if (x = y, 1_{R}, 0_{R})) j) \cdot_{R} Y (j))$
20	19	oveq2d	$⊢ (φ \land i \in N) \to \underset{j \in N}{\sum_{R}} ((i 1_{A} j) \cdot_{R} Y (j)) = \underset{j \in N}{\sum_{R}} ((i (x \in N, y \in N ⟼ if (x = y, 1_{R}, 0_{R})) j) \cdot_{R} Y (j))$
21		eqidd	$⊢ ((φ \land i \in N) \land j \in N) \to (x \in N, y \in N ⟼ if (x = y, 1_{R}, 0_{R})) = (x \in N, y \in N ⟼ if (x = y, 1_{R}, 0_{R}))$
22		eqeq12	$⊢ (x = i \land y = j) \to (x = y \leftrightarrow i = j)$
23	22	ifbid	$⊢ (x = i \land y = j) \to if (x = y, 1_{R}, 0_{R}) = if (i = j, 1_{R}, 0_{R})$
24	23	adantl	$⊢ (((φ \land i \in N) \land j \in N) \land (x = i \land y = j)) \to if (x = y, 1_{R}, 0_{R}) = if (i = j, 1_{R}, 0_{R})$
25		simpr	$⊢ (φ \land i \in N) \to i \in N$
26	25	adantr	$⊢ ((φ \land i \in N) \land j \in N) \to i \in N$
27		simpr	$⊢ ((φ \land i \in N) \land j \in N) \to j \in N$
28		fvexd	$⊢ ((φ \land i \in N) \land j \in N) \to 1_{R} \in V$
29		fvexd	$⊢ ((φ \land i \in N) \land j \in N) \to 0_{R} \in V$
30	28 29	ifcld	$⊢ ((φ \land i \in N) \land j \in N) \to if (i = j, 1_{R}, 0_{R}) \in V$
31	21 24 26 27 30	ovmpod	$⊢ ((φ \land i \in N) \land j \in N) \to i (x \in N, y \in N ⟼ if (x = y, 1_{R}, 0_{R})) j = if (i = j, 1_{R}, 0_{R})$
32	31	oveq1d	$⊢ ((φ \land i \in N) \land j \in N) \to (i (x \in N, y \in N ⟼ if (x = y, 1_{R}, 0_{R})) j) \cdot_{R} Y (j) = if (i = j, 1_{R}, 0_{R}) \cdot_{R} Y (j)$
33		iftrue	$⊢ i = j \to if (i = j, 1_{R}, 0_{R}) = 1_{R}$
34	33	adantr	$⊢ (i = j \land ((φ \land i \in N) \land j \in N)) \to if (i = j, 1_{R}, 0_{R}) = 1_{R}$
35	34	oveq1d	$⊢ (i = j \land ((φ \land i \in N) \land j \in N)) \to if (i = j, 1_{R}, 0_{R}) \cdot_{R} Y (j) = 1_{R} \cdot_{R} Y (j)$
36	4	adantr	$⊢ (φ \land i \in N) \to R \in Ring$
37	36	adantr	$⊢ ((φ \land i \in N) \land j \in N) \to R \in Ring$
38	2	fvexi	$⊢ B \in V$
39	38	a1i	$⊢ φ \to B \in V$
40	39 5	elmapd	$⊢ φ \to (Y \in (B^{N}) \leftrightarrow Y : N ⟶ B)$
41		ffvelcdm	$⊢ (Y : N ⟶ B \land j \in N) \to Y (j) \in B$
42	41	ex	$⊢ Y : N ⟶ B \to (j \in N \to Y (j) \in B)$
43	40 42	syl6bi	$⊢ φ \to (Y \in (B^{N}) \to (j \in N \to Y (j) \in B))$
44	6 43	mpd	$⊢ φ \to (j \in N \to Y (j) \in B)$
45	44	adantr	$⊢ (φ \land i \in N) \to (j \in N \to Y (j) \in B)$
46	45	imp	$⊢ ((φ \land i \in N) \land j \in N) \to Y (j) \in B$
47	2 7 13	ringlidm	$⊢ (R \in Ring \land Y (j) \in B) \to 1_{R} \cdot_{R} Y (j) = Y (j)$
48	37 46 47	syl2anc	$⊢ ((φ \land i \in N) \land j \in N) \to 1_{R} \cdot_{R} Y (j) = Y (j)$
49	48	adantl	$⊢ (i = j \land ((φ \land i \in N) \land j \in N)) \to 1_{R} \cdot_{R} Y (j) = Y (j)$
50		fveq2	$⊢ j = i \to Y (j) = Y (i)$
51	50	equcoms	$⊢ i = j \to Y (j) = Y (i)$
52	51	adantr	$⊢ (i = j \land ((φ \land i \in N) \land j \in N)) \to Y (j) = Y (i)$
53	35 49 52	3eqtrd	$⊢ (i = j \land ((φ \land i \in N) \land j \in N)) \to if (i = j, 1_{R}, 0_{R}) \cdot_{R} Y (j) = Y (i)$
54		iftrue	$⊢ j = i \to if (j = i, Y (i), 0_{R}) = Y (i)$
55	54	equcoms	$⊢ i = j \to if (j = i, Y (i), 0_{R}) = Y (i)$
56	55	adantr	$⊢ (i = j \land ((φ \land i \in N) \land j \in N)) \to if (j = i, Y (i), 0_{R}) = Y (i)$
57	53 56	eqtr4d	$⊢ (i = j \land ((φ \land i \in N) \land j \in N)) \to if (i = j, 1_{R}, 0_{R}) \cdot_{R} Y (j) = if (j = i, Y (i), 0_{R})$
58		iffalse	$⊢ \neg i = j \to if (i = j, 1_{R}, 0_{R}) = 0_{R}$
59	58	oveq1d	$⊢ \neg i = j \to if (i = j, 1_{R}, 0_{R}) \cdot_{R} Y (j) = 0_{R} \cdot_{R} Y (j)$
60	59	adantr	$⊢ (\neg i = j \land ((φ \land i \in N) \land j \in N)) \to if (i = j, 1_{R}, 0_{R}) \cdot_{R} Y (j) = 0_{R} \cdot_{R} Y (j)$
61	2 7 14	ringlz	$⊢ (R \in Ring \land Y (j) \in B) \to 0_{R} \cdot_{R} Y (j) = 0_{R}$
62	37 46 61	syl2anc	$⊢ ((φ \land i \in N) \land j \in N) \to 0_{R} \cdot_{R} Y (j) = 0_{R}$
63	62	adantl	$⊢ (\neg i = j \land ((φ \land i \in N) \land j \in N)) \to 0_{R} \cdot_{R} Y (j) = 0_{R}$
64		eqcom	$⊢ i = j \leftrightarrow j = i$
65		iffalse	$⊢ \neg j = i \to if (j = i, Y (i), 0_{R}) = 0_{R}$
66	64 65	sylnbi	$⊢ \neg i = j \to if (j = i, Y (i), 0_{R}) = 0_{R}$
67	66	eqcomd	$⊢ \neg i = j \to 0_{R} = if (j = i, Y (i), 0_{R})$
68	67	adantr	$⊢ (\neg i = j \land ((φ \land i \in N) \land j \in N)) \to 0_{R} = if (j = i, Y (i), 0_{R})$
69	60 63 68	3eqtrd	$⊢ (\neg i = j \land ((φ \land i \in N) \land j \in N)) \to if (i = j, 1_{R}, 0_{R}) \cdot_{R} Y (j) = if (j = i, Y (i), 0_{R})$
70	57 69	pm2.61ian	$⊢ ((φ \land i \in N) \land j \in N) \to if (i = j, 1_{R}, 0_{R}) \cdot_{R} Y (j) = if (j = i, Y (i), 0_{R})$
71	32 70	eqtrd	$⊢ ((φ \land i \in N) \land j \in N) \to (i (x \in N, y \in N ⟼ if (x = y, 1_{R}, 0_{R})) j) \cdot_{R} Y (j) = if (j = i, Y (i), 0_{R})$
72	71	mpteq2dva	$⊢ (φ \land i \in N) \to (j \in N ⟼ (i (x \in N, y \in N ⟼ if (x = y, 1_{R}, 0_{R})) j) \cdot_{R} Y (j)) = (j \in N ⟼ if (j = i, Y (i), 0_{R}))$
73	72	oveq2d	$⊢ (φ \land i \in N) \to \underset{j \in N}{\sum_{R}} ((i (x \in N, y \in N ⟼ if (x = y, 1_{R}, 0_{R})) j) \cdot_{R} Y (j)) = \underset{j \in N}{\sum_{R}} if (j = i, Y (i), 0_{R})$
74		ringmnd	$⊢ R \in Ring \to R \in Mnd$
75	4 74	syl	$⊢ φ \to R \in Mnd$
76	75	adantr	$⊢ (φ \land i \in N) \to R \in Mnd$
77	5	adantr	$⊢ (φ \land i \in N) \to N \in Fin$
78		eqid	$⊢ (j \in N ⟼ if (j = i, Y (i), 0_{R})) = (j \in N ⟼ if (j = i, Y (i), 0_{R}))$
79		ffvelcdm	$⊢ (Y : N ⟶ B \land i \in N) \to Y (i) \in B$
80	79 2	eleqtrdi	$⊢ (Y : N ⟶ B \land i \in N) \to Y (i) \in {Base}_{R}$
81	80	ex	$⊢ Y : N ⟶ B \to (i \in N \to Y (i) \in {Base}_{R})$
82	40 81	syl6bi	$⊢ φ \to (Y \in (B^{N}) \to (i \in N \to Y (i) \in {Base}_{R}))$
83	6 82	mpd	$⊢ φ \to (i \in N \to Y (i) \in {Base}_{R})$
84	83	imp	$⊢ (φ \land i \in N) \to Y (i) \in {Base}_{R}$
85	14 76 77 25 78 84	gsummptif1n0	$⊢ (φ \land i \in N) \to \underset{j \in N}{\sum_{R}} if (j = i, Y (i), 0_{R}) = Y (i)$
86	20 73 85	3eqtrd	$⊢ (φ \land i \in N) \to \underset{j \in N}{\sum_{R}} ((i 1_{A} j) \cdot_{R} Y (j)) = Y (i)$
87	86	mpteq2dva	$⊢ φ \to (i \in N ⟼ \underset{j \in N}{\sum_{R}} ((i 1_{A} j) \cdot_{R} Y (j))) = (i \in N ⟼ Y (i))$
88		ffn	$⊢ Y : N ⟶ B \to Y Fn N$
89	40 88	syl6bi	$⊢ φ \to (Y \in (B^{N}) \to Y Fn N)$
90	6 89	mpd	$⊢ φ \to Y Fn N$
91		eqcom	$⊢ (i \in N ⟼ Y (i)) = Y \leftrightarrow Y = (i \in N ⟼ Y (i))$
92		dffn5	$⊢ Y Fn N \leftrightarrow Y = (i \in N ⟼ Y (i))$
93	91 92	bitr4i	$⊢ (i \in N ⟼ Y (i)) = Y \leftrightarrow Y Fn N$
94	90 93	sylibr	$⊢ φ \to (i \in N ⟼ Y (i)) = Y$
95	12 87 94	3eqtrd	$⊢ φ \to 1_{A} \underset{˙}{\cdot} Y = Y$

Metamath Proof Explorer

Theorem 1mavmul

Proof