Metamath Proof Explorer

Theorem madjusmdetlem1

Description: Lemma for madjusmdet . (Contributed by Thierry Arnoux, 22-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 )
madjusmdetlem1.g 
|- G = ( Base ` ( SymGrp ` ( 1 ... N ) ) )
madjusmdetlem1.s 
|- S = ( pmSgn ` ( 1 ... N ) )
madjusmdetlem1.u 
|- U = ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J )
madjusmdetlem1.w 
|- W = ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( ( P ` i ) U ( Q ` j ) ) )
madjusmdetlem1.p 
|- ( ph -> P e. G )
madjusmdetlem1.q 
|- ( ph -> Q e. G )
madjusmdetlem1.1 
|- ( ph -> ( P ` N ) = I )
madjusmdetlem1.2 
|- ( ph -> ( Q ` N ) = J )
madjusmdetlem1.3 
|- ( ph -> ( I ( subMat1 ` U ) J ) = ( N ( subMat1 ` W ) N ) )
Assertion madjusmdetlem1 
|- ( ph -> ( J ( K ` M ) I ) = ( ( Z ` ( ( S ` P ) x. ( S ` Q ) ) ) .x. ( E ` ( I ( subMat1 ` M ) J ) ) ) )

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 madjusmdetlem1.g 
 |-  G = ( Base ` ( SymGrp ` ( 1 ... N ) ) )
14 madjusmdetlem1.s 
 |-  S = ( pmSgn ` ( 1 ... N ) )
15 madjusmdetlem1.u 
 |-  U = ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J )
16 madjusmdetlem1.w 
 |-  W = ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( ( P ` i ) U ( Q ` j ) ) )
17 madjusmdetlem1.p 
 |-  ( ph -> P e. G )
18 madjusmdetlem1.q 
 |-  ( ph -> Q e. G )
19 madjusmdetlem1.1 
 |-  ( ph -> ( P ` N ) = I )
20 madjusmdetlem1.2 
 |-  ( ph -> ( Q ` N ) = J )
21 madjusmdetlem1.3 
 |-  ( ph -> ( I ( subMat1 ` U ) J ) = ( N ( subMat1 ` W ) N ) )
22 2 1 3 4 maducoevalmin1 
 |-  ( ( M e. B /\ J e. ( 1 ... N ) /\ I e. ( 1 ... N ) ) -> ( J ( K ` M ) I ) = ( D ` ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ) )
23 12 11 10 22 syl3anc 
 |-  ( ph -> ( J ( K ` M ) I ) = ( D ` ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ) )
24 15 fveq2i 
 |-  ( D ` U ) = ( D ` ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) )
25 23 24 eqtr4di 
 |-  ( ph -> ( J ( K ` M ) I ) = ( D ` U ) )
26 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
27 crngring 
 |-  ( R e. CRing -> R e. Ring )
28 9 27 syl 
 |-  ( ph -> R e. Ring )
29 2 1 minmar1cl 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ ( I e. ( 1 ... N ) /\ J e. ( 1 ... N ) ) ) -> ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) e. B )
30 28 12 10 11 29 syl22anc 
 |-  ( ph -> ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) e. B )
31 15 30 eqeltrid 
 |-  ( ph -> U e. B )
32 2 1 3 13 14 6 5 16 9 26 31 17 18 mdetpmtr12 
 |-  ( ph -> ( D ` U ) = ( ( Z ` ( ( S ` P ) x. ( S ` Q ) ) ) .x. ( D ` W ) ) )
33 simplr 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ j = N ) -> i = N )
34 33 fveq2d 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ j = N ) -> ( P ` i ) = ( P ` N ) )
35 19 3ad2ant1 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( P ` N ) = I )
36 35 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ j = N ) -> ( P ` N ) = I )
37 34 36 eqtrd 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ j = N ) -> ( P ` i ) = I )
38 simpr 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ j = N ) -> j = N )
39 38 fveq2d 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ j = N ) -> ( Q ` j ) = ( Q ` N ) )
40 20 3ad2ant1 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( Q ` N ) = J )
41 40 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ j = N ) -> ( Q ` N ) = J )
42 39 41 eqtrd 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ j = N ) -> ( Q ` j ) = J )
43 37 42 oveq12d 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ j = N ) -> ( ( P ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( Q ` j ) ) = ( I ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) J ) )
44 12 3ad2ant1 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> M e. B )
45 44 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ j = N ) -> M e. B )
46 10 3ad2ant1 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> I e. ( 1 ... N ) )
47 46 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ j = N ) -> I e. ( 1 ... N ) )
48 11 3ad2ant1 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> J e. ( 1 ... N ) )
49 48 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ j = N ) -> J e. ( 1 ... N ) )
50 eqid 
 |-  ( ( 1 ... N ) minMatR1 R ) = ( ( 1 ... N ) minMatR1 R )
