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 
|- ( ph -> N e. NN )
submateq.i 
|- ( ph -> I e. ( 1 ... N ) )
submateq.j 
|- ( ph -> J e. ( 1 ... N ) )
submateq.e 
|- ( ph -> E e. B )
submateq.f 
|- ( ph -> F e. B )
submateq.1 
|- ( ( ph /\ i e. ( ( 1 ... N ) \ { I } ) /\ j e. ( ( 1 ... N ) \ { J } ) ) -> ( i E j ) = ( i F j ) )
Assertion submateq 
|- ( ph -> ( I ( subMat1 ` E ) J ) = ( I ( subMat1 ` F ) J ) )

Proof

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