Metamath Proof Explorer

Theorem madjusmdetlem3

Description: Lemma for madjusmdet . (Contributed by Thierry Arnoux, 27-Aug-2020)

Ref Expression
Hypotheses madjusmdet.b 
|- B = ( Base ` A )
madjusmdet.a 
|- A = ( ( 1 ... N ) Mat R )
madjusmdet.d 
|- D = ( ( 1 ... N ) maDet R )
madjusmdet.k 
|- K = ( ( 1 ... N ) maAdju R )
madjusmdet.t 
|- .x. = ( .r ` R )
madjusmdet.z 
|- Z = ( ZRHom ` R )
madjusmdet.e 
|- E = ( ( 1 ... ( N - 1 ) ) maDet R )
madjusmdet.n 
|- ( ph -> N e. NN )
madjusmdet.r 
|- ( ph -> R e. CRing )
madjusmdet.i 
|- ( ph -> I e. ( 1 ... N ) )
madjusmdet.j 
|- ( ph -> J e. ( 1 ... N ) )
madjusmdet.m 
|- ( ph -> M e. B )
madjusmdetlem2.p 
|- P = ( i e. ( 1 ... N ) |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )
madjusmdetlem2.s 
|- S = ( i e. ( 1 ... N ) |-> if ( i = 1 , N , if ( i <_ N , ( i - 1 ) , i ) ) )
madjusmdetlem4.q 
|- Q = ( j e. ( 1 ... N ) |-> if ( j = 1 , J , if ( j <_ J , ( j - 1 ) , j ) ) )
madjusmdetlem4.t 
|- T = ( j e. ( 1 ... N ) |-> if ( j = 1 , N , if ( j <_ N , ( j - 1 ) , j ) ) )
madjusmdetlem3.w 
|- W = ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( ( ( P o. `' S ) ` i ) U ( ( Q o. `' T ) ` j ) ) )
madjusmdetlem3.u 
|- ( ph -> U e. B )
Assertion madjusmdetlem3 
|- ( ph -> ( I ( subMat1 ` U ) J ) = ( N ( subMat1 ` W ) N ) )

Proof

Step Hyp Ref Expression
1 madjusmdet.b 
 |-  B = ( Base ` A )
2 madjusmdet.a 
 |-  A = ( ( 1 ... N ) Mat R )
3 madjusmdet.d 
 |-  D = ( ( 1 ... N ) maDet R )
4 madjusmdet.k 
 |-  K = ( ( 1 ... N ) maAdju R )
5 madjusmdet.t 
 |-  .x. = ( .r ` R )
6 madjusmdet.z 
 |-  Z = ( ZRHom ` R )
7 madjusmdet.e 
 |-  E = ( ( 1 ... ( N - 1 ) ) maDet R )
8 madjusmdet.n 
 |-  ( ph -> N e. NN )
9 madjusmdet.r 
 |-  ( ph -> R e. CRing )
10 madjusmdet.i 
 |-  ( ph -> I e. ( 1 ... N ) )
11 madjusmdet.j 
 |-  ( ph -> J e. ( 1 ... N ) )
12 madjusmdet.m 
 |-  ( ph -> M e. B )
13 madjusmdetlem2.p 
 |-  P = ( i e. ( 1 ... N ) |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )
14 madjusmdetlem2.s 
 |-  S = ( i e. ( 1 ... N ) |-> if ( i = 1 , N , if ( i <_ N , ( i - 1 ) , i ) ) )
15 madjusmdetlem4.q 
 |-  Q = ( j e. ( 1 ... N ) |-> if ( j = 1 , J , if ( j <_ J , ( j - 1 ) , j ) ) )
16 madjusmdetlem4.t 
 |-  T = ( j e. ( 1 ... N ) |-> if ( j = 1 , N , if ( j <_ N , ( j - 1 ) , j ) ) )
17 madjusmdetlem3.w 
 |-  W = ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( ( ( P o. `' S ) ` i ) U ( ( Q o. `' T ) ` j ) ) )
18 madjusmdetlem3.u 
 |-  ( ph -> U e. B )
19 nnuz 
 |-  NN = ( ZZ>= ` 1 )
20 8 19 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
21 fzdif2 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( ( 1 ... N ) \ { N } ) = ( 1 ... ( N - 1 ) ) )
22 20 21 syl 
 |-  ( ph -> ( ( 1 ... N ) \ { N } ) = ( 1 ... ( N - 1 ) ) )
23 difss 
 |-  ( ( 1 ... N ) \ { N } ) C_ ( 1 ... N )
24 22 23 eqsstrrdi 
 |-  ( ph -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
25 24 adantr 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
26 simprl 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> i e. ( 1 ... ( N - 1 ) ) )
27 25 26 sseldd 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> i e. ( 1 ... N ) )
28 simprr 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> j e. ( 1 ... ( N - 1 ) ) )
29 25 28 sseldd 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> j e. ( 1 ... N ) )
30 ovexd 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> ( ( ( P o. `' S ) ` i ) U ( ( Q o. `' T ) ` j ) ) e. _V )
31 17 ovmpt4g 
 |-  ( ( i e. ( 1 ... N ) /\ j e. ( 1 ... N ) /\ ( ( ( P o. `' S ) ` i ) U ( ( Q o. `' T ) ` j ) ) e. _V ) -> ( i W j ) = ( ( ( P o. `' S ) ` i ) U ( ( Q o. `' T ) ` j ) ) )
32 27 29 30 31 syl3anc 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> ( i W j ) = ( ( ( P o. `' S ) ` i ) U ( ( Q o. `' T ) ` j ) ) )
33 26 28 ovresd 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> ( i ( W |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) j ) = ( i W j ) )
34 eqid 
 |-  ( I ( subMat1 ` U ) J ) = ( I ( subMat1 ` U ) J )
35 8 adantr 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> N e. NN )
36 10 adantr 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> I e. ( 1 ... N ) )
37 11 adantr 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> J e. ( 1 ... N ) )
38 eqid 
 |-  ( Base ` R ) = ( Base ` R )
39 2 38 1 matbas2i 
 |-  ( U e. B -> U e. ( ( Base ` R ) ^m ( ( 1 ... N ) X. ( 1 ... N ) ) ) )