51 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
52 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
53 2 1 50 51 52 minmar1eval 
 |-  ( ( M e. B /\ ( I e. ( 1 ... N ) /\ J e. ( 1 ... N ) ) /\ ( I e. ( 1 ... N ) /\ J e. ( 1 ... N ) ) ) -> ( I ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) J ) = if ( I = I , if ( J = J , ( 1r ` R ) , ( 0g ` R ) ) , ( I M J ) ) )
54 45 47 49 47 49 53 syl122anc 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ j = N ) -> ( I ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) J ) = if ( I = I , if ( J = J , ( 1r ` R ) , ( 0g ` R ) ) , ( I M J ) ) )
55 eqid 
 |-  I = I
56 55 iftruei 
 |-  if ( I = I , if ( J = J , ( 1r ` R ) , ( 0g ` R ) ) , ( I M J ) ) = if ( J = J , ( 1r ` R ) , ( 0g ` R ) )
57 eqid 
 |-  J = J
58 57 iftruei 
 |-  if ( J = J , ( 1r ` R ) , ( 0g ` R ) ) = ( 1r ` R )
59 56 58 eqtri 
 |-  if ( I = I , if ( J = J , ( 1r ` R ) , ( 0g ` R ) ) , ( I M J ) ) = ( 1r ` R )
60 59 a1i 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ j = N ) -> if ( I = I , if ( J = J , ( 1r ` R ) , ( 0g ` R ) ) , ( I M J ) ) = ( 1r ` R ) )
61 43 54 60 3eqtrrd 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ j = N ) -> ( 1r ` R ) = ( ( P ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( Q ` j ) ) )
62 simplr 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ -. j = N ) -> i = N )
63 62 fveq2d 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ -. j = N ) -> ( P ` i ) = ( P ` N ) )
64 35 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ -. j = N ) -> ( P ` N ) = I )
65 63 64 eqtrd 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ -. j = N ) -> ( P ` i ) = I )
66 65 oveq1d 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ -. j = N ) -> ( ( P ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( Q ` j ) ) = ( I ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( Q ` j ) ) )
67 44 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ -. j = N ) -> M e. B )
68 46 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ -. j = N ) -> I e. ( 1 ... N ) )
69 48 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ -. j = N ) -> J e. ( 1 ... N ) )
70 18 3ad2ant1 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> Q e. G )
71 simp3 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> j e. ( 1 ... N ) )
72 eqid 
 |-  ( SymGrp ` ( 1 ... N ) ) = ( SymGrp ` ( 1 ... N ) )
73 72 13 symgfv 
 |-  ( ( Q e. G /\ j e. ( 1 ... N ) ) -> ( Q ` j ) e. ( 1 ... N ) )
