1marepvsma1

Description: The submatrix of the identity matrix with the ith column replaced by the vector obtained by removing the ith row and the ith column is an identity matrix. (Contributed by AV, 14-Feb-2019) (Revised by AV, 27-Feb-2019)

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

Proof

Step	Hyp	Ref	Expression
1		1marepvsma1.v	$⊢ V = {Base}_{R}^{N}$
2		1marepvsma1.1	$⊢ \underset{˙}{1} = 1_{(N Mat R)}$
3		1marepvsma1.x	$⊢ X = (\underset{˙}{1} (N matRepV R) Z) (I)$
4	3	oveqi	$⊢ i X j = i (\underset{˙}{1} (N matRepV R) Z) (I) j$
5	4	a1i	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in (N ∖ \{I\}) \land j \in (N ∖ \{I\})) \to i X j = i (\underset{˙}{1} (N matRepV R) Z) (I) j$
6		eqid	$⊢ N Mat R = N Mat R$
7		eqid	$⊢ {Base}_{(N Mat R)} = {Base}_{(N Mat R)}$
8	6 7 2	mat1bas	$⊢ (R \in Ring \land N \in Fin) \to \underset{˙}{1} \in {Base}_{(N Mat R)}$
9	8	adantr	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to \underset{˙}{1} \in {Base}_{(N Mat R)}$
10		simprr	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to Z \in V$
11		simprl	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to I \in N$
12	9 10 11	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)$
13	12	3ad2ant1	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in (N ∖ \{I\}) \land j \in (N ∖ \{I\})) \to (\underset{˙}{1} \in {Base}_{(N Mat R)} \land Z \in V \land I \in N)$
14		eldifi	$⊢ i \in (N ∖ \{I\}) \to i \in N$
15		eldifi	$⊢ j \in (N ∖ \{I\}) \to j \in N$
16	14 15	anim12i	$⊢ (i \in (N ∖ \{I\}) \land j \in (N ∖ \{I\})) \to (i \in N \land j \in N)$
17	16	3adant1	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in (N ∖ \{I\}) \land j \in (N ∖ \{I\})) \to (i \in N \land j \in N)$
18		eqid	$⊢ N matRepV R = N matRepV R$
19	6 7 18 1	marepveval	$⊢ ((\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 (\underset{˙}{1} (N matRepV R) Z) (I) j = if (j = I, Z (i), i \underset{˙}{1} j)$
20	13 17 19	syl2anc	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in (N ∖ \{I\}) \land j \in (N ∖ \{I\})) \to i (\underset{˙}{1} (N matRepV R) Z) (I) j = if (j = I, Z (i), i \underset{˙}{1} j)$
21		eldifsni	$⊢ j \in (N ∖ \{I\}) \to j \neq I$
22	21	neneqd	$⊢ j \in (N ∖ \{I\}) \to \neg j = I$
23	22	3ad2ant3	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in (N ∖ \{I\}) \land j \in (N ∖ \{I\})) \to \neg j = I$
24	23	iffalsed	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in (N ∖ \{I\}) \land j \in (N ∖ \{I\})) \to if (j = I, Z (i), i \underset{˙}{1} j) = i \underset{˙}{1} j$
25		eqid	$⊢ 1_{R} = 1_{R}$
26		eqid	$⊢ 0_{R} = 0_{R}$
27		simp1lr	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in (N ∖ \{I\}) \land j \in (N ∖ \{I\})) \to N \in Fin$
28		simp1ll	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in (N ∖ \{I\}) \land j \in (N ∖ \{I\})) \to R \in Ring$
29	14	3ad2ant2	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in (N ∖ \{I\}) \land j \in (N ∖ \{I\})) \to i \in N$
30	15	3ad2ant3	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in (N ∖ \{I\}) \land j \in (N ∖ \{I\})) \to j \in N$
31	6 25 26 27 28 29 30 2	mat1ov	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in (N ∖ \{I\}) \land j \in (N ∖ \{I\})) \to i \underset{˙}{1} j = if (i = j, 1_{R}, 0_{R})$
32	24 31	eqtrd	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in (N ∖ \{I\}) \land j \in (N ∖ \{I\})) \to if (j = I, Z (i), i \underset{˙}{1} j) = if (i = j, 1_{R}, 0_{R})$
33	5 20 32	3eqtrd	$⊢ (((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \land i \in (N ∖ \{I\}) \land j \in (N ∖ \{I\})) \to i X j = if (i = j, 1_{R}, 0_{R})$
34	33	mpoeq3dva	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to (i \in (N ∖ \{I\}), j \in (N ∖ \{I\}) ⟼ i X j) = (i \in (N ∖ \{I\}), j \in (N ∖ \{I\}) ⟼ if (i = j, 1_{R}, 0_{R}))$
35	6 7 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)}$
36	35	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)}$
37	3 36	eqeltrid	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to X \in {Base}_{(N Mat R)}$
38		eqid	$⊢ N subMat R = N subMat R$
39	6 38 7	submaval	$⊢ (X \in {Base}_{(N Mat R)} \land I \in N \land I \in N) \to I (N subMat R) (X) I = (i \in (N ∖ \{I\}), j \in (N ∖ \{I\}) ⟼ i X j)$
40	37 11 11 39	syl3anc	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to I (N subMat R) (X) I = (i \in (N ∖ \{I\}), j \in (N ∖ \{I\}) ⟼ i X j)$
41		diffi	$⊢ N \in Fin \to N ∖ \{I\} \in Fin$
42	41	anim2i	$⊢ (R \in Ring \land N \in Fin) \to (R \in Ring \land N ∖ \{I\} \in Fin)$
43	42	ancomd	$⊢ (R \in Ring \land N \in Fin) \to (N ∖ \{I\} \in Fin \land R \in Ring)$
44	43	adantr	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to (N ∖ \{I\} \in Fin \land R \in Ring)$
45		eqid	$⊢ (N ∖ \{I\}) Mat R = (N ∖ \{I\}) Mat R$
46	45 25 26	mat1	$⊢ (N ∖ \{I\} \in Fin \land R \in Ring) \to 1_{((N ∖ \{I\}) Mat R)} = (i \in (N ∖ \{I\}), j \in (N ∖ \{I\}) ⟼ if (i = j, 1_{R}, 0_{R}))$
47	44 46	syl	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to 1_{((N ∖ \{I\}) Mat R)} = (i \in (N ∖ \{I\}), j \in (N ∖ \{I\}) ⟼ if (i = j, 1_{R}, 0_{R}))$
48	34 40 47	3eqtr4d	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to I (N subMat R) (X) I = 1_{((N ∖ \{I\}) Mat R)}$

Metamath Proof Explorer

Theorem 1marepvsma1

Proof