40 18 39 syl 
 |-  ( ph -> U e. ( ( Base ` R ) ^m ( ( 1 ... N ) X. ( 1 ... N ) ) ) )
41 40 adantr 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> U e. ( ( Base ` R ) ^m ( ( 1 ... N ) X. ( 1 ... N ) ) ) )
42 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
43 42 27 sselid 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> i e. NN )
44 42 29 sselid 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> j e. NN )
45 eqidd 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> if ( i < I , i , ( i + 1 ) ) = if ( i < I , i , ( i + 1 ) ) )
46 eqidd 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> if ( j < J , j , ( j + 1 ) ) = if ( j < J , j , ( j + 1 ) ) )
47 34 35 35 36 37 41 43 44 45 46 smatlem 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> ( i ( I ( subMat1 ` U ) J ) j ) = ( if ( i < I , i , ( i + 1 ) ) U if ( j < J , j , ( j + 1 ) ) ) )
48 1 2 3 4 5 6 7 8 9 10 10 12 13 14 madjusmdetlem2 
 |-  ( ( ph /\ i e. ( 1 ... ( N - 1 ) ) ) -> if ( i < I , i , ( i + 1 ) ) = ( ( P o. `' S ) ` i ) )
49 26 48 syldan 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> if ( i < I , i , ( i + 1 ) ) = ( ( P o. `' S ) ` i ) )
50 1 2 3 4 5 6 7 8 9 11 11 12 15 16 madjusmdetlem2 
 |-  ( ( ph /\ j e. ( 1 ... ( N - 1 ) ) ) -> if ( j < J , j , ( j + 1 ) ) = ( ( Q o. `' T ) ` j ) )
51 28 50 syldan 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> if ( j < J , j , ( j + 1 ) ) = ( ( Q o. `' T ) ` j ) )
52 49 51 oveq12d 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> ( if ( i < I , i , ( i + 1 ) ) U if ( j < J , j , ( j + 1 ) ) ) = ( ( ( P o. `' S ) ` i ) U ( ( Q o. `' T ) ` j ) ) )
53 47 52 eqtrd 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> ( i ( I ( subMat1 ` U ) J ) j ) = ( ( ( P o. `' S ) ` i ) U ( ( Q o. `' T ) ` j ) ) )
54 32 33 53 3eqtr4rd 
 |-  ( ( ph /\ ( i e. ( 1 ... ( N - 1 ) ) /\ j e. ( 1 ... ( N - 1 ) ) ) ) -> ( i ( I ( subMat1 ` U ) J ) j ) = ( i ( W |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) j ) )
55 54 ralrimivva 
 |-  ( ph -> A. i e. ( 1 ... ( N - 1 ) ) A. j e. ( 1 ... ( N - 1 ) ) ( i ( I ( subMat1 ` U ) J ) j ) = ( i ( W |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) j ) )
56 eqid 
 |-  ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) = ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) )
57 2 1 56 34 8 10 11 18 smatcl 
 |-  ( ph -> ( I ( subMat1 ` U ) J ) e. ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) )
58 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
59 eqid 
 |-  ( 1 ... N ) = ( 1 ... N )
60 eqid 
 |-  ( SymGrp ` ( 1 ... N ) ) = ( SymGrp ` ( 1 ... N ) )
61 eqid 
 |-  ( Base ` ( SymGrp ` ( 1 ... N ) ) ) = ( Base ` ( SymGrp ` ( 1 ... N ) ) )
62 59 13 60 61 fzto1st 
 |-  ( I e. ( 1 ... N ) -> P e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
63 10 62 syl 
 |-  ( ph -> P e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
64 eluzfz2 
 |-  ( N e. ( ZZ>= ` 1 ) -> N e. ( 1 ... N ) )
65 20 64 syl 
 |-  ( ph -> N e. ( 1 ... N ) )
66 59 14 60 61 fzto1st 
 |-  ( N e. ( 1 ... N ) -> S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
67 65 66 syl 
 |-  ( ph -> S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
68 eqid 
 |-  ( invg ` ( SymGrp ` ( 1 ... N ) ) ) = ( invg ` ( SymGrp ` ( 1 ... N ) ) )
69 60 61 68 symginv 
 |-  ( S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) -> ( ( invg ` ( SymGrp ` ( 1 ... N ) ) ) ` S ) = `' S )
70 67 69 syl 
 |-  ( ph -> ( ( invg ` ( SymGrp ` ( 1 ... N ) ) ) ` S ) = `' S )
71 60 symggrp 
 |-  ( ( 1 ... N ) e. Fin -> ( SymGrp ` ( 1 ... N ) ) e. Grp )
72 58 71 syl 
 |-  ( ph -> ( SymGrp ` ( 1 ... N ) ) e. Grp )
73 61 68 grpinvcl 
 |-  ( ( ( SymGrp ` ( 1 ... N ) ) e. Grp /\ S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( ( invg ` ( SymGrp ` ( 1 ... N ) ) ) ` S ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
74 72 67 73 syl2anc 
 |-  ( ph -> ( ( invg ` ( SymGrp ` ( 1 ... N ) ) ) ` S ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
75 70 74 eqeltrrd 
 |-  ( ph -> `' S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
76 eqid 
 |-  ( +g ` ( SymGrp ` ( 1 ... N ) ) ) = ( +g ` ( SymGrp ` ( 1 ... N ) ) )
77 60 61 76 symgov 
 |-  ( ( P e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) /\ `' S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( P ( +g ` ( SymGrp ` ( 1 ... N ) ) ) `' S ) = ( P o. `' S ) )
78 60 61 76 symgcl 
 |-  ( ( P e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) /\ `' S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( P ( +g ` ( SymGrp ` ( 1 ... N ) ) ) `' S ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
79 77 78 eqeltrrd 
 |-  ( ( P e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) /\ `' S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( P o. `' S ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
80 63 75 79 syl2anc 
 |-  ( ph -> ( P o. `' S ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
81 80 3ad2ant1 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( P o. `' S ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
82 simp2 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> i e. ( 1 ... N ) )
83 60 61 symgfv 
 |-  ( ( ( P o. `' S ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( P o. `' S ) ` i ) e. ( 1 ... N ) )
84 81 82 83 syl2anc 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( ( P o. `' S ) ` i ) e. ( 1 ... N ) )
85 59 15 60 61 fzto1st 
 |-  ( J e. ( 1 ... N ) -> Q e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
86 11 85 syl 
 |-  ( ph -> Q e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
87 59 16 60 61 fzto1st 
 |-  ( N e. ( 1 ... N ) -> T e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
88 65 87 syl 
 |-  ( ph -> T e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
89 60 61 68 symginv 
 |-  ( T e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) -> ( ( invg ` ( SymGrp ` ( 1 ... N ) ) ) ` T ) = `' T )
90 88 89 syl 
 |-  ( ph -> ( ( invg ` ( SymGrp ` ( 1 ... N ) ) ) ` T ) = `' T )
91 61 68 grpinvcl 
 |-  ( ( ( SymGrp ` ( 1 ... N ) ) e. Grp /\ T e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( ( invg ` ( SymGrp ` ( 1 ... N ) ) ) ` T ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
92 72 88 91 syl2anc 
 |-  ( ph -> ( ( invg ` ( SymGrp ` ( 1 ... N ) ) ) ` T ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
93 90 92 eqeltrrd 
 |-  ( ph -> `' T e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
94 60 61 76 symgov 
 |-  ( ( Q e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) /\ `' T e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( Q ( +g ` ( SymGrp ` ( 1 ... N ) ) ) `' T ) = ( Q o. `' T ) )
95 60 61 76 symgcl 
 |-  ( ( Q e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) /\ `' T e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( Q ( +g ` ( SymGrp ` ( 1 ... N ) ) ) `' T ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
96 94 95 eqeltrrd 
 |-  ( ( Q e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) /\ `' T e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( Q o. `' T ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
97 86 93 96 syl2anc 
 |-  ( ph -> ( Q o. `' T ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
98 97 3ad2ant1 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( Q o. `' T ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
99 simp3 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> j e. ( 1 ... N ) )
100 60 61 symgfv 
 |-  ( ( ( Q o. `' T ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( Q o. `' T ) ` j ) e. ( 1 ... N ) )
101 98 99 100 syl2anc 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( ( Q o. `' T ) ` j ) e. ( 1 ... N ) )
102 18 3ad2ant1 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> U e. B )
103 2 38 1 84 101 102 matecld 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( ( ( P o. `' S ) ` i ) U ( ( Q o. `' T ) ` j ) ) e. ( Base ` R ) )
104 2 38 1 58 9 103 matbas2d 
 |-  ( ph -> ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( ( ( P o. `' S ) ` i ) U ( ( Q o. `' T ) ` j ) ) ) e. B )
105 17 104 eqeltrid 
 |-  ( ph -> W e. B )
106 2 1 submatres 
 |-  ( ( N e. NN /\ W e. B ) -> ( N ( subMat1 ` W ) N ) = ( W |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) )
107 8 105 106 syl2anc 
 |-  ( ph -> ( N ( subMat1 ` W ) N ) = ( W |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) )
108 eqid 
 |-  ( N ( subMat1 ` W ) N ) = ( N ( subMat1 ` W ) N )
109 2 1 56 108 8 65 65 105 smatcl 
 |-  ( ph -> ( N ( subMat1 ` W ) N ) e. ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) )
110 107 109 eqeltrrd 
 |-  ( ph -> ( W |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) e. ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) )
111 eqid 
 |-  ( ( 1 ... ( N - 1 ) ) Mat R ) = ( ( 1 ... ( N - 1 ) ) Mat R )
112 111 56 eqmat 
 |-  ( ( ( I ( subMat1 ` U ) J ) e. ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) /\ ( W |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) e. ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) ) -> ( ( I ( subMat1 ` U ) J ) = ( W |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) <-> A. i e. ( 1 ... ( N - 1 ) ) A. j e. ( 1 ... ( N - 1 ) ) ( i ( I ( subMat1 ` U ) J ) j ) = ( i ( W |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) j ) ) )
113 57 110 112 syl2anc 
 |-  ( ph -> ( ( I ( subMat1 ` U ) J ) = ( W |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) <-> A. i e. ( 1 ... ( N - 1 ) ) A. j e. ( 1 ... ( N - 1 ) ) ( i ( I ( subMat1 ` U ) J ) j ) = ( i ( W |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) j ) ) )
114 55 113 mpbird 
 |-  ( ph -> ( I ( subMat1 ` U ) J ) = ( W |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) )
115 114 107 eqtr4d 
 |-  ( ph -> ( I ( subMat1 ` U ) J ) = ( N ( subMat1 ` W ) N ) )