1marepvmarrepid

Description: Replacing the ith row by 0's and the ith component of a (column) vector at the diagonal position for the identity matrix with the ith column replaced by the vector results in the matrix itself. (Contributed by AV, 14-Feb-2019) (Revised by AV, 27-Feb-2019)

	Ref	Expression
Hypotheses	marepvmarrep1.v	$⊢ V = {Base}_{R}^{N}$
	marepvmarrep1.o	$⊢ \underset{˙}{1} = 1_{(N Mat R)}$
	marepvmarrep1.x	$⊢ X = (\underset{˙}{1} (N matRepV R) Z) (I)$
Assertion	1marepvmarrepid	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to I (X (N matRRep R) Z (I)) I = X$

Proof

Step	Hyp	Ref	Expression
1		marepvmarrep1.v	$⊢ V = {Base}_{R}^{N}$
2		marepvmarrep1.o	$⊢ \underset{˙}{1} = 1_{(N Mat R)}$
3		marepvmarrep1.x	$⊢ X = (\underset{˙}{1} (N matRepV R) Z) (I)$
4		eqid	$⊢ N Mat R = N Mat R$
5		eqid	$⊢ {Base}_{(N Mat R)} = {Base}_{(N Mat R)}$
6	4 5 1 2	ma1repvcl	$⊢ ((R \in Ring \land N \in Fin) \land (Z \in V \land I \in N)) \to (\underset{˙}{1} (N matRepV R) Z) (I) \in {Base}_{(N Mat R)}$
7	6	ancom2s	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to (\underset{˙}{1} (N matRepV R) Z) (I) \in {Base}_{(N Mat R)}$
8	3 7	eqeltrid	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to X \in {Base}_{(N Mat R)}$
9		elmapi	$⊢ Z \in ({Base}_{R}^{N}) \to Z : N ⟶ {Base}_{R}$
10		ffvelcdm	$⊢ (Z : N ⟶ {Base}_{R} \land I \in N) \to Z (I) \in {Base}_{R}$
11	10	ex	$⊢ Z : N ⟶ {Base}_{R} \to (I \in N \to Z (I) \in {Base}_{R})$
12	9 11	syl	$⊢ Z \in ({Base}_{R}^{N}) \to (I \in N \to Z (I) \in {Base}_{R})$
13	12 1	eleq2s	$⊢ Z \in V \to (I \in N \to Z (I) \in {Base}_{R})$
14	13	impcom	$⊢ (I \in N \land Z \in V) \to Z (I) \in {Base}_{R}$
15	14	adantl	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to Z (I) \in {Base}_{R}$
16		simpl	$⊢ (I \in N \land Z \in V) \to I \in N$
17	16	adantl	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to I \in N$
18		eqid	$⊢ N matRRep R = N matRRep R$
19		eqid	$⊢ 0_{R} = 0_{R}$
20	4 5 18 19	marrepval	$⊢ ((X \in {Base}_{(N Mat R)} \land Z (I) \in {Base}_{R}) \land (I \in N \land I \in N)) \to I (X (N matRRep R) Z (I)) I = (i \in N, j \in N ⟼ if (i = I, if (j = I, Z (I), 0_{R}), i X j))$
21	8 15 17 17 20	syl22anc	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to I (X (N matRRep R) Z (I)) I = (i \in N, j \in N ⟼ if (i = I, if (j = I, Z (I), 0_{R}), i X j))$
22		iftrue	$⊢ i = I \to if (i = I, if (j = I, Z (I), 0_{R}), i X j) = if (j = I, Z (I), 0_{R})$
23	22	adantr	$⊢ (i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N)) \to if (i = I, if (j = I, Z (I), 0_{R}), i X j) = if (j = I, Z (I), 0_{R})$
24		iftrue	$⊢ j = I \to if (j = I, Z (I), 0_{R}) = Z (I)$
25	24	adantr	$⊢ (j = I \land (i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N))) \to if (j = I, Z (I), 0_{R}) = Z (I)$
26		iftrue	$⊢ j = I \to if (j = I, Z (i), i \underset{˙}{1} j) = Z (i)$
27		fveq2	$⊢ i = I \to Z (i) = Z (I)$
28	27	adantr	$⊢ (i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N)) \to Z (i) = Z (I)$
29	26 28	sylan9eq	$⊢ (j = I \land (i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N))) \to if (j = I, Z (i), i \underset{˙}{1} j) = Z (I)$
30	25 29	eqtr4d	$⊢ (j = I \land (i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N))) \to if (j = I, Z (I), 0_{R}) = if (j = I, Z (i), i \underset{˙}{1} j)$
31		eqid	$⊢ 1_{R} = 1_{R}$
32		simpr	$⊢ (R \in Ring \land N \in Fin) \to N \in Fin$
33	32	adantr	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to N \in Fin$
34	33	3ad2ant1	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N) \to N \in Fin$
35		simpl	$⊢ (R \in Ring \land N \in Fin) \to R \in Ring$
36	35	adantr	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to R \in Ring$
37	36	3ad2ant1	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N) \to R \in Ring$
38		simp2	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N) \to i \in N$
39		simp3	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N) \to j \in N$
40	4 31 19 34 37 38 39 2	mat1ov	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N) \to i \underset{˙}{1} j = if (i = j, 1_{R}, 0_{R})$
41	40	adantl	$⊢ (i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N)) \to i \underset{˙}{1} j = if (i = j, 1_{R}, 0_{R})$
42	41	adantl	$⊢ (\neg j = I \land (i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N))) \to i \underset{˙}{1} j = if (i = j, 1_{R}, 0_{R})$
43		eqtr2	$⊢ (i = I \land i = j) \to I = j$
44	43	eqcomd	$⊢ (i = I \land i = j) \to j = I$
45	44	ex	$⊢ i = I \to (i = j \to j = I)$
46	45	con3d	$⊢ i = I \to (\neg j = I \to \neg i = j)$
47	46	adantr	$⊢ (i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N)) \to (\neg j = I \to \neg i = j)$
48	47	impcom	$⊢ (\neg j = I \land (i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N))) \to \neg i = j$
49		iffalse	$⊢ \neg i = j \to if (i = j, 1_{R}, 0_{R}) = 0_{R}$
50	48 49	syl	$⊢ (\neg j = I \land (i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N))) \to if (i = j, 1_{R}, 0_{R}) = 0_{R}$
51	42 50	eqtrd	$⊢ (\neg j = I \land (i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N))) \to i \underset{˙}{1} j = 0_{R}$
52		iffalse	$⊢ \neg j = I \to if (j = I, Z (i), i \underset{˙}{1} j) = i \underset{˙}{1} j$
53	52	adantr	$⊢ (\neg j = I \land (i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N))) \to if (j = I, Z (i), i \underset{˙}{1} j) = i \underset{˙}{1} j$
54		iffalse	$⊢ \neg j = I \to if (j = I, Z (I), 0_{R}) = 0_{R}$
55	54	adantr	$⊢ (\neg j = I \land (i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N))) \to if (j = I, Z (I), 0_{R}) = 0_{R}$
56	51 53 55	3eqtr4rd	$⊢ (\neg j = I \land (i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N))) \to if (j = I, Z (I), 0_{R}) = if (j = I, Z (i), i \underset{˙}{1} j)$
57	30 56	pm2.61ian	$⊢ (i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N)) \to if (j = I, Z (I), 0_{R}) = if (j = I, Z (i), i \underset{˙}{1} j)$
58	23 57	eqtrd	$⊢ (i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N)) \to if (i = I, if (j = I, Z (I), 0_{R}), i X j) = if (j = I, Z (i), i \underset{˙}{1} j)$
59		iffalse	$⊢ \neg i = I \to if (i = I, if (j = I, Z (I), 0_{R}), i X j) = i X j$
60	59	adantr	$⊢ (\neg i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N)) \to if (i = I, if (j = I, Z (I), 0_{R}), i X j) = i X j$
61	4 5 2	mat1bas	$⊢ (R \in Ring \land N \in Fin) \to \underset{˙}{1} \in {Base}_{(N Mat R)}$
62	61	adantr	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to \underset{˙}{1} \in {Base}_{(N Mat R)}$
63		simpr	$⊢ (I \in N \land Z \in V) \to Z \in V$
64	63	adantl	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to Z \in V$
65	62 64 17	3jca	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to (\underset{˙}{1} \in {Base}_{(N Mat R)} \land Z \in V \land I \in N)$
66	65	3ad2ant1	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N) \to (\underset{˙}{1} \in {Base}_{(N Mat R)} \land Z \in V \land I \in N)$
67		3simpc	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N) \to (i \in N \land j \in N)$
68	37 66 67	3jca	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N) \to (R \in Ring \land (\underset{˙}{1} \in {Base}_{(N Mat R)} \land Z \in V \land I \in N) \land (i \in N \land j \in N))$
69	68	adantl	$⊢ (\neg i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N)) \to (R \in Ring \land (\underset{˙}{1} \in {Base}_{(N Mat R)} \land Z \in V \land I \in N) \land (i \in N \land j \in N))$
70	4 5 1 2 19 3	ma1repveval	$⊢ (R \in Ring \land (\underset{˙}{1} \in {Base}_{(N Mat R)} \land Z \in V \land I \in N) \land (i \in N \land j \in N)) \to i X j = if (j = I, Z (i), if (j = i, 1_{R}, 0_{R}))$
71	69 70	syl	$⊢ (\neg i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N)) \to i X j = if (j = I, Z (i), if (j = i, 1_{R}, 0_{R}))$
72	34	ad2antlr	$⊢ ((\neg i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N)) \land \neg j = I) \to N \in Fin$
73	37	ad2antlr	$⊢ ((\neg i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N)) \land \neg j = I) \to R \in Ring$
74	38	ad2antlr	$⊢ ((\neg i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N)) \land \neg j = I) \to i \in N$
75	39	ad2antlr	$⊢ ((\neg i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N)) \land \neg j = I) \to j \in N$
76	4 31 19 72 73 74 75 2	mat1ov	$⊢ ((\neg i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N)) \land \neg j = I) \to i \underset{˙}{1} j = if (i = j, 1_{R}, 0_{R})$
77		equcom	$⊢ i = j \leftrightarrow j = i$
78	77	a1i	$⊢ ((\neg i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N)) \land \neg j = I) \to (i = j \leftrightarrow j = i)$
79	78	ifbid	$⊢ ((\neg i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N)) \land \neg j = I) \to if (i = j, 1_{R}, 0_{R}) = if (j = i, 1_{R}, 0_{R})$
80	76 79	eqtr2d	$⊢ ((\neg i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N)) \land \neg j = I) \to if (j = i, 1_{R}, 0_{R}) = i \underset{˙}{1} j$
81	80	ifeq2da	$⊢ (\neg i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N)) \to if (j = I, Z (i), if (j = i, 1_{R}, 0_{R})) = if (j = I, Z (i), i \underset{˙}{1} j)$
82	60 71 81	3eqtrd	$⊢ (\neg i = I \land (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N)) \to if (i = I, if (j = I, Z (I), 0_{R}), i X j) = if (j = I, Z (i), i \underset{˙}{1} j)$
83	58 82	pm2.61ian	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in N \land j \in N) \to if (i = I, if (j = I, Z (I), 0_{R}), i X j) = if (j = I, Z (i), i \underset{˙}{1} j)$
84	83	mpoeq3dva	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to (i \in N, j \in N ⟼ if (i = I, if (j = I, Z (I), 0_{R}), i X j)) = (i \in N, j \in N ⟼ if (j = I, Z (i), i \underset{˙}{1} j))$
85		eqid	$⊢ N matRepV R = N matRepV R$
86	4 5 85 1	marepvval	$⊢ (\underset{˙}{1} \in {Base}_{(N Mat R)} \land Z \in V \land I \in N) \to (\underset{˙}{1} (N matRepV R) Z) (I) = (i \in N, j \in N ⟼ if (j = I, Z (i), i \underset{˙}{1} j))$
87	65 86	syl	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to (\underset{˙}{1} (N matRepV R) Z) (I) = (i \in N, j \in N ⟼ if (j = I, Z (i), i \underset{˙}{1} j))$
88	3 87	eqtr2id	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to (i \in N, j \in N ⟼ if (j = I, Z (i), i \underset{˙}{1} j)) = X$
89	21 84 88	3eqtrd	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to I (X (N matRRep R) Z (I)) I = X$

Metamath Proof Explorer

Theorem 1marepvmarrepid

Proof