Metamath Proof Explorer

Theorem madjusmdetlem4

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 )
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 ) ) )
Assertion madjusmdetlem4 
|- ( ph -> ( J ( K ` M ) I ) = ( ( Z ` ( -u 1 ^ ( I + J ) ) ) .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 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 eqid 
 |-  ( Base ` ( SymGrp ` ( 1 ... N ) ) ) = ( Base ` ( SymGrp ` ( 1 ... N ) ) )
18 eqid 
 |-  ( pmSgn ` ( 1 ... N ) ) = ( pmSgn ` ( 1 ... N ) )
19 eqid 
 |-  ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) = ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J )
20 fveq2 
 |-  ( k = i -> ( ( P o. `' S ) ` k ) = ( ( P o. `' S ) ` i ) )
21 20 oveq1d 
 |-  ( k = i -> ( ( ( P o. `' S ) ` k ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( ( Q o. `' T ) ` l ) ) = ( ( ( P o. `' S ) ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( ( Q o. `' T ) ` l ) ) )
22 fveq2 
 |-  ( l = j -> ( ( Q o. `' T ) ` l ) = ( ( Q o. `' T ) ` j ) )
23 22 oveq2d 
 |-  ( l = j -> ( ( ( P o. `' S ) ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( ( Q o. `' T ) ` l ) ) = ( ( ( P o. `' S ) ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( ( Q o. `' T ) ` j ) ) )
24 21 23 cbvmpov 
 |-  ( k e. ( 1 ... N ) , l e. ( 1 ... N ) |-> ( ( ( P o. `' S ) ` k ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( ( Q o. `' T ) ` l ) ) ) = ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( ( ( P o. `' S ) ` i ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( ( Q o. `' T ) ` j ) ) )
25 eqid 
 |-  ( 1 ... N ) = ( 1 ... N )
26 eqid 
 |-  ( SymGrp ` ( 1 ... N ) ) = ( SymGrp ` ( 1 ... N ) )
27 25 13 26 17 fzto1st 
 |-  ( I e. ( 1 ... N ) -> P e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
28 10 27 syl 
 |-  ( ph -> P e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
29 nnuz 
 |-  NN = ( ZZ>= ` 1 )
30 8 29 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
31 eluzfz2 
 |-  ( N e. ( ZZ>= ` 1 ) -> N e. ( 1 ... N ) )
32 30 31 syl 
 |-  ( ph -> N e. ( 1 ... N ) )
33 25 14 26 17 fzto1st 
 |-  ( N e. ( 1 ... N ) -> S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
34 32 33 syl 
 |-  ( ph -> S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
35 eqid 
 |-  ( invg ` ( SymGrp ` ( 1 ... N ) ) ) = ( invg ` ( SymGrp ` ( 1 ... N ) ) )
36 26 17 35 symginv 
 |-  ( S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) -> ( ( invg ` ( SymGrp ` ( 1 ... N ) ) ) ` S ) = `' S )
37 34 36 syl 
 |-  ( ph -> ( ( invg ` ( SymGrp ` ( 1 ... N ) ) ) ` S ) = `' S )
38 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
39 26 symggrp 
 |-  ( ( 1 ... N ) e. Fin -> ( SymGrp ` ( 1 ... N ) ) e. Grp )
40 38 39 syl 
 |-  ( ph -> ( SymGrp ` ( 1 ... N ) ) e. Grp )
41 17 35 grpinvcl 
 |-  ( ( ( SymGrp ` ( 1 ... N ) ) e. Grp /\ S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( ( invg ` ( SymGrp ` ( 1 ... N ) ) ) ` S ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
42 40 34 41 syl2anc 
 |-  ( ph -> ( ( invg ` ( SymGrp ` ( 1 ... N ) ) ) ` S ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
43 37 42 eqeltrrd 
 |-  ( ph -> `' S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
44 eqid 
 |-  ( +g ` ( SymGrp ` ( 1 ... N ) ) ) = ( +g ` ( SymGrp ` ( 1 ... N ) ) )
45 26 17 44 symgov 
 |-  ( ( P e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) /\ `' S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( P ( +g ` ( SymGrp ` ( 1 ... N ) ) ) `' S ) = ( P o. `' S ) )
46 26 17 44 symgcl 
 |-  ( ( P e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) /\ `' S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( P ( +g ` ( SymGrp ` ( 1 ... N ) ) ) `' S ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
47 45 46 eqeltrrd 
 |-  ( ( P e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) /\ `' S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( P o. `' S ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
48 28 43 47 syl2anc 
 |-  ( ph -> ( P o. `' S ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
49 25 15 26 17 fzto1st 
 |-  ( J e. ( 1 ... N ) -> Q e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
50 11 49 syl 
 |-  ( ph -> Q e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
51 25 16 26 17 fzto1st 
 |-  ( N e. ( 1 ... N ) -> T e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
52 32 51 syl 
 |-  ( ph -> T e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
53 26 17 35 symginv 
 |-  ( T e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) -> ( ( invg ` ( SymGrp ` ( 1 ... N ) ) ) ` T ) = `' T )
54 52 53 syl 
 |-  ( ph -> ( ( invg ` ( SymGrp ` ( 1 ... N ) ) ) ` T ) = `' T )
55 17 35 grpinvcl 
 |-  ( ( ( SymGrp ` ( 1 ... N ) ) e. Grp /\ T e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( ( invg ` ( SymGrp ` ( 1 ... N ) ) ) ` T ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
56 40 52 55 syl2anc 
 |-  ( ph -> ( ( invg ` ( SymGrp ` ( 1 ... N ) ) ) ` T ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
57 54 56 eqeltrrd 
 |-  ( ph -> `' T e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
58 26 17 44 symgov 
 |-  ( ( Q e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) /\ `' T e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( Q ( +g ` ( SymGrp ` ( 1 ... N ) ) ) `' T ) = ( Q o. `' T ) )
59 26 17 44 symgcl 
 |-  ( ( Q e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) /\ `' T e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( Q ( +g ` ( SymGrp ` ( 1 ... N ) ) ) `' T ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
60 58 59 eqeltrrd 
 |-  ( ( Q e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) /\ `' T e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( Q o. `' T ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
61 50 57 60 syl2anc 
 |-  ( ph -> ( Q o. `' T ) e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
62 26 17 symgbasf1o 
 |-  ( S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) -> S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
63 34 62 syl 
 |-  ( ph -> S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
64 f1of1 
 |-  ( S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> S : ( 1 ... N ) -1-1-> ( 1 ... N ) )
65 df-f1 
 |-  ( S : ( 1 ... N ) -1-1-> ( 1 ... N ) <-> ( S : ( 1 ... N ) --> ( 1 ... N ) /\ Fun `' S ) )
66 65 simprbi 
 |-  ( S : ( 1 ... N ) -1-1-> ( 1 ... N ) -> Fun `' S )
67 63 64 66 3syl 
 |-  ( ph -> Fun `' S )
68 f1ocnv 
 |-  ( S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> `' S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
69 f1odm 
 |-  ( `' S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> dom `' S = ( 1 ... N ) )
70 63 68 69 3syl 
 |-  ( ph -> dom `' S = ( 1 ... N ) )
71 32 70 eleqtrrd 
 |-  ( ph -> N e. dom `' S )
72 fvco 
 |-  ( ( Fun `' S /\ N e. dom `' S ) -> ( ( P o. `' S ) ` N ) = ( P ` ( `' S ` N ) ) )
73 67 71 72 syl2anc 
 |-  ( ph -> ( ( P o. `' S ) ` N ) = ( P ` ( `' S ` N ) ) )
74 25 14 26 17 fzto1stinvn 
 |-  ( N e. ( 1 ... N ) -> ( `' S ` N ) = 1 )
75 32 74 syl 
 |-  ( ph -> ( `' S ` N ) = 1 )
76 75 fveq2d 
 |-  ( ph -> ( P ` ( `' S ` N ) ) = ( P ` 1 ) )
77 25 13 fzto1stfv1 
 |-  ( I e. ( 1 ... N ) -> ( P ` 1 ) = I )
78 10 77 syl 
 |-  ( ph -> ( P ` 1 ) = I )
79 73 76 78 3eqtrd 
 |-  ( ph -> ( ( P o. `' S ) ` N ) = I )
80 26 17 symgbasf1o 
 |-  ( T e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) -> T : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
81 52 80 syl 
 |-  ( ph -> T : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
82 f1of1 
 |-  ( T : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> T : ( 1 ... N ) -1-1-> ( 1 ... N ) )
83 df-f1 
 |-  ( T : ( 1 ... N ) -1-1-> ( 1 ... N ) <-> ( T : ( 1 ... N ) --> ( 1 ... N ) /\ Fun `' T ) )
84 83 simprbi 
 |-  ( T : ( 1 ... N ) -1-1-> ( 1 ... N ) -> Fun `' T )
85 81 82 84 3syl 
 |-  ( ph -> Fun `' T )
86 f1ocnv 
 |-  ( T : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> `' T : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
87 f1odm 
 |-  ( `' T : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> dom `' T = ( 1 ... N ) )
88 81 86 87 3syl 
 |-  ( ph -> dom `' T = ( 1 ... N ) )
89 32 88 eleqtrrd 
 |-  ( ph -> N e. dom `' T )
90 fvco 
 |-  ( ( Fun `' T /\ N e. dom `' T ) -> ( ( Q o. `' T ) ` N ) = ( Q ` ( `' T ` N ) ) )
91 85 89 90 syl2anc 
 |-  ( ph -> ( ( Q o. `' T ) ` N ) = ( Q ` ( `' T ` N ) ) )
92 25 16 26 17 fzto1stinvn 
 |-  ( N e. ( 1 ... N ) -> ( `' T ` N ) = 1 )
93 32 92 syl 
 |-  ( ph -> ( `' T ` N ) = 1 )
94 93 fveq2d 
 |-  ( ph -> ( Q ` ( `' T ` N ) ) = ( Q ` 1 ) )
95 25 15 fzto1stfv1 
 |-  ( J e. ( 1 ... N ) -> ( Q ` 1 ) = J )
96 11 95 syl 
 |-  ( ph -> ( Q ` 1 ) = J )
97 91 94 96 3eqtrd 
 |-  ( ph -> ( ( Q o. `' T ) ` N ) = J )
98 crngring 
 |-  ( R e. CRing -> R e. Ring )
99 9 98 syl 
 |-  ( ph -> R e. Ring )
100 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 )
101 99 12 10 11 100 syl22anc 
 |-  ( ph -> ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) e. B )
102 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 24 101 madjusmdetlem3 
 |-  ( ph -> ( I ( subMat1 ` ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ) J ) = ( N ( subMat1 ` ( k e. ( 1 ... N ) , l e. ( 1 ... N ) |-> ( ( ( P o. `' S ) ` k ) ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) ( ( Q o. `' T ) ` l ) ) ) ) N ) )
103 1 2 3 4 5 6 7 8 9 10 11 12 17 18 19 24 48 61 79 97 102 madjusmdetlem1 
 |-  ( ph -> ( J ( K ` M ) I ) = ( ( Z ` ( ( ( pmSgn ` ( 1 ... N ) ) ` ( P o. `' S ) ) x. ( ( pmSgn ` ( 1 ... N ) ) ` ( Q o. `' T ) ) ) ) .x. ( E ` ( I ( subMat1 ` M ) J ) ) ) )
104 26 18 17 psgnco 
 |-  ( ( ( 1 ... N ) e. Fin /\ P e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) /\ `' S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( ( pmSgn ` ( 1 ... N ) ) ` ( P o. `' S ) ) = ( ( ( pmSgn ` ( 1 ... N ) ) ` P ) x. ( ( pmSgn ` ( 1 ... N ) ) ` `' S ) ) )
105 38 28 43 104 syl3anc 
 |-  ( ph -> ( ( pmSgn ` ( 1 ... N ) ) ` ( P o. `' S ) ) = ( ( ( pmSgn ` ( 1 ... N ) ) ` P ) x. ( ( pmSgn ` ( 1 ... N ) ) ` `' S ) ) )
106 25 13 26 17 18 psgnfzto1st 
 |-  ( I e. ( 1 ... N ) -> ( ( pmSgn ` ( 1 ... N ) ) ` P ) = ( -u 1 ^ ( I + 1 ) ) )
107 10 106 syl 
 |-  ( ph -> ( ( pmSgn ` ( 1 ... N ) ) ` P ) = ( -u 1 ^ ( I + 1 ) ) )
108 26 18 17 psgninv 
 |-  ( ( ( 1 ... N ) e. Fin /\ S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( ( pmSgn ` ( 1 ... N ) ) ` `' S ) = ( ( pmSgn ` ( 1 ... N ) ) ` S ) )
109 38 34 108 syl2anc 
 |-  ( ph -> ( ( pmSgn ` ( 1 ... N ) ) ` `' S ) = ( ( pmSgn ` ( 1 ... N ) ) ` S ) )
110 25 14 26 17 18 psgnfzto1st 
 |-  ( N e. ( 1 ... N ) -> ( ( pmSgn ` ( 1 ... N ) ) ` S ) = ( -u 1 ^ ( N + 1 ) ) )
111 32 110 syl 
 |-  ( ph -> ( ( pmSgn ` ( 1 ... N ) ) ` S ) = ( -u 1 ^ ( N + 1 ) ) )
112 109 111 eqtrd 
 |-  ( ph -> ( ( pmSgn ` ( 1 ... N ) ) ` `' S ) = ( -u 1 ^ ( N + 1 ) ) )
113 107 112 oveq12d 
 |-  ( ph -> ( ( ( pmSgn ` ( 1 ... N ) ) ` P ) x. ( ( pmSgn ` ( 1 ... N ) ) ` `' S ) ) = ( ( -u 1 ^ ( I + 1 ) ) x. ( -u 1 ^ ( N + 1 ) ) ) )
114 105 113 eqtrd 
 |-  ( ph -> ( ( pmSgn ` ( 1 ... N ) ) ` ( P o. `' S ) ) = ( ( -u 1 ^ ( I + 1 ) ) x. ( -u 1 ^ ( N + 1 ) ) ) )
115 26 18 17 psgnco 
 |-  ( ( ( 1 ... N ) e. Fin /\ Q e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) /\ `' T e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( ( pmSgn ` ( 1 ... N ) ) ` ( Q o. `' T ) ) = ( ( ( pmSgn ` ( 1 ... N ) ) ` Q ) x. ( ( pmSgn ` ( 1 ... N ) ) ` `' T ) ) )
116 38 50 57 115 syl3anc 
 |-  ( ph -> ( ( pmSgn ` ( 1 ... N ) ) ` ( Q o. `' T ) ) = ( ( ( pmSgn ` ( 1 ... N ) ) ` Q ) x. ( ( pmSgn ` ( 1 ... N ) ) ` `' T ) ) )
117 25 15 26 17 18 psgnfzto1st 
 |-  ( J e. ( 1 ... N ) -> ( ( pmSgn ` ( 1 ... N ) ) ` Q ) = ( -u 1 ^ ( J + 1 ) ) )
118 11 117 syl 
 |-  ( ph -> ( ( pmSgn ` ( 1 ... N ) ) ` Q ) = ( -u 1 ^ ( J + 1 ) ) )
119 26 18 17 psgninv 
 |-  ( ( ( 1 ... N ) e. Fin /\ T e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) ) -> ( ( pmSgn ` ( 1 ... N ) ) ` `' T ) = ( ( pmSgn ` ( 1 ... N ) ) ` T ) )
120 38 52 119 syl2anc 
 |-  ( ph -> ( ( pmSgn ` ( 1 ... N ) ) ` `' T ) = ( ( pmSgn ` ( 1 ... N ) ) ` T ) )
121 25 16 26 17 18 psgnfzto1st 
 |-  ( N e. ( 1 ... N ) -> ( ( pmSgn ` ( 1 ... N ) ) ` T ) = ( -u 1 ^ ( N + 1 ) ) )
122 32 121 syl 
 |-  ( ph -> ( ( pmSgn ` ( 1 ... N ) ) ` T ) = ( -u 1 ^ ( N + 1 ) ) )
123 120 122 eqtrd 
 |-  ( ph -> ( ( pmSgn ` ( 1 ... N ) ) ` `' T ) = ( -u 1 ^ ( N + 1 ) ) )
124 118 123 oveq12d 
 |-  ( ph -> ( ( ( pmSgn ` ( 1 ... N ) ) ` Q ) x. ( ( pmSgn ` ( 1 ... N ) ) ` `' T ) ) = ( ( -u 1 ^ ( J + 1 ) ) x. ( -u 1 ^ ( N + 1 ) ) ) )
125 116 124 eqtrd 
 |-  ( ph -> ( ( pmSgn ` ( 1 ... N ) ) ` ( Q o. `' T ) ) = ( ( -u 1 ^ ( J + 1 ) ) x. ( -u 1 ^ ( N + 1 ) ) ) )
126 114 125 oveq12d 
 |-  ( ph -> ( ( ( pmSgn ` ( 1 ... N ) ) ` ( P o. `' S ) ) x. ( ( pmSgn ` ( 1 ... N ) ) ` ( Q o. `' T ) ) ) = ( ( ( -u 1 ^ ( I + 1 ) ) x. ( -u 1 ^ ( N + 1 ) ) ) x. ( ( -u 1 ^ ( J + 1 ) ) x. ( -u 1 ^ ( N + 1 ) ) ) ) )
127 1cnd 
 |-  ( ph -> 1 e. CC )
128 127 negcld 
 |-  ( ph -> -u 1 e. CC )
129 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
130 129 10 sselid 
 |-  ( ph -> I e. NN )
131 130 nnnn0d 
 |-  ( ph -> I e. NN0 )
132 1nn0 
 |-  1 e. NN0
133 132 a1i 
 |-  ( ph -> 1 e. NN0 )
134 131 133 nn0addcld 
 |-  ( ph -> ( I + 1 ) e. NN0 )
135 128 134 expcld 
 |-  ( ph -> ( -u 1 ^ ( I + 1 ) ) e. CC )
136 8 nnnn0d 
 |-  ( ph -> N e. NN0 )
137 136 133 nn0addcld 
 |-  ( ph -> ( N + 1 ) e. NN0 )
138 128 137 expcld 
 |-  ( ph -> ( -u 1 ^ ( N + 1 ) ) e. CC )
139 129 11 sselid 
 |-  ( ph -> J e. NN )
140 139 nnnn0d 
 |-  ( ph -> J e. NN0 )
141 140 133 nn0addcld 
 |-  ( ph -> ( J + 1 ) e. NN0 )
142 128 141 expcld 
 |-  ( ph -> ( -u 1 ^ ( J + 1 ) ) e. CC )
143 135 138 142 138 mul4d 
 |-  ( ph -> ( ( ( -u 1 ^ ( I + 1 ) ) x. ( -u 1 ^ ( N + 1 ) ) ) x. ( ( -u 1 ^ ( J + 1 ) ) x. ( -u 1 ^ ( N + 1 ) ) ) ) = ( ( ( -u 1 ^ ( I + 1 ) ) x. ( -u 1 ^ ( J + 1 ) ) ) x. ( ( -u 1 ^ ( N + 1 ) ) x. ( -u 1 ^ ( N + 1 ) ) ) ) )
144 128 141 134 expaddd 
 |-  ( ph -> ( -u 1 ^ ( ( I + 1 ) + ( J + 1 ) ) ) = ( ( -u 1 ^ ( I + 1 ) ) x. ( -u 1 ^ ( J + 1 ) ) ) )
145 130 nncnd 
 |-  ( ph -> I e. CC )
146 139 nncnd 
 |-  ( ph -> J e. CC )
147 145 127 146 127 add4d 
 |-  ( ph -> ( ( I + 1 ) + ( J + 1 ) ) = ( ( I + J ) + ( 1 + 1 ) ) )
148 1p1e2 
 |-  ( 1 + 1 ) = 2
149 148 oveq2i 
 |-  ( ( I + J ) + ( 1 + 1 ) ) = ( ( I + J ) + 2 )
150 147 149 eqtrdi 
 |-  ( ph -> ( ( I + 1 ) + ( J + 1 ) ) = ( ( I + J ) + 2 ) )
151 150 oveq2d 
 |-  ( ph -> ( -u 1 ^ ( ( I + 1 ) + ( J + 1 ) ) ) = ( -u 1 ^ ( ( I + J ) + 2 ) ) )
152 2nn0 
 |-  2 e. NN0
153 152 a1i 
 |-  ( ph -> 2 e. NN0 )
154 131 140 nn0addcld 
 |-  ( ph -> ( I + J ) e. NN0 )
155 128 153 154 expaddd 
 |-  ( ph -> ( -u 1 ^ ( ( I + J ) + 2 ) ) = ( ( -u 1 ^ ( I + J ) ) x. ( -u 1 ^ 2 ) ) )
156 neg1sqe1 
 |-  ( -u 1 ^ 2 ) = 1
157 156 oveq2i 
 |-  ( ( -u 1 ^ ( I + J ) ) x. ( -u 1 ^ 2 ) ) = ( ( -u 1 ^ ( I + J ) ) x. 1 )
158 155 157 eqtrdi 
 |-  ( ph -> ( -u 1 ^ ( ( I + J ) + 2 ) ) = ( ( -u 1 ^ ( I + J ) ) x. 1 ) )
159 128 154 expcld 
 |-  ( ph -> ( -u 1 ^ ( I + J ) ) e. CC )
160 159 mulid1d 
 |-  ( ph -> ( ( -u 1 ^ ( I + J ) ) x. 1 ) = ( -u 1 ^ ( I + J ) ) )
161 151 158 160 3eqtrd 
 |-  ( ph -> ( -u 1 ^ ( ( I + 1 ) + ( J + 1 ) ) ) = ( -u 1 ^ ( I + J ) ) )
162 144 161 eqtr3d 
 |-  ( ph -> ( ( -u 1 ^ ( I + 1 ) ) x. ( -u 1 ^ ( J + 1 ) ) ) = ( -u 1 ^ ( I + J ) ) )
163 137 nn0zd 
 |-  ( ph -> ( N + 1 ) e. ZZ )
164 m1expcl2 
 |-  ( ( N + 1 ) e. ZZ -> ( -u 1 ^ ( N + 1 ) ) e. { -u 1 , 1 } )
165 1neg1t1neg1 
 |-  ( ( -u 1 ^ ( N + 1 ) ) e. { -u 1 , 1 } -> ( ( -u 1 ^ ( N + 1 ) ) x. ( -u 1 ^ ( N + 1 ) ) ) = 1 )
166 163 164 165 3syl 
 |-  ( ph -> ( ( -u 1 ^ ( N + 1 ) ) x. ( -u 1 ^ ( N + 1 ) ) ) = 1 )
167 162 166 oveq12d 
 |-  ( ph -> ( ( ( -u 1 ^ ( I + 1 ) ) x. ( -u 1 ^ ( J + 1 ) ) ) x. ( ( -u 1 ^ ( N + 1 ) ) x. ( -u 1 ^ ( N + 1 ) ) ) ) = ( ( -u 1 ^ ( I + J ) ) x. 1 ) )
168 143 167 160 3eqtrd 
 |-  ( ph -> ( ( ( -u 1 ^ ( I + 1 ) ) x. ( -u 1 ^ ( N + 1 ) ) ) x. ( ( -u 1 ^ ( J + 1 ) ) x. ( -u 1 ^ ( N + 1 ) ) ) ) = ( -u 1 ^ ( I + J ) ) )
169 126 168 eqtrd 
 |-  ( ph -> ( ( ( pmSgn ` ( 1 ... N ) ) ` ( P o. `' S ) ) x. ( ( pmSgn ` ( 1 ... N ) ) ` ( Q o. `' T ) ) ) = ( -u 1 ^ ( I + J ) ) )
170 169 fveq2d 
 |-  ( ph -> ( Z ` ( ( ( pmSgn ` ( 1 ... N ) ) ` ( P o. `' S ) ) x. ( ( pmSgn ` ( 1 ... N ) ) ` ( Q o. `' T ) ) ) ) = ( Z ` ( -u 1 ^ ( I + J ) ) ) )
171 170 oveq1d 
 |-  ( ph -> ( ( Z ` ( ( ( pmSgn ` ( 1 ... N ) ) ` ( P o. `' S ) ) x. ( ( pmSgn ` ( 1 ... N ) ) ` ( Q o. `' T ) ) ) ) .x. ( E ` ( I ( subMat1 ` M ) J ) ) ) = ( ( Z ` ( -u 1 ^ ( I + J ) ) ) .x. ( E ` ( I ( subMat1 ` M ) J ) ) ) )
172 103 171 eqtrd 
 |-  ( ph -> ( J ( K ` M ) I ) = ( ( Z ` ( -u 1 ^ ( I + J ) ) ) .x. ( E ` ( I ( subMat1 ` M ) J ) ) ) )