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 ... N ) Mat R ) )
1smat1.r 
|- ( ph -> R e. Ring )
1smat1.n 
|- ( ph -> N e. NN )
1smat1.i 
|- ( ph -> I e. ( 1 ... N ) )
Assertion 1smat1 
|- ( ph -> ( I ( subMat1 ` .1. ) I ) = ( 1r ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) )

Proof

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