Metamath Proof Explorer


Theorem submateq

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

Ref Expression
Hypotheses submateq.a A = 1 N Mat R
submateq.b B = Base A
submateq.n φ N
submateq.i φ I 1 N
submateq.j φ J 1 N
submateq.e φ E B
submateq.f φ F B
submateq.1 φ i 1 N I j 1 N J i E j = i F j
Assertion submateq φ I subMat 1 E J = I subMat 1 F J

Proof

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