1smat1

Description: The submatrix of the identity matrix obtained by removing the ith row and the ith column is an identity matrix. Cf. 1marepvsma1 . (Contributed by Thierry Arnoux, 19-Aug-2020)

	Ref	Expression
Hypotheses	1smat1.1	$⊢ \underset{˙}{1} = 1_{((1 \dots N) Mat R)}$
	1smat1.r	$⊢ φ \to R \in Ring$
	1smat1.n	$⊢ φ \to N \in ℕ$
	1smat1.i	$⊢ φ \to I \in (1 \dots N)$
Assertion	1smat1	$⊢ φ \to I {subMat}_{1} (\underset{˙}{1}) I = 1_{((1 \dots N - 1) Mat R)}$

Proof

Step	Hyp	Ref	Expression
1		1smat1.1	$⊢ \underset{˙}{1} = 1_{((1 \dots N) Mat R)}$
2		1smat1.r	$⊢ φ \to R \in Ring$
3		1smat1.n	$⊢ φ \to N \in ℕ$
4		1smat1.i	$⊢ φ \to I \in (1 \dots N)$
5		eqid	$⊢ I {subMat}_{1} (\underset{˙}{1}) I = I {subMat}_{1} (\underset{˙}{1}) I$
6	3	adantr	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to N \in ℕ$
7	4	adantr	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to I \in (1 \dots N)$
8		fzfi	$⊢ (1 \dots N) \in Fin$
9		eqid	$⊢ (1 \dots N) Mat R = (1 \dots N) Mat R$
10		eqid	$⊢ {Base}_{((1 \dots N) Mat R)} = {Base}_{((1 \dots N) Mat R)}$
11	9 10 1	mat1bas	$⊢ (R \in Ring \land (1 \dots N) \in Fin) \to \underset{˙}{1} \in {Base}_{((1 \dots N) Mat R)}$
12	2 8 11	sylancl	$⊢ φ \to \underset{˙}{1} \in {Base}_{((1 \dots N) Mat R)}$
13		eqid	$⊢ {Base}_{R} = {Base}_{R}$
14	9 13	matbas2	$⊢ ((1 \dots N) \in Fin \land R \in Ring) \to {Base}_{R}^{((1 \dots N) \times (1 \dots N))} = {Base}_{((1 \dots N) Mat R)}$
15	8 2 14	sylancr	$⊢ φ \to {Base}_{R}^{((1 \dots N) \times (1 \dots N))} = {Base}_{((1 \dots N) Mat R)}$
16	12 15	eleqtrrd	$⊢ φ \to \underset{˙}{1} \in ({Base}_{R}^{((1 \dots N) \times (1 \dots N))})$
17	16	adantr	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to \underset{˙}{1} \in ({Base}_{R}^{((1 \dots N) \times (1 \dots N))})$
18		fz1ssnn	$⊢ (1 \dots N - 1) \subseteq ℕ$
19		simprl	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to i \in (1 \dots N - 1)$
20	18 19	sseldi	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to i \in ℕ$
21		simprr	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to j \in (1 \dots N - 1)$
22	18 21	sseldi	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to j \in ℕ$
23		eqidd	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to if (i < I, i, i + 1) = if (i < I, i, i + 1)$
24		eqidd	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to if (j < I, j, j + 1) = if (j < I, j, j + 1)$
25	5 6 6 7 7 17 20 22 23 24	smatlem	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to i (I {subMat}_{1} (\underset{˙}{1}) I) j = if (i < I, i, i + 1) \underset{˙}{1} if (j < I, j, j + 1)$
26		eqid	$⊢ 1_{R} = 1_{R}$
27		eqid	$⊢ 0_{R} = 0_{R}$
28	8	a1i	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to (1 \dots N) \in Fin$
29	2	adantr	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to R \in Ring$
30		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
31	20 30	eleqtrdi	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to i \in ℤ_{\geq 1}$
32		fznatpl1	$⊢ (N \in ℕ \land i \in (1 \dots N - 1)) \to i + 1 \in (1 \dots N)$
33	6 19 32	syl2anc	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to i + 1 \in (1 \dots N)$
34		peano2fzr	$⊢ (i \in ℤ_{\geq 1} \land i + 1 \in (1 \dots N)) \to i \in (1 \dots N)$
35	31 33 34	syl2anc	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to i \in (1 \dots N)$
36	35 33	jca	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to (i \in (1 \dots N) \land i + 1 \in (1 \dots N))$
37		eleq1	$⊢ i = if (i < I, i, i + 1) \to (i \in (1 \dots N) \leftrightarrow if (i < I, i, i + 1) \in (1 \dots N))$
38		eleq1	$⊢ i + 1 = if (i < I, i, i + 1) \to (i + 1 \in (1 \dots N) \leftrightarrow if (i < I, i, i + 1) \in (1 \dots N))$
39	37 38	ifboth	$⊢ (i \in (1 \dots N) \land i + 1 \in (1 \dots N)) \to if (i < I, i, i + 1) \in (1 \dots N)$
40	36 39	syl	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to if (i < I, i, i + 1) \in (1 \dots N)$
41	22 30	eleqtrdi	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to j \in ℤ_{\geq 1}$
42		fznatpl1	$⊢ (N \in ℕ \land j \in (1 \dots N - 1)) \to j + 1 \in (1 \dots N)$
43	6 21 42	syl2anc	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to j + 1 \in (1 \dots N)$
44		peano2fzr	$⊢ (j \in ℤ_{\geq 1} \land j + 1 \in (1 \dots N)) \to j \in (1 \dots N)$
45	41 43 44	syl2anc	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to j \in (1 \dots N)$
46	45 43	jca	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to (j \in (1 \dots N) \land j + 1 \in (1 \dots N))$
47		eleq1	$⊢ j = if (j < I, j, j + 1) \to (j \in (1 \dots N) \leftrightarrow if (j < I, j, j + 1) \in (1 \dots N))$
48		eleq1	$⊢ j + 1 = if (j < I, j, j + 1) \to (j + 1 \in (1 \dots N) \leftrightarrow if (j < I, j, j + 1) \in (1 \dots N))$
49	47 48	ifboth	$⊢ (j \in (1 \dots N) \land j + 1 \in (1 \dots N)) \to if (j < I, j, j + 1) \in (1 \dots N)$
50	46 49	syl	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to if (j < I, j, j + 1) \in (1 \dots N)$
51	9 26 27 28 29 40 50 1	mat1ov	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to if (i < I, i, i + 1) \underset{˙}{1} if (j < I, j, j + 1) = if (if (i < I, i, i + 1) = if (j < I, j, j + 1), 1_{R}, 0_{R})$
52		simpr	$⊢ ((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \to i < I$
53	52	iftrued	$⊢ ((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \to if (i < I, i, i + 1) = i$
54	53	eqeq1d	$⊢ ((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \to (if (i < I, i, i + 1) = if (j < I, j, j + 1) \leftrightarrow i = if (j < I, j, j + 1))$
55		simpr	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land j < I) \to j < I$
56	55	iftrued	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land j < I) \to if (j < I, j, j + 1) = j$
57	56	eqeq2d	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land j < I) \to (i = if (j < I, j, j + 1) \leftrightarrow i = j)$
58		simpr	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to \neg j < I$
59	58	iffalsed	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to if (j < I, j, j + 1) = j + 1$
60	59	eqeq2d	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to (i = if (j < I, j, j + 1) \leftrightarrow i = j + 1)$
61	20	nnred	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to i \in ℝ$
62	61	ad2antrr	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to i \in ℝ$
63		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
64	63 4	sseldi	$⊢ φ \to I \in ℕ$
65	64	nnred	$⊢ φ \to I \in ℝ$
66	65	ad3antrrr	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to I \in ℝ$
67	22	nnred	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to j \in ℝ$
68	67	ad2antrr	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to j \in ℝ$
69		1red	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to 1 \in ℝ$
70	68 69	readdcld	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to j + 1 \in ℝ$
71	52	adantr	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to i < I$
72	64	nnzd	$⊢ φ \to I \in ℤ$
73	72	ad3antrrr	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to I \in ℤ$
74	22	nnzd	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to j \in ℤ$
75	74	ad2antrr	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to j \in ℤ$
76	66 68 58	nltled	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to I \leq j$
77		zleltp1	$⊢ (I \in ℤ \land j \in ℤ) \to (I \leq j \leftrightarrow I < j + 1)$
78	77	biimpa	$⊢ ((I \in ℤ \land j \in ℤ) \land I \leq j) \to I < j + 1$
79	73 75 76 78	syl21anc	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to I < j + 1$
80	62 66 70 71 79	lttrd	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to i < j + 1$
81	62 80	ltned	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to i \neq j + 1$
82	81	neneqd	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to \neg i = j + 1$
83	62 66 68 71 76	ltletrd	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to i < j$
84	62 83	ltned	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to i \neq j$
85	84	neneqd	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to \neg i = j$
86	82 85	2falsed	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to (i = j + 1 \leftrightarrow i = j)$
87	60 86	bitrd	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \land \neg j < I) \to (i = if (j < I, j, j + 1) \leftrightarrow i = j)$
88	57 87	pm2.61dan	$⊢ ((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \to (i = if (j < I, j, j + 1) \leftrightarrow i = j)$
89	54 88	bitrd	$⊢ ((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land i < I) \to (if (i < I, i, i + 1) = if (j < I, j, j + 1) \leftrightarrow i = j)$
90		simpr	$⊢ ((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \to \neg i < I$
91	90	iffalsed	$⊢ ((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \to if (i < I, i, i + 1) = i + 1$
92	91	eqeq1d	$⊢ ((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \to (if (i < I, i, i + 1) = if (j < I, j, j + 1) \leftrightarrow i + 1 = if (j < I, j, j + 1))$
93		simpr	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to j < I$
94	93	iftrued	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to if (j < I, j, j + 1) = j$
95	94	eqeq2d	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to (i + 1 = if (j < I, j, j + 1) \leftrightarrow i + 1 = j)$
96	67	ad2antrr	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to j \in ℝ$
97	65	ad3antrrr	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to I \in ℝ$
98	61	ad2antrr	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to i \in ℝ$
99		1red	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to 1 \in ℝ$
100	98 99	readdcld	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to i + 1 \in ℝ$
101	72	ad3antrrr	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to I \in ℤ$
102	20	nnzd	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to i \in ℤ$
103	102	ad2antrr	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to i \in ℤ$
104	90	adantr	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to \neg i < I$
105	97 98 104	nltled	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to I \leq i$
106		zleltp1	$⊢ (I \in ℤ \land i \in ℤ) \to (I \leq i \leftrightarrow I < i + 1)$
107	106	biimpa	$⊢ ((I \in ℤ \land i \in ℤ) \land I \leq i) \to I < i + 1$
108	101 103 105 107	syl21anc	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to I < i + 1$
109	96 97 100 93 108	lttrd	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to j < i + 1$
110	96 109	ltned	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to j \neq i + 1$
111	110	necomd	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to i + 1 \neq j$
112	111	neneqd	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to \neg i + 1 = j$
113	96 97 98 93 105	ltletrd	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to j < i$
114	96 113	ltned	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to j \neq i$
115	114	necomd	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to i \neq j$
116	115	neneqd	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to \neg i = j$
117	112 116	2falsed	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to (i + 1 = j \leftrightarrow i = j)$
118	95 117	bitrd	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land j < I) \to (i + 1 = if (j < I, j, j + 1) \leftrightarrow i = j)$
119		simpr	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land \neg j < I) \to \neg j < I$
120	119	iffalsed	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land \neg j < I) \to if (j < I, j, j + 1) = j + 1$
121	120	eqeq2d	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land \neg j < I) \to (i + 1 = if (j < I, j, j + 1) \leftrightarrow i + 1 = j + 1)$
122	20	nncnd	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to i \in ℂ$
123	122	ad3antrrr	$⊢ ((((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land \neg j < I) \land i + 1 = j + 1) \to i \in ℂ$
124	22	nncnd	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to j \in ℂ$
125	124	ad3antrrr	$⊢ ((((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land \neg j < I) \land i + 1 = j + 1) \to j \in ℂ$
126		1cnd	$⊢ ((((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land \neg j < I) \land i + 1 = j + 1) \to 1 \in ℂ$
127		simpr	$⊢ ((((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land \neg j < I) \land i + 1 = j + 1) \to i + 1 = j + 1$
128	123 125 126 127	addcan2ad	$⊢ ((((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land \neg j < I) \land i + 1 = j + 1) \to i = j$
129		simpr	$⊢ ((((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land \neg j < I) \land i = j) \to i = j$
130	129	oveq1d	$⊢ ((((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land \neg j < I) \land i = j) \to i + 1 = j + 1$
131	128 130	impbida	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land \neg j < I) \to (i + 1 = j + 1 \leftrightarrow i = j)$
132	121 131	bitrd	$⊢ (((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \land \neg j < I) \to (i + 1 = if (j < I, j, j + 1) \leftrightarrow i = j)$
133	118 132	pm2.61dan	$⊢ ((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \to (i + 1 = if (j < I, j, j + 1) \leftrightarrow i = j)$
134	92 133	bitrd	$⊢ ((φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \land \neg i < I) \to (if (i < I, i, i + 1) = if (j < I, j, j + 1) \leftrightarrow i = j)$
135	89 134	pm2.61dan	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to (if (i < I, i, i + 1) = if (j < I, j, j + 1) \leftrightarrow i = j)$
136	135	ifbid	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to if (if (i < I, i, i + 1) = if (j < I, j, j + 1), 1_{R}, 0_{R}) = if (i = j, 1_{R}, 0_{R})$
137		eqid	$⊢ (1 \dots N - 1) Mat R = (1 \dots N - 1) Mat R$
138		fzfid	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to (1 \dots N - 1) \in Fin$
139		eqid	$⊢ 1_{((1 \dots N - 1) Mat R)} = 1_{((1 \dots N - 1) Mat R)}$
140	137 26 27 138 29 19 21 139	mat1ov	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to i 1_{((1 \dots N - 1) Mat R)} j = if (i = j, 1_{R}, 0_{R})$
141	136 140	eqtr4d	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to if (if (i < I, i, i + 1) = if (j < I, j, j + 1), 1_{R}, 0_{R}) = i 1_{((1 \dots N - 1) Mat R)} j$
142	25 51 141	3eqtrd	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to i (I {subMat}_{1} (\underset{˙}{1}) I) j = i 1_{((1 \dots N - 1) Mat R)} j$
143	142	ralrimivva	$⊢ φ \to \forall i \in (1 \dots N - 1) \forall j \in (1 \dots N - 1) i (I {subMat}_{1} (\underset{˙}{1}) I) j = i 1_{((1 \dots N - 1) Mat R)} j$
144	5 3 3 4 4 16	smatrcl	$⊢ φ \to I {subMat}_{1} (\underset{˙}{1}) I \in ({Base}_{R}^{((1 \dots N - 1) \times (1 \dots N - 1))})$
145		elmapfn	$⊢ I {subMat}_{1} (\underset{˙}{1}) I \in ({Base}_{R}^{((1 \dots N - 1) \times (1 \dots N - 1))}) \to (I {subMat}_{1} (\underset{˙}{1}) I) Fn ((1 \dots N - 1) \times (1 \dots N - 1))$
146	144 145	syl	$⊢ φ \to (I {subMat}_{1} (\underset{˙}{1}) I) Fn ((1 \dots N - 1) \times (1 \dots N - 1))$
147		fzfi	$⊢ (1 \dots N - 1) \in Fin$
148		eqid	$⊢ {Base}_{((1 \dots N - 1) Mat R)} = {Base}_{((1 \dots N - 1) Mat R)}$
149	137 148 139	mat1bas	$⊢ (R \in Ring \land (1 \dots N - 1) \in Fin) \to 1_{((1 \dots N - 1) Mat R)} \in {Base}_{((1 \dots N - 1) Mat R)}$
150	2 147 149	sylancl	$⊢ φ \to 1_{((1 \dots N - 1) Mat R)} \in {Base}_{((1 \dots N - 1) Mat R)}$
151	137 13	matbas2	$⊢ ((1 \dots N - 1) \in Fin \land R \in Ring) \to {Base}_{R}^{((1 \dots N - 1) \times (1 \dots N - 1))} = {Base}_{((1 \dots N - 1) Mat R)}$
152	147 2 151	sylancr	$⊢ φ \to {Base}_{R}^{((1 \dots N - 1) \times (1 \dots N - 1))} = {Base}_{((1 \dots N - 1) Mat R)}$
153	150 152	eleqtrrd	$⊢ φ \to 1_{((1 \dots N - 1) Mat R)} \in ({Base}_{R}^{((1 \dots N - 1) \times (1 \dots N - 1))})$
154		elmapfn	$⊢ 1_{((1 \dots N - 1) Mat R)} \in ({Base}_{R}^{((1 \dots N - 1) \times (1 \dots N - 1))}) \to 1_{((1 \dots N - 1) Mat R)} Fn ((1 \dots N - 1) \times (1 \dots N - 1))$
155	153 154	syl	$⊢ φ \to 1_{((1 \dots N - 1) Mat R)} Fn ((1 \dots N - 1) \times (1 \dots N - 1))$
156		eqfnov2	$⊢ ((I {subMat}_{1} (\underset{˙}{1}) I) Fn ((1 \dots N - 1) \times (1 \dots N - 1)) \land 1_{((1 \dots N - 1) Mat R)} Fn ((1 \dots N - 1) \times (1 \dots N - 1))) \to (I {subMat}_{1} (\underset{˙}{1}) I = 1_{((1 \dots N - 1) Mat R)} \leftrightarrow \forall i \in (1 \dots N - 1) \forall j \in (1 \dots N - 1) i (I {subMat}_{1} (\underset{˙}{1}) I) j = i 1_{((1 \dots N - 1) Mat R)} j)$
157	146 155 156	syl2anc	$⊢ φ \to (I {subMat}_{1} (\underset{˙}{1}) I = 1_{((1 \dots N - 1) Mat R)} \leftrightarrow \forall i \in (1 \dots N - 1) \forall j \in (1 \dots N - 1) i (I {subMat}_{1} (\underset{˙}{1}) I) j = i 1_{((1 \dots N - 1) Mat R)} j)$
158	143 157	mpbird	$⊢ φ \to I {subMat}_{1} (\underset{˙}{1}) I = 1_{((1 \dots N - 1) Mat R)}$

Metamath Proof Explorer

Theorem 1smat1

Proof