Metamath Proof Explorer

Theorem 1smat1

Description: The submatrix of the identity matrix obtained by removing the ith row and the ith column is an identity matrix. Cf. 1marepvsma1 . (Contributed by Thierry Arnoux, 19-Aug-2020)

Ref Expression
Hypotheses 1smat1.1 ⊢ 1 = ( 1r ‘ ( ( 1 ... 𝑁 ) Mat 𝑅 ) )
1smat1.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
1smat1.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
1smat1.i ⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑁 ) )
Assertion 1smat1 ( 𝜑 → ( 𝐼 ( subMat1 ‘ 1 ) 𝐼 ) = ( 1r ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 1smat1.1 ⊢ 1 = ( 1r ‘ ( ( 1 ... 𝑁 ) Mat 𝑅 ) )
2 1smat1.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
3 1smat1.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 1smat1.i ⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑁 ) )
5 eqid ⊢ ( 𝐼 ( subMat1 ‘ 1 ) 𝐼 ) = ( 𝐼 ( subMat1 ‘ 1 ) 𝐼 )
6 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑁 ∈ ℕ )
7 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝐼 ∈ ( 1 ... 𝑁 ) )
8 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
9 eqid ⊢ ( ( 1 ... 𝑁 ) Mat 𝑅 ) = ( ( 1 ... 𝑁 ) Mat 𝑅 )
10 eqid ⊢ ( Base ‘ ( ( 1 ... 𝑁 ) Mat 𝑅 ) ) = ( Base ‘ ( ( 1 ... 𝑁 ) Mat 𝑅 ) )
11 9 10 1 mat1bas ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1 ... 𝑁 ) ∈ Fin ) → 1 ∈ ( Base ‘ ( ( 1 ... 𝑁 ) Mat 𝑅 ) ) )
12 2 8 11 sylancl ⊢ ( 𝜑 → 1 ∈ ( Base ‘ ( ( 1 ... 𝑁 ) Mat 𝑅 ) ) )
13 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14 9 13 matbas2 ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... 𝑁 ) × ( 1 ... 𝑁 ) ) ) = ( Base ‘ ( ( 1 ... 𝑁 ) Mat 𝑅 ) ) )
15 8 2 14 sylancr ⊢ ( 𝜑 → ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... 𝑁 ) × ( 1 ... 𝑁 ) ) ) = ( Base ‘ ( ( 1 ... 𝑁 ) Mat 𝑅 ) ) )
16 12 15 eleqtrrd ⊢ ( 𝜑 → 1 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... 𝑁 ) × ( 1 ... 𝑁 ) ) ) )
17 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 1 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... 𝑁 ) × ( 1 ... 𝑁 ) ) ) )
18 fz1ssnn ⊢ ( 1 ... ( 𝑁 − 1 ) ) ⊆ ℕ
19 simprl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
20 18 19 sselid ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑖 ∈ ℕ )
21 simprr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
22 18 21 sselid ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑗 ∈ ℕ )
23 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) = if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) )
24 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) )
25 5 6 6 7 7 17 20 22 23 24 smatlem ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( 𝑖 ( 𝐼 ( subMat1 ‘ 1 ) 𝐼 ) 𝑗 ) = ( if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) 1 if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ) )
26 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
27 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
28 8 a1i ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( 1 ... 𝑁 ) ∈ Fin )
29 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑅 ∈ Ring )
30 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
31 20 30 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ 1 ) )
32 fznatpl1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 1 ... 𝑁 ) )
33 6 19 32 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( 𝑖 + 1 ) ∈ ( 1 ... 𝑁 ) )
34 peano2fzr ⊢ ( ( 𝑖 ∈ ( ℤ≥ ‘ 1 ) ∧ ( 𝑖 + 1 ) ∈ ( 1 ... 𝑁 ) ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
35 31 33 34 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
36 35 33 jca ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ ( 𝑖 + 1 ) ∈ ( 1 ... 𝑁 ) ) )
37 eleq1 ⊢ ( 𝑖 = if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) → ( 𝑖 ∈ ( 1 ... 𝑁 ) ↔ if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) ∈ ( 1 ... 𝑁 ) ) )
38 eleq1 ⊢ ( ( 𝑖 + 1 ) = if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) → ( ( 𝑖 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) ∈ ( 1 ... 𝑁 ) ) )
39 37 38 ifboth ⊢ ( ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ ( 𝑖 + 1 ) ∈ ( 1 ... 𝑁 ) ) → if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) ∈ ( 1 ... 𝑁 ) )
40 36 39 syl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) ∈ ( 1 ... 𝑁 ) )
41 22 30 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑗 ∈ ( ℤ≥ ‘ 1 ) )
42 fznatpl1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑗 + 1 ) ∈ ( 1 ... 𝑁 ) )
43 6 21 42 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( 𝑗 + 1 ) ∈ ( 1 ... 𝑁 ) )
44 peano2fzr ⊢ ( ( 𝑗 ∈ ( ℤ≥ ‘ 1 ) ∧ ( 𝑗 + 1 ) ∈ ( 1 ... 𝑁 ) ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
45 41 43 44 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
46 45 43 jca ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ∧ ( 𝑗 + 1 ) ∈ ( 1 ... 𝑁 ) ) )
47 eleq1 ⊢ ( 𝑗 = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ∈ ( 1 ... 𝑁 ) ) )
48 eleq1 ⊢ ( ( 𝑗 + 1 ) = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) → ( ( 𝑗 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ∈ ( 1 ... 𝑁 ) ) )
49 47 48 ifboth ⊢ ( ( 𝑗 ∈ ( 1 ... 𝑁 ) ∧ ( 𝑗 + 1 ) ∈ ( 1 ... 𝑁 ) ) → if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ∈ ( 1 ... 𝑁 ) )
50 46 49 syl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ∈ ( 1 ... 𝑁 ) )
51 9 26 27 28 29 40 50 1 mat1ov ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) 1 if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ) = if ( if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
52 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) → 𝑖 < 𝐼 )
53 52 iftrued ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) → if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) = 𝑖 )
54 53 eqeq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) → ( if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ↔ 𝑖 = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ) )
55 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → 𝑗 < 𝐼 )
56 55 iftrued ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) = 𝑗 )
57 56 eqeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → ( 𝑖 = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ↔ 𝑖 = 𝑗 ) )
58 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → ¬ 𝑗 < 𝐼 )
59 58 iffalsed ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) = ( 𝑗 + 1 ) )
60 59 eqeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → ( 𝑖 = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ↔ 𝑖 = ( 𝑗 + 1 ) ) )
61 20 nnred ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑖 ∈ ℝ )
62 61 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → 𝑖 ∈ ℝ )
63 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
64 63 4 sselid ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
65 64 nnred ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
66 65 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → 𝐼 ∈ ℝ )
67 22 nnred ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑗 ∈ ℝ )
68 67 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → 𝑗 ∈ ℝ )
69 1red ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → 1 ∈ ℝ )
70 68 69 readdcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → ( 𝑗 + 1 ) ∈ ℝ )
71 52 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → 𝑖 < 𝐼 )
72 64 nnzd ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
73 72 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → 𝐼 ∈ ℤ )
74 22 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑗 ∈ ℤ )
75 74 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → 𝑗 ∈ ℤ )
76 66 68 58 nltled ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → 𝐼 ≤ 𝑗 )
77 zleltp1 ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 𝐼 ≤ 𝑗 ↔ 𝐼 < ( 𝑗 + 1 ) ) )
78 77 biimpa ⊢ ( ( ( 𝐼 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ∧ 𝐼 ≤ 𝑗 ) → 𝐼 < ( 𝑗 + 1 ) )
79 73 75 76 78 syl21anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → 𝐼 < ( 𝑗 + 1 ) )
80 62 66 70 71 79 lttrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → 𝑖 < ( 𝑗 + 1 ) )
81 62 80 ltned ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → 𝑖 ≠ ( 𝑗 + 1 ) )
82 81 neneqd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → ¬ 𝑖 = ( 𝑗 + 1 ) )
83 62 66 68 71 76 ltletrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → 𝑖 < 𝑗 )
84 62 83 ltned ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → 𝑖 ≠ 𝑗 )
85 84 neneqd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → ¬ 𝑖 = 𝑗 )
86 82 85 2falsed ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → ( 𝑖 = ( 𝑗 + 1 ) ↔ 𝑖 = 𝑗 ) )
87 60 86 bitrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → ( 𝑖 = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ↔ 𝑖 = 𝑗 ) )
88 57 87 pm2.61dan ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) → ( 𝑖 = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ↔ 𝑖 = 𝑗 ) )
89 54 88 bitrd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 < 𝐼 ) → ( if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ↔ 𝑖 = 𝑗 ) )
90 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) → ¬ 𝑖 < 𝐼 )
91 90 iffalsed ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) → if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) = ( 𝑖 + 1 ) )
92 91 eqeq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) → ( if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ↔ ( 𝑖 + 1 ) = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ) )
93 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → 𝑗 < 𝐼 )
94 93 iftrued ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) = 𝑗 )
95 94 eqeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → ( ( 𝑖 + 1 ) = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ↔ ( 𝑖 + 1 ) = 𝑗 ) )
96 67 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → 𝑗 ∈ ℝ )
97 65 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → 𝐼 ∈ ℝ )
98 61 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → 𝑖 ∈ ℝ )
99 1red ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → 1 ∈ ℝ )
100 98 99 readdcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → ( 𝑖 + 1 ) ∈ ℝ )
101 72 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → 𝐼 ∈ ℤ )
102 20 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑖 ∈ ℤ )
103 102 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → 𝑖 ∈ ℤ )
104 90 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → ¬ 𝑖 < 𝐼 )
105 97 98 104 nltled ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → 𝐼 ≤ 𝑖 )
106 zleltp1 ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 𝐼 ≤ 𝑖 ↔ 𝐼 < ( 𝑖 + 1 ) ) )
107 106 biimpa ⊢ ( ( ( 𝐼 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝐼 ≤ 𝑖 ) → 𝐼 < ( 𝑖 + 1 ) )
108 101 103 105 107 syl21anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → 𝐼 < ( 𝑖 + 1 ) )
109 96 97 100 93 108 lttrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → 𝑗 < ( 𝑖 + 1 ) )
110 96 109 ltned ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → 𝑗 ≠ ( 𝑖 + 1 ) )
111 110 necomd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → ( 𝑖 + 1 ) ≠ 𝑗 )
112 111 neneqd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → ¬ ( 𝑖 + 1 ) = 𝑗 )
113 96 97 98 93 105 ltletrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → 𝑗 < 𝑖 )
114 96 113 ltned ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → 𝑗 ≠ 𝑖 )
115 114 necomd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → 𝑖 ≠ 𝑗 )
116 115 neneqd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → ¬ 𝑖 = 𝑗 )
117 112 116 2falsed ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → ( ( 𝑖 + 1 ) = 𝑗 ↔ 𝑖 = 𝑗 ) )
118 95 117 bitrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ 𝑗 < 𝐼 ) → ( ( 𝑖 + 1 ) = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ↔ 𝑖 = 𝑗 ) )
119 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → ¬ 𝑗 < 𝐼 )
120 119 iffalsed ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) = ( 𝑗 + 1 ) )
121 120 eqeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → ( ( 𝑖 + 1 ) = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ↔ ( 𝑖 + 1 ) = ( 𝑗 + 1 ) ) )
122 20 nncnd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑖 ∈ ℂ )
123 122 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) ∧ ( 𝑖 + 1 ) = ( 𝑗 + 1 ) ) → 𝑖 ∈ ℂ )
124 22 nncnd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑗 ∈ ℂ )
125 124 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) ∧ ( 𝑖 + 1 ) = ( 𝑗 + 1 ) ) → 𝑗 ∈ ℂ )
126 1cnd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) ∧ ( 𝑖 + 1 ) = ( 𝑗 + 1 ) ) → 1 ∈ ℂ )
127 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) ∧ ( 𝑖 + 1 ) = ( 𝑗 + 1 ) ) → ( 𝑖 + 1 ) = ( 𝑗 + 1 ) )
128 123 125 126 127 addcan2ad ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) ∧ ( 𝑖 + 1 ) = ( 𝑗 + 1 ) ) → 𝑖 = 𝑗 )
129 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) ∧ 𝑖 = 𝑗 ) → 𝑖 = 𝑗 )
130 129 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) ∧ 𝑖 = 𝑗 ) → ( 𝑖 + 1 ) = ( 𝑗 + 1 ) )
131 128 130 impbida ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → ( ( 𝑖 + 1 ) = ( 𝑗 + 1 ) ↔ 𝑖 = 𝑗 ) )
132 121 131 bitrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) ∧ ¬ 𝑗 < 𝐼 ) → ( ( 𝑖 + 1 ) = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ↔ 𝑖 = 𝑗 ) )
133 118 132 pm2.61dan ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) → ( ( 𝑖 + 1 ) = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ↔ 𝑖 = 𝑗 ) )
134 92 133 bitrd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ∧ ¬ 𝑖 < 𝐼 ) → ( if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ↔ 𝑖 = 𝑗 ) )
135 89 134 pm2.61dan ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) ↔ 𝑖 = 𝑗 ) )
136 135 ifbid ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → if ( if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
137 eqid ⊢ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) = ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 )
138 fzfid ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( 1 ... ( 𝑁 − 1 ) ) ∈ Fin )
139 eqid ⊢ ( 1r ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) = ( 1r ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) )
140 137 26 27 138 29 19 21 139 mat1ov ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( 𝑖 ( 1r ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) 𝑗 ) = if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
141 136 140 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → if ( if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) = if ( 𝑗 < 𝐼 , 𝑗 , ( 𝑗 + 1 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 𝑖 ( 1r ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) 𝑗 ) )
142 25 51 141 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( 𝑖 ( 𝐼 ( subMat1 ‘ 1 ) 𝐼 ) 𝑗 ) = ( 𝑖 ( 1r ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) 𝑗 ) )
143 142 ralrimivva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∀ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 𝑖 ( 𝐼 ( subMat1 ‘ 1 ) 𝐼 ) 𝑗 ) = ( 𝑖 ( 1r ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) 𝑗 ) )
144 5 3 3 4 4 16 smatrcl ⊢ ( 𝜑 → ( 𝐼 ( subMat1 ‘ 1 ) 𝐼 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) )
145 elmapfn ⊢ ( ( 𝐼 ( subMat1 ‘ 1 ) 𝐼 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( 𝐼 ( subMat1 ‘ 1 ) 𝐼 ) Fn ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) )
146 144 145 syl ⊢ ( 𝜑 → ( 𝐼 ( subMat1 ‘ 1 ) 𝐼 ) Fn ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) )
147 fzfi ⊢ ( 1 ... ( 𝑁 − 1 ) ) ∈ Fin
148 eqid ⊢ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) = ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) )
149 137 148 139 mat1bas ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1 ... ( 𝑁 − 1 ) ) ∈ Fin ) → ( 1r ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) )
150 2 147 149 sylancl ⊢ ( 𝜑 → ( 1r ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) )
151 137 13 matbas2 ⊢ ( ( ( 1 ... ( 𝑁 − 1 ) ) ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) = ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) )
152 147 2 151 sylancr ⊢ ( 𝜑 → ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) = ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) )
153 150 152 eleqtrrd ⊢ ( 𝜑 → ( 1r ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) )
154 elmapfn ⊢ ( ( 1r ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( 1r ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) Fn ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) )
155 153 154 syl ⊢ ( 𝜑 → ( 1r ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) Fn ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) )
156 eqfnov2 ⊢ ( ( ( 𝐼 ( subMat1 ‘ 1 ) 𝐼 ) Fn ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ( 1r ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) Fn ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( ( 𝐼 ( subMat1 ‘ 1 ) 𝐼 ) = ( 1r ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) ↔ ∀ 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∀ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 𝑖 ( 𝐼 ( subMat1 ‘ 1 ) 𝐼 ) 𝑗 ) = ( 𝑖 ( 1r ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) 𝑗 ) ) )
157 146 155 156 syl2anc ⊢ ( 𝜑 → ( ( 𝐼 ( subMat1 ‘ 1 ) 𝐼 ) = ( 1r ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) ↔ ∀ 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∀ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 𝑖 ( 𝐼 ( subMat1 ‘ 1 ) 𝐼 ) 𝑗 ) = ( 𝑖 ( 1r ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) 𝑗 ) ) )
158 143 157 mpbird ⊢ ( 𝜑 → ( 𝐼 ( subMat1 ‘ 1 ) 𝐼 ) = ( 1r ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) )