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 𝐴 = ( ( 1 ... 𝑁 ) Mat 𝑅 )
submateq.b 𝐵 = ( Base ‘ 𝐴 )
submateq.n ( 𝜑𝑁 ∈ ℕ )
submateq.i ( 𝜑𝐼 ∈ ( 1 ... 𝑁 ) )
submateq.j ( 𝜑𝐽 ∈ ( 1 ... 𝑁 ) )
submateq.e ( 𝜑𝐸𝐵 )
submateq.f ( 𝜑𝐹𝐵 )
submateq.1 ( ( 𝜑𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐽 } ) ) → ( 𝑖 𝐸 𝑗 ) = ( 𝑖 𝐹 𝑗 ) )
Assertion submateq ( 𝜑 → ( 𝐼 ( subMat1 ‘ 𝐸 ) 𝐽 ) = ( 𝐼 ( subMat1 ‘ 𝐹 ) 𝐽 ) )

Proof

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