74 70 71 73 syl2anc 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( Q ` j ) e. ( 1 ... N ) )
75 74 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ -. j = N ) -> ( Q ` j ) e. ( 1 ... N ) )
76 2 1 50 51 52 minmar1eval 
 |-  ( ( M e. B /\ ( I e. ( 1 ... N ) /\ J e. ( 1 ... N ) ) /\ ( I e. ( 1 ... N ) /\ ( Q ` j ) e. ( 1 ... N ) ) ) -> ( I ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( Q ` j ) ) = if ( I = I , if ( ( Q ` j ) = J , ( 1r ` R ) , ( 0g ` R ) ) , ( I M ( Q ` j ) ) ) )
77 67 68 69 68 75 76 syl122anc 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ -. j = N ) -> ( I ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( Q ` j ) ) = if ( I = I , if ( ( Q ` j ) = J , ( 1r ` R ) , ( 0g ` R ) ) , ( I M ( Q ` j ) ) ) )
78 55 a1i 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ -. j = N ) -> I = I )
79 78 iftrued 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ -. j = N ) -> if ( I = I , if ( ( Q ` j ) = J , ( 1r ` R ) , ( 0g ` R ) ) , ( I M ( Q ` j ) ) ) = if ( ( Q ` j ) = J , ( 1r ` R ) , ( 0g ` R ) ) )
80 simpr 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ ( Q ` j ) = J ) -> ( Q ` j ) = J )
81 80 fveq2d 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ ( Q ` j ) = J ) -> ( `' Q ` ( Q ` j ) ) = ( `' Q ` J ) )
82 72 13 symgbasf1o 
 |-  ( Q e. G -> Q : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
83 70 82 syl 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> Q : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
84 83 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ ( Q ` j ) = J ) -> Q : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
85 71 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ ( Q ` j ) = J ) -> j e. ( 1 ... N ) )
86 f1ocnvfv1 
 |-  ( ( Q : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( `' Q ` ( Q ` j ) ) = j )
87 84 85 86 syl2anc 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ ( Q ` j ) = J ) -> ( `' Q ` ( Q ` j ) ) = j )
88 20 fveq2d 
 |-  ( ph -> ( `' Q ` ( Q ` N ) ) = ( `' Q ` J ) )
89 18 82 syl 
 |-  ( ph -> Q : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
90 nnuz 
 |-  NN = ( ZZ>= ` 1 )
91 8 90 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
92 eluzfz2 
 |-  ( N e. ( ZZ>= ` 1 ) -> N e. ( 1 ... N ) )
93 91 92 syl 
 |-  ( ph -> N e. ( 1 ... N ) )
94 f1ocnvfv1 
 |-  ( ( Q : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ N e. ( 1 ... N ) ) -> ( `' Q ` ( Q ` N ) ) = N )
95 89 93 94 syl2anc 
 |-  ( ph -> ( `' Q ` ( Q ` N ) ) = N )
96 88 95 eqtr3d 
 |-  ( ph -> ( `' Q ` J ) = N )
97 96 3ad2ant1 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( `' Q ` J ) = N )
98 97 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ ( Q ` j ) = J ) -> ( `' Q ` J ) = N )
99 81 87 98 3eqtr3d 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ ( Q ` j ) = J ) -> j = N )
100 99 ex 
 |-  ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) -> ( ( Q ` j ) = J -> j = N ) )
101 100 con3d 
 |-  ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) -> ( -. j = N -> -. ( Q ` j ) = J ) )
102 101 imp 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ -. j = N ) -> -. ( Q ` j ) = J )
103 102 iffalsed 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ -. j = N ) -> if ( ( Q ` j ) = J , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) )
104 79 103 eqtrd 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ -. j = N ) -> if ( I = I , if ( ( Q ` j ) = J , ( 1r ` R ) , ( 0g ` R ) ) , ( I M ( Q ` j ) ) ) = ( 0g ` R ) )
105 66 77 104 3eqtrrd 
 |-  ( ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) /\ -. j = N ) -> ( 0g ` R ) = ( ( P ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( Q ` j ) ) )
106 61 105 ifeqda 
 |-  ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ i = N ) -> if ( j = N , ( 1r ` R ) , ( 0g ` R ) ) = ( ( P ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( Q ` j ) ) )
107 simp2 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> i e. ( 1 ... N ) )
108 107 adantr 
 |-  ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ -. i = N ) -> i e. ( 1 ... N ) )
109 71 adantr 
 |-  ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ -. i = N ) -> j e. ( 1 ... N ) )
110 ovexd 
 |-  ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ -. i = N ) -> ( ( P ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( Q ` j ) ) e. _V )
111 15 oveqi 
 |-  ( ( P ` i ) U ( Q ` j ) ) = ( ( P ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( Q ` j ) )
112 111 a1i 
 |-  ( ( i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( ( P ` i ) U ( Q ` j ) ) = ( ( P ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( Q ` j ) ) )
113 112 mpoeq3ia 
 |-  ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( ( P ` i ) U ( Q ` j ) ) ) = ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( ( P ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( Q ` j ) ) )
114 16 113 eqtri 
 |-  W = ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( ( P ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( Q ` j ) ) )
115 114 ovmpt4g 
 |-  ( ( i e. ( 1 ... N ) /\ j e. ( 1 ... N ) /\ ( ( P ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( Q ` j ) ) e. _V ) -> ( i W j ) = ( ( P ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( Q ` j ) ) )
116 108 109 110 115 syl3anc 
 |-  ( ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) /\ -. i = N ) -> ( i W j ) = ( ( P ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( Q ` j ) ) )
117 106 116 ifeqda 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> if ( i = N , if ( j = N , ( 1r ` R ) , ( 0g ` R ) ) , ( i W j ) ) = ( ( P ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( Q ` j ) ) )
118 117 mpoeq3dva 
 |-  ( ph -> ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> if ( i = N , if ( j = N , ( 1r ` R ) , ( 0g ` R ) ) , ( i W j ) ) ) = ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( ( P ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( Q ` j ) ) ) )
119 eqid 
 |-  ( Base ` R ) = ( Base ` R )
120 17 3ad2ant1 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> P e. G )
121 72 13 symgfv 
 |-  ( ( P e. G /\ i e. ( 1 ... N ) ) -> ( P ` i ) e. ( 1 ... N ) )
122 120 107 121 syl2anc 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( P ` i ) e. ( 1 ... N ) )
123 31 3ad2ant1 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> U e. B )
124 2 119 1 122 74 123 matecld 
 |-  ( ( ph /\ i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( ( P ` i ) U ( Q ` j ) ) e. ( Base ` R ) )
125 2 119 1 26 9 124 matbas2d 
 |-  ( ph -> ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( ( P ` i ) U ( Q ` j ) ) ) e. B )
126 16 125 eqeltrid 
 |-  ( ph -> W e. B )
127 119 51 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
128 28 127 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
129 eqid 
 |-  ( ( 1 ... N ) matRRep R ) = ( ( 1 ... N ) matRRep R )
130 2 1 129 52 marrepval 
 |-  ( ( ( W e. B /\ ( 1r ` R ) e. ( Base ` R ) ) /\ ( N e. ( 1 ... N ) /\ N e. ( 1 ... N ) ) ) -> ( N ( W ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) N ) = ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> if ( i = N , if ( j = N , ( 1r ` R ) , ( 0g ` R ) ) , ( i W j ) ) ) )
131 126 128 93 93 130 syl22anc 
 |-  ( ph -> ( N ( W ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) N ) = ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> if ( i = N , if ( j = N , ( 1r ` R ) , ( 0g ` R ) ) , ( i W j ) ) ) )
132 114 a1i 
 |-  ( ph -> W = ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( ( P ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( Q ` j ) ) ) )
133 118 131 132 3eqtr4d 
 |-  ( ph -> ( N ( W ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) N ) = W )
134 133 fveq2d 
 |-  ( ph -> ( D ` ( N ( W ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) N ) ) = ( D ` W ) )
135 eqid 
 |-  ( ( 1 ... N ) subMat R ) = ( ( 1 ... N ) subMat R )
136 2 135 1 submaval 
 |-  ( ( W e. B /\ N e. ( 1 ... N ) /\ N e. ( 1 ... N ) ) -> ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) = ( i e. ( ( 1 ... N ) \ { N } ) , j e. ( ( 1 ... N ) \ { N } ) |-> ( i W j ) ) )
137 126 93 93 136 syl3anc 
 |-  ( ph -> ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) = ( i e. ( ( 1 ... N ) \ { N } ) , j e. ( ( 1 ... N ) \ { N } ) |-> ( i W j ) ) )
138 fzdif2 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( ( 1 ... N ) \ { N } ) = ( 1 ... ( N - 1 ) ) )
139 91 138 syl 
 |-  ( ph -> ( ( 1 ... N ) \ { N } ) = ( 1 ... ( N - 1 ) ) )
140 mpoeq12 
 |-  ( ( ( ( 1 ... N ) \ { N } ) = ( 1 ... ( N - 1 ) ) /\ ( ( 1 ... N ) \ { N } ) = ( 1 ... ( N - 1 ) ) ) -> ( i e. ( ( 1 ... N ) \ { N } ) , j e. ( ( 1 ... N ) \ { N } ) |-> ( i W j ) ) = ( i e. ( 1 ... ( N - 1 ) ) , j e. ( 1 ... ( N - 1 ) ) |-> ( i W j ) ) )
141 139 139 140 syl2anc 
 |-  ( ph -> ( i e. ( ( 1 ... N ) \ { N } ) , j e. ( ( 1 ... N ) \ { N } ) |-> ( i W j ) ) = ( i e. ( 1 ... ( N - 1 ) ) , j e. ( 1 ... ( N - 1 ) ) |-> ( i W j ) ) )
142 137 141 eqtrd 
 |-  ( ph -> ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) = ( i e. ( 1 ... ( N - 1 ) ) , j e. ( 1 ... ( N - 1 ) ) |-> ( i W j ) ) )
143 difssd 
 |-  ( ph -> ( ( 1 ... N ) \ { N } ) C_ ( 1 ... N ) )
144 139 143 eqsstrrd 
 |-  ( ph -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
145 2 1 submabas 
 |-  ( ( W e. B /\ ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) ) -> ( i e. ( 1 ... ( N - 1 ) ) , j e. ( 1 ... ( N - 1 ) ) |-> ( i W j ) ) e. ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) )
146 126 144 145 syl2anc 
 |-  ( ph -> ( i e. ( 1 ... ( N - 1 ) ) , j e. ( 1 ... ( N - 1 ) ) |-> ( i W j ) ) e. ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) )
147 142 146 eqeltrd 
 |-  ( ph -> ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) e. ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) )
148 eqid 
 |-  ( ( 1 ... ( N - 1 ) ) Mat R ) = ( ( 1 ... ( N - 1 ) ) Mat R )
149 eqid 
 |-  ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) = ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) )
150 7 148 149 119 mdetcl 
 |-  ( ( R e. CRing /\ ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) e. ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) ) -> ( E ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) e. ( Base ` R ) )
151 9 147 150 syl2anc 
 |-  ( ph -> ( E ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) e. ( Base ` R ) )
152 119 5 51 ringlidm 
 |-  ( ( R e. Ring /\ ( E ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) e. ( Base ` R ) ) -> ( ( 1r ` R ) .x. ( E ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) ) = ( E ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) )
153 28 151 152 syl2anc 
 |-  ( ph -> ( ( 1r ` R ) .x. ( E ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) ) = ( E ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) )
154 2 fveq2i 
 |-  ( Base ` A ) = ( Base ` ( ( 1 ... N ) Mat R ) )
155 1 154 eqtri 
 |-  B = ( Base ` ( ( 1 ... N ) Mat R ) )
156 126 155 eleqtrdi 
 |-  ( ph -> W e. ( Base ` ( ( 1 ... N ) Mat R ) ) )
157 smadiadetr 
 |-  ( ( ( R e. CRing /\ W e. ( Base ` ( ( 1 ... N ) Mat R ) ) ) /\ ( N e. ( 1 ... N ) /\ ( 1r ` R ) e. ( Base ` R ) ) ) -> ( ( ( 1 ... N ) maDet R ) ` ( N ( W ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) N ) ) = ( ( 1r ` R ) ( .r ` R ) ( ( ( ( 1 ... N ) \ { N } ) maDet R ) ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) ) )
158 9 156 93 128 157 syl22anc 
 |-  ( ph -> ( ( ( 1 ... N ) maDet R ) ` ( N ( W ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) N ) ) = ( ( 1r ` R ) ( .r ` R ) ( ( ( ( 1 ... N ) \ { N } ) maDet R ) ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) ) )
159 3 fveq1i 
 |-  ( D ` ( N ( W ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) N ) ) = ( ( ( 1 ... N ) maDet R ) ` ( N ( W ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) N ) )
160 5 oveqi 
 |-  ( ( 1r ` R ) .x. ( ( ( ( 1 ... N ) \ { N } ) maDet R ) ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) ) = ( ( 1r ` R ) ( .r ` R ) ( ( ( ( 1 ... N ) \ { N } ) maDet R ) ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) )
161 159 160 eqeq12i 
 |-  ( ( D ` ( N ( W ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) N ) ) = ( ( 1r ` R ) .x. ( ( ( ( 1 ... N ) \ { N } ) maDet R ) ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) ) <-> ( ( ( 1 ... N ) maDet R ) ` ( N ( W ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) N ) ) = ( ( 1r ` R ) ( .r ` R ) ( ( ( ( 1 ... N ) \ { N } ) maDet R ) ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) ) )
162 158 161 sylibr 
 |-  ( ph -> ( D ` ( N ( W ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) N ) ) = ( ( 1r ` R ) .x. ( ( ( ( 1 ... N ) \ { N } ) maDet R ) ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) ) )
163 139 oveq1d 
 |-  ( ph -> ( ( ( 1 ... N ) \ { N } ) maDet R ) = ( ( 1 ... ( N - 1 ) ) maDet R ) )
164 163 7 eqtr4di 
 |-  ( ph -> ( ( ( 1 ... N ) \ { N } ) maDet R ) = E )
165 164 fveq1d 
 |-  ( ph -> ( ( ( ( 1 ... N ) \ { N } ) maDet R ) ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) = ( E ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) )
166 165 oveq2d 
 |-  ( ph -> ( ( 1r ` R ) .x. ( ( ( ( 1 ... N ) \ { N } ) maDet R ) ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) ) = ( ( 1r ` R ) .x. ( E ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) ) )
167 162 166 eqtrd 
 |-  ( ph -> ( D ` ( N ( W ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) N ) ) = ( ( 1r ` R ) .x. ( E ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) ) )
168 2 1 submat1n 
 |-  ( ( N e. NN /\ W e. B ) -> ( N ( subMat1 ` W ) N ) = ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) )
169 8 126 168 syl2anc 
 |-  ( ph -> ( N ( subMat1 ` W ) N ) = ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) )
170 169 fveq2d 
 |-  ( ph -> ( E ` ( N ( subMat1 ` W ) N ) ) = ( E ` ( N ( ( ( 1 ... N ) subMat R ) ` W ) N ) ) )
171 153 167 170 3eqtr4d 
 |-  ( ph -> ( D ` ( N ( W ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) N ) ) = ( E ` ( N ( subMat1 ` W ) N ) ) )
172 134 171 eqtr3d 
 |-  ( ph -> ( D ` W ) = ( E ` ( N ( subMat1 ` W ) N ) ) )
173 2 1 8 10 11 28 12 15 submatminr1 
 |-  ( ph -> ( I ( subMat1 ` M ) J ) = ( I ( subMat1 ` U ) J ) )
174 173 21 eqtrd 
 |-  ( ph -> ( I ( subMat1 ` M ) J ) = ( N ( subMat1 ` W ) N ) )
175 174 fveq2d 
 |-  ( ph -> ( E ` ( I ( subMat1 ` M ) J ) ) = ( E ` ( N ( subMat1 ` W ) N ) ) )
176 172 175 eqtr4d 
 |-  ( ph -> ( D ` W ) = ( E ` ( I ( subMat1 ` M ) J ) ) )
177 176 oveq2d 
 |-  ( ph -> ( ( Z ` ( ( S ` P ) x. ( S ` Q ) ) ) .x. ( D ` W ) ) = ( ( Z ` ( ( S ` P ) x. ( S ` Q ) ) ) .x. ( E ` ( I ( subMat1 ` M ) J ) ) ) )
178 25 32 177 3eqtrd 
 |-  ( ph -> ( J ( K ` M ) I ) = ( ( Z ` ( ( S ` P ) x. ( S ` Q ) ) ) .x. ( E ` ( I ( subMat1 ` M ) J ) ) ) )