submateq

Description: Sufficient condition for two submatrices to be equal. (Contributed by Thierry Arnoux, 25-Aug-2020)

	Ref	Expression
Hypotheses	submateq.a	$⊢ A = (1 \dots N) Mat R$
	submateq.b	$⊢ B = {Base}_{A}$
	submateq.n	$⊢ φ \to N \in ℕ$
	submateq.i	$⊢ φ \to I \in (1 \dots N)$
	submateq.j	$⊢ φ \to J \in (1 \dots N)$
	submateq.e	$⊢ φ \to E \in B$
	submateq.f	$⊢ φ \to F \in B$
	submateq.1	$⊢ (φ \land i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to i E j = i F j$
Assertion	submateq	$⊢ φ \to I {subMat}_{1} (E) J = I {subMat}_{1} (F) J$

Proof

Step	Hyp	Ref	Expression
1		submateq.a	$⊢ A = (1 \dots N) Mat R$
2		submateq.b	$⊢ B = {Base}_{A}$
3		submateq.n	$⊢ φ \to N \in ℕ$
4		submateq.i	$⊢ φ \to I \in (1 \dots N)$
5		submateq.j	$⊢ φ \to J \in (1 \dots N)$
6		submateq.e	$⊢ φ \to E \in B$
7		submateq.f	$⊢ φ \to F \in B$
8		submateq.1	$⊢ (φ \land i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to i E j = i F j$
9		simprl	$⊢ (φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \to x \in (1 \dots N - 1)$
10	3	ad2antrr	$⊢ ((φ \land x \in (1 \dots N - 1)) \land I \leq x) \to N \in ℕ$
11	4	ad2antrr	$⊢ ((φ \land x \in (1 \dots N - 1)) \land I \leq x) \to I \in (1 \dots N)$
12		simplr	$⊢ ((φ \land x \in (1 \dots N - 1)) \land I \leq x) \to x \in (1 \dots N - 1)$
13		simpr	$⊢ ((φ \land x \in (1 \dots N - 1)) \land I \leq x) \to I \leq x$
14	10 11 12 13	submateqlem1	$⊢ ((φ \land x \in (1 \dots N - 1)) \land I \leq x) \to (x \in (I \dots N) \land x + 1 \in ((1 \dots N) ∖ \{I\}))$
15	14	simprd	$⊢ ((φ \land x \in (1 \dots N - 1)) \land I \leq x) \to x + 1 \in ((1 \dots N) ∖ \{I\})$
16	9 15	syldanl	$⊢ ((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \to x + 1 \in ((1 \dots N) ∖ \{I\})$
17	16	adantr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land J \leq y) \to x + 1 \in ((1 \dots N) ∖ \{I\})$
18		simprr	$⊢ (φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \to y \in (1 \dots N - 1)$
19	3	ad2antrr	$⊢ ((φ \land y \in (1 \dots N - 1)) \land J \leq y) \to N \in ℕ$
20	5	ad2antrr	$⊢ ((φ \land y \in (1 \dots N - 1)) \land J \leq y) \to J \in (1 \dots N)$
21		simplr	$⊢ ((φ \land y \in (1 \dots N - 1)) \land J \leq y) \to y \in (1 \dots N - 1)$
22		simpr	$⊢ ((φ \land y \in (1 \dots N - 1)) \land J \leq y) \to J \leq y$
23	19 20 21 22	submateqlem1	$⊢ ((φ \land y \in (1 \dots N - 1)) \land J \leq y) \to (y \in (J \dots N) \land y + 1 \in ((1 \dots N) ∖ \{J\}))$
24	23	simprd	$⊢ ((φ \land y \in (1 \dots N - 1)) \land J \leq y) \to y + 1 \in ((1 \dots N) ∖ \{J\})$
25	18 24	syldanl	$⊢ ((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land J \leq y) \to y + 1 \in ((1 \dots N) ∖ \{J\})$
26	25	adantlr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land J \leq y) \to y + 1 \in ((1 \dots N) ∖ \{J\})$
27	17 26	jca	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land J \leq y) \to (x + 1 \in ((1 \dots N) ∖ \{I\}) \land y + 1 \in ((1 \dots N) ∖ \{J\}))$
28		ovexd	$⊢ φ \to x + 1 \in V$
29		ovexd	$⊢ φ \to y + 1 \in V$
30		simpl	$⊢ (i = x + 1 \land j = y + 1) \to i = x + 1$
31	30	eleq1d	$⊢ (i = x + 1 \land j = y + 1) \to (i \in ((1 \dots N) ∖ \{I\}) \leftrightarrow x + 1 \in ((1 \dots N) ∖ \{I\}))$
32		simpr	$⊢ (i = x + 1 \land j = y + 1) \to j = y + 1$
33	32	eleq1d	$⊢ (i = x + 1 \land j = y + 1) \to (j \in ((1 \dots N) ∖ \{J\}) \leftrightarrow y + 1 \in ((1 \dots N) ∖ \{J\}))$
34	31 33	anbi12d	$⊢ (i = x + 1 \land j = y + 1) \to ((i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \leftrightarrow (x + 1 \in ((1 \dots N) ∖ \{I\}) \land y + 1 \in ((1 \dots N) ∖ \{J\})))$
35		oveq12	$⊢ (i = x + 1 \land j = y + 1) \to i E j = (x + 1) E (y + 1)$
36		oveq12	$⊢ (i = x + 1 \land j = y + 1) \to i F j = (x + 1) F (y + 1)$
37	35 36	eqeq12d	$⊢ (i = x + 1 \land j = y + 1) \to (i E j = i F j \leftrightarrow (x + 1) E (y + 1) = (x + 1) F (y + 1))$
38	34 37	imbi12d	$⊢ (i = x + 1 \land j = y + 1) \to (((i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to i E j = i F j) \leftrightarrow ((x + 1 \in ((1 \dots N) ∖ \{I\}) \land y + 1 \in ((1 \dots N) ∖ \{J\})) \to (x + 1) E (y + 1) = (x + 1) F (y + 1)))$
39	8	3expib	$⊢ φ \to ((i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to i E j = i F j)$
40	28 29 38 39	vtocl2d	$⊢ φ \to ((x + 1 \in ((1 \dots N) ∖ \{I\}) \land y + 1 \in ((1 \dots N) ∖ \{J\})) \to (x + 1) E (y + 1) = (x + 1) F (y + 1))$
41	40	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land J \leq y) \to ((x + 1 \in ((1 \dots N) ∖ \{I\}) \land y + 1 \in ((1 \dots N) ∖ \{J\})) \to (x + 1) E (y + 1) = (x + 1) F (y + 1))$
42	27 41	mpd	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land J \leq y) \to (x + 1) E (y + 1) = (x + 1) F (y + 1)$
43		eqid	$⊢ I {subMat}_{1} (E) J = I {subMat}_{1} (E) J$
44	3	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land J \leq y) \to N \in ℕ$
45	4	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land J \leq y) \to I \in (1 \dots N)$
46	5	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land J \leq y) \to J \in (1 \dots N)$
47		eqid	$⊢ {Base}_{R} = {Base}_{R}$
48	1 47 2	matbas2i	$⊢ E \in B \to E \in ({Base}_{R}^{((1 \dots N) \times (1 \dots N))})$
49	6 48	syl	$⊢ φ \to E \in ({Base}_{R}^{((1 \dots N) \times (1 \dots N))})$
50	49	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land J \leq y) \to E \in ({Base}_{R}^{((1 \dots N) \times (1 \dots N))})$
51	14	simpld	$⊢ ((φ \land x \in (1 \dots N - 1)) \land I \leq x) \to x \in (I \dots N)$
52	9 51	syldanl	$⊢ ((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \to x \in (I \dots N)$
53	52	adantr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land J \leq y) \to x \in (I \dots N)$
54	23	simpld	$⊢ ((φ \land y \in (1 \dots N - 1)) \land J \leq y) \to y \in (J \dots N)$
55	18 54	syldanl	$⊢ ((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land J \leq y) \to y \in (J \dots N)$
56	55	adantlr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land J \leq y) \to y \in (J \dots N)$
57	43 44 44 45 46 50 53 56	smatbr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land J \leq y) \to x (I {subMat}_{1} (E) J) y = (x + 1) E (y + 1)$
58		eqid	$⊢ I {subMat}_{1} (F) J = I {subMat}_{1} (F) J$
59	1 47 2	matbas2i	$⊢ F \in B \to F \in ({Base}_{R}^{((1 \dots N) \times (1 \dots N))})$
60	7 59	syl	$⊢ φ \to F \in ({Base}_{R}^{((1 \dots N) \times (1 \dots N))})$
61	60	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land J \leq y) \to F \in ({Base}_{R}^{((1 \dots N) \times (1 \dots N))})$
62	58 44 44 45 46 61 53 56	smatbr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land J \leq y) \to x (I {subMat}_{1} (F) J) y = (x + 1) F (y + 1)$
63	42 57 62	3eqtr4d	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land J \leq y) \to x (I {subMat}_{1} (E) J) y = x (I {subMat}_{1} (F) J) y$
64	16	adantr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land y < J) \to x + 1 \in ((1 \dots N) ∖ \{I\})$
65	3	ad2antrr	$⊢ ((φ \land y \in (1 \dots N - 1)) \land y < J) \to N \in ℕ$
66	5	ad2antrr	$⊢ ((φ \land y \in (1 \dots N - 1)) \land y < J) \to J \in (1 \dots N)$
67		simplr	$⊢ ((φ \land y \in (1 \dots N - 1)) \land y < J) \to y \in (1 \dots N - 1)$
68		simpr	$⊢ ((φ \land y \in (1 \dots N - 1)) \land y < J) \to y < J$
69	65 66 67 68	submateqlem2	$⊢ ((φ \land y \in (1 \dots N - 1)) \land y < J) \to (y \in (1 ..^J) \land y \in ((1 \dots N) ∖ \{J\}))$
70	69	simprd	$⊢ ((φ \land y \in (1 \dots N - 1)) \land y < J) \to y \in ((1 \dots N) ∖ \{J\})$
71	18 70	syldanl	$⊢ ((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land y < J) \to y \in ((1 \dots N) ∖ \{J\})$
72	71	adantlr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land y < J) \to y \in ((1 \dots N) ∖ \{J\})$
73	64 72	jca	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land y < J) \to (x + 1 \in ((1 \dots N) ∖ \{I\}) \land y \in ((1 \dots N) ∖ \{J\}))$
74		vex	$⊢ y \in V$
75	74	a1i	$⊢ φ \to y \in V$
76		simpl	$⊢ (i = x + 1 \land j = y) \to i = x + 1$
77	76	eleq1d	$⊢ (i = x + 1 \land j = y) \to (i \in ((1 \dots N) ∖ \{I\}) \leftrightarrow x + 1 \in ((1 \dots N) ∖ \{I\}))$
78		simpr	$⊢ (i = x + 1 \land j = y) \to j = y$
79		eqidd	$⊢ (i = x + 1 \land j = y) \to (1 \dots N) ∖ \{J\} = (1 \dots N) ∖ \{J\}$
80	78 79	eleq12d	$⊢ (i = x + 1 \land j = y) \to (j \in ((1 \dots N) ∖ \{J\}) \leftrightarrow y \in ((1 \dots N) ∖ \{J\}))$
81	77 80	anbi12d	$⊢ (i = x + 1 \land j = y) \to ((i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \leftrightarrow (x + 1 \in ((1 \dots N) ∖ \{I\}) \land y \in ((1 \dots N) ∖ \{J\})))$
82		oveq12	$⊢ (i = x + 1 \land j = y) \to i E j = (x + 1) E y$
83		oveq12	$⊢ (i = x + 1 \land j = y) \to i F j = (x + 1) F y$
84	82 83	eqeq12d	$⊢ (i = x + 1 \land j = y) \to (i E j = i F j \leftrightarrow (x + 1) E y = (x + 1) F y)$
85	81 84	imbi12d	$⊢ (i = x + 1 \land j = y) \to (((i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to i E j = i F j) \leftrightarrow ((x + 1 \in ((1 \dots N) ∖ \{I\}) \land y \in ((1 \dots N) ∖ \{J\})) \to (x + 1) E y = (x + 1) F y))$
86	28 75 85 39	vtocl2d	$⊢ φ \to ((x + 1 \in ((1 \dots N) ∖ \{I\}) \land y \in ((1 \dots N) ∖ \{J\})) \to (x + 1) E y = (x + 1) F y)$
87	86	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land y < J) \to ((x + 1 \in ((1 \dots N) ∖ \{I\}) \land y \in ((1 \dots N) ∖ \{J\})) \to (x + 1) E y = (x + 1) F y)$
88	73 87	mpd	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land y < J) \to (x + 1) E y = (x + 1) F y$
89	3	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land y < J) \to N \in ℕ$
90	4	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land y < J) \to I \in (1 \dots N)$
91	5	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land y < J) \to J \in (1 \dots N)$
92	49	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land y < J) \to E \in ({Base}_{R}^{((1 \dots N) \times (1 \dots N))})$
93	52	adantr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land y < J) \to x \in (I \dots N)$
94	69	simpld	$⊢ ((φ \land y \in (1 \dots N - 1)) \land y < J) \to y \in (1 ..^J)$
95	18 94	syldanl	$⊢ ((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land y < J) \to y \in (1 ..^J)$
96	95	adantlr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land y < J) \to y \in (1 ..^J)$
97	43 89 89 90 91 92 93 96	smattr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land y < J) \to x (I {subMat}_{1} (E) J) y = (x + 1) E y$
98	60	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land y < J) \to F \in ({Base}_{R}^{((1 \dots N) \times (1 \dots N))})$
99	58 89 89 90 91 98 93 96	smattr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land y < J) \to x (I {subMat}_{1} (F) J) y = (x + 1) F y$
100	88 97 99	3eqtr4d	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \land y < J) \to x (I {subMat}_{1} (E) J) y = x (I {subMat}_{1} (F) J) y$
101		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
102	101 5	sseldi	$⊢ φ \to J \in ℕ$
103	102	nnred	$⊢ φ \to J \in ℝ$
104	103	adantr	$⊢ (φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \to J \in ℝ$
105		fz1ssnn	$⊢ (1 \dots N - 1) \subseteq ℕ$
106	105 18	sseldi	$⊢ (φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \to y \in ℕ$
107	106	nnred	$⊢ (φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \to y \in ℝ$
108		lelttric	$⊢ (J \in ℝ \land y \in ℝ) \to (J \leq y \lor y < J)$
109	104 107 108	syl2anc	$⊢ (φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \to (J \leq y \lor y < J)$
110	109	adantr	$⊢ ((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \to (J \leq y \lor y < J)$
111	63 100 110	mpjaodan	$⊢ ((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land I \leq x) \to x (I {subMat}_{1} (E) J) y = x (I {subMat}_{1} (F) J) y$
112	3	ad2antrr	$⊢ ((φ \land x \in (1 \dots N - 1)) \land x < I) \to N \in ℕ$
113	4	ad2antrr	$⊢ ((φ \land x \in (1 \dots N - 1)) \land x < I) \to I \in (1 \dots N)$
114		simplr	$⊢ ((φ \land x \in (1 \dots N - 1)) \land x < I) \to x \in (1 \dots N - 1)$
115		simpr	$⊢ ((φ \land x \in (1 \dots N - 1)) \land x < I) \to x < I$
116	112 113 114 115	submateqlem2	$⊢ ((φ \land x \in (1 \dots N - 1)) \land x < I) \to (x \in (1 ..^I) \land x \in ((1 \dots N) ∖ \{I\}))$
117	116	simprd	$⊢ ((φ \land x \in (1 \dots N - 1)) \land x < I) \to x \in ((1 \dots N) ∖ \{I\})$
118	9 117	syldanl	$⊢ ((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \to x \in ((1 \dots N) ∖ \{I\})$
119	118	adantr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land J \leq y) \to x \in ((1 \dots N) ∖ \{I\})$
120	25	adantlr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land J \leq y) \to y + 1 \in ((1 \dots N) ∖ \{J\})$
121	119 120	jca	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land J \leq y) \to (x \in ((1 \dots N) ∖ \{I\}) \land y + 1 \in ((1 \dots N) ∖ \{J\}))$
122		vex	$⊢ x \in V$
123	122	a1i	$⊢ φ \to x \in V$
124		simpl	$⊢ (i = x \land j = y + 1) \to i = x$
125	124	eleq1d	$⊢ (i = x \land j = y + 1) \to (i \in ((1 \dots N) ∖ \{I\}) \leftrightarrow x \in ((1 \dots N) ∖ \{I\}))$
126		simpr	$⊢ (i = x \land j = y + 1) \to j = y + 1$
127	126	eleq1d	$⊢ (i = x \land j = y + 1) \to (j \in ((1 \dots N) ∖ \{J\}) \leftrightarrow y + 1 \in ((1 \dots N) ∖ \{J\}))$
128	125 127	anbi12d	$⊢ (i = x \land j = y + 1) \to ((i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \leftrightarrow (x \in ((1 \dots N) ∖ \{I\}) \land y + 1 \in ((1 \dots N) ∖ \{J\})))$
129		oveq12	$⊢ (i = x \land j = y + 1) \to i E j = x E (y + 1)$
130		oveq12	$⊢ (i = x \land j = y + 1) \to i F j = x F (y + 1)$
131	129 130	eqeq12d	$⊢ (i = x \land j = y + 1) \to (i E j = i F j \leftrightarrow x E (y + 1) = x F (y + 1))$
132	128 131	imbi12d	$⊢ (i = x \land j = y + 1) \to (((i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to i E j = i F j) \leftrightarrow ((x \in ((1 \dots N) ∖ \{I\}) \land y + 1 \in ((1 \dots N) ∖ \{J\})) \to x E (y + 1) = x F (y + 1)))$
133	123 29 132 39	vtocl2d	$⊢ φ \to ((x \in ((1 \dots N) ∖ \{I\}) \land y + 1 \in ((1 \dots N) ∖ \{J\})) \to x E (y + 1) = x F (y + 1))$
134	133	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land J \leq y) \to ((x \in ((1 \dots N) ∖ \{I\}) \land y + 1 \in ((1 \dots N) ∖ \{J\})) \to x E (y + 1) = x F (y + 1))$
135	121 134	mpd	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land J \leq y) \to x E (y + 1) = x F (y + 1)$
136	3	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land J \leq y) \to N \in ℕ$
137	4	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land J \leq y) \to I \in (1 \dots N)$
138	5	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land J \leq y) \to J \in (1 \dots N)$
139	49	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land J \leq y) \to E \in ({Base}_{R}^{((1 \dots N) \times (1 \dots N))})$
140	116	simpld	$⊢ ((φ \land x \in (1 \dots N - 1)) \land x < I) \to x \in (1 ..^I)$
141	9 140	syldanl	$⊢ ((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \to x \in (1 ..^I)$
142	141	adantr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land J \leq y) \to x \in (1 ..^I)$
143	55	adantlr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land J \leq y) \to y \in (J \dots N)$
144	43 136 136 137 138 139 142 143	smatbl	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land J \leq y) \to x (I {subMat}_{1} (E) J) y = x E (y + 1)$
145	60	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land J \leq y) \to F \in ({Base}_{R}^{((1 \dots N) \times (1 \dots N))})$
146	58 136 136 137 138 145 142 143	smatbl	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land J \leq y) \to x (I {subMat}_{1} (F) J) y = x F (y + 1)$
147	135 144 146	3eqtr4d	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land J \leq y) \to x (I {subMat}_{1} (E) J) y = x (I {subMat}_{1} (F) J) y$
148	118	adantr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land y < J) \to x \in ((1 \dots N) ∖ \{I\})$
149	71	adantlr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land y < J) \to y \in ((1 \dots N) ∖ \{J\})$
150	148 149	jca	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land y < J) \to (x \in ((1 \dots N) ∖ \{I\}) \land y \in ((1 \dots N) ∖ \{J\}))$
151		simpl	$⊢ (i = x \land j = y) \to i = x$
152	151	eleq1d	$⊢ (i = x \land j = y) \to (i \in ((1 \dots N) ∖ \{I\}) \leftrightarrow x \in ((1 \dots N) ∖ \{I\}))$
153		simpr	$⊢ (i = x \land j = y) \to j = y$
154	153	eleq1d	$⊢ (i = x \land j = y) \to (j \in ((1 \dots N) ∖ \{J\}) \leftrightarrow y \in ((1 \dots N) ∖ \{J\}))$
155	152 154	anbi12d	$⊢ (i = x \land j = y) \to ((i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \leftrightarrow (x \in ((1 \dots N) ∖ \{I\}) \land y \in ((1 \dots N) ∖ \{J\})))$
156		oveq12	$⊢ (i = x \land j = y) \to i E j = x E y$
157		oveq12	$⊢ (i = x \land j = y) \to i F j = x F y$
158	156 157	eqeq12d	$⊢ (i = x \land j = y) \to (i E j = i F j \leftrightarrow x E y = x F y)$
159	155 158	imbi12d	$⊢ (i = x \land j = y) \to (((i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to i E j = i F j) \leftrightarrow ((x \in ((1 \dots N) ∖ \{I\}) \land y \in ((1 \dots N) ∖ \{J\})) \to x E y = x F y))$
160	123 75 159 39	vtocl2d	$⊢ φ \to ((x \in ((1 \dots N) ∖ \{I\}) \land y \in ((1 \dots N) ∖ \{J\})) \to x E y = x F y)$
161	160	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land y < J) \to ((x \in ((1 \dots N) ∖ \{I\}) \land y \in ((1 \dots N) ∖ \{J\})) \to x E y = x F y)$
162	150 161	mpd	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land y < J) \to x E y = x F y$
163	3	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land y < J) \to N \in ℕ$
164	4	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land y < J) \to I \in (1 \dots N)$
165	5	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land y < J) \to J \in (1 \dots N)$
166	49	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land y < J) \to E \in ({Base}_{R}^{((1 \dots N) \times (1 \dots N))})$
167	141	adantr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land y < J) \to x \in (1 ..^I)$
168	95	adantlr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land y < J) \to y \in (1 ..^J)$
169	43 163 163 164 165 166 167 168	smattl	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land y < J) \to x (I {subMat}_{1} (E) J) y = x E y$
170	60	ad3antrrr	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land y < J) \to F \in ({Base}_{R}^{((1 \dots N) \times (1 \dots N))})$
171	58 163 163 164 165 170 167 168	smattl	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land y < J) \to x (I {subMat}_{1} (F) J) y = x F y$
172	162 169 171	3eqtr4d	$⊢ (((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \land y < J) \to x (I {subMat}_{1} (E) J) y = x (I {subMat}_{1} (F) J) y$
173	109	adantr	$⊢ ((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \to (J \leq y \lor y < J)$
174	147 172 173	mpjaodan	$⊢ ((φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \land x < I) \to x (I {subMat}_{1} (E) J) y = x (I {subMat}_{1} (F) J) y$
175	101 4	sseldi	$⊢ φ \to I \in ℕ$
176	175	nnred	$⊢ φ \to I \in ℝ$
177	176	adantr	$⊢ (φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \to I \in ℝ$
178	105 9	sseldi	$⊢ (φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \to x \in ℕ$
179	178	nnred	$⊢ (φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \to x \in ℝ$
180		lelttric	$⊢ (I \in ℝ \land x \in ℝ) \to (I \leq x \lor x < I)$
181	177 179 180	syl2anc	$⊢ (φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \to (I \leq x \lor x < I)$
182	111 174 181	mpjaodan	$⊢ (φ \land (x \in (1 \dots N - 1) \land y \in (1 \dots N - 1))) \to x (I {subMat}_{1} (E) J) y = x (I {subMat}_{1} (F) J) y$
183	182	ralrimivva	$⊢ φ \to \forall x \in (1 \dots N - 1) \forall y \in (1 \dots N - 1) x (I {subMat}_{1} (E) J) y = x (I {subMat}_{1} (F) J) y$
184		eqid	$⊢ {Base}_{((1 \dots N - 1) Mat R)} = {Base}_{((1 \dots N - 1) Mat R)}$
185	1 2 184 43 3 4 5 6	smatcl	$⊢ φ \to I {subMat}_{1} (E) J \in {Base}_{((1 \dots N - 1) Mat R)}$
186	1 2 184 58 3 4 5 7	smatcl	$⊢ φ \to I {subMat}_{1} (F) J \in {Base}_{((1 \dots N - 1) Mat R)}$
187		eqid	$⊢ (1 \dots N - 1) Mat R = (1 \dots N - 1) Mat R$
188	187 184	eqmat	$⊢ (I {subMat}_{1} (E) J \in {Base}_{((1 \dots N - 1) Mat R)} \land I {subMat}_{1} (F) J \in {Base}_{((1 \dots N - 1) Mat R)}) \to (I {subMat}_{1} (E) J = I {subMat}_{1} (F) J \leftrightarrow \forall x \in (1 \dots N - 1) \forall y \in (1 \dots N - 1) x (I {subMat}_{1} (E) J) y = x (I {subMat}_{1} (F) J) y)$
189	185 186 188	syl2anc	$⊢ φ \to (I {subMat}_{1} (E) J = I {subMat}_{1} (F) J \leftrightarrow \forall x \in (1 \dots N - 1) \forall y \in (1 \dots N - 1) x (I {subMat}_{1} (E) J) y = x (I {subMat}_{1} (F) J) y)$
190	183 189	mpbird	$⊢ φ \to I {subMat}_{1} (E) J = I {subMat}_{1} (F) J$

Metamath Proof Explorer

Theorem submateq

Proof