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 sseldi ⊢ ( 𝜑 → 𝐽 ∈ ℕ )
103 102 nnred ⊢ ( 𝜑 → 𝐽 ∈ ℝ )
104 103 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝐽 ∈ ℝ )
105 fz1ssnn ⊢ ( 1 ... ( 𝑁 − 1 ) ) ⊆ ℕ
106 105 18 sseldi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 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 sseldi ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
176 175 nnred ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
177 176 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝐼 ∈ ℝ )
178 105 9 sseldi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 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 ‘ 𝐹 ) 𝐽 ) )