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