Step | Hyp | Ref
| Expression |
1 | | eleq2 2690 |
. . . . . . . 8
|
2 | 1 | ifbid 4108 |
. . . . . . 7
|
3 | 2 | ifeq2d 4105 |
. . . . . 6
|
4 | 3 | mpt2eq3dv 6721 |
. . . . 5
|
5 | 4 | fveq2d 6195 |
. . . 4
|
6 | 5 | eqeq2d 2632 |
. . 3
|
7 | | eleq2 2690 |
. . . . . . . 8
|
8 | 7 | ifbid 4108 |
. . . . . . 7
|
9 | 8 | ifeq2d 4105 |
. . . . . 6
|
10 | 9 | mpt2eq3dv 6721 |
. . . . 5
|
11 | 10 | fveq2d 6195 |
. . . 4
|
12 | 11 | eqeq2d 2632 |
. . 3
|
13 | | eleq2 2690 |
. . . . . . . 8
|
14 | 13 | ifbid 4108 |
. . . . . . 7
|
15 | 14 | ifeq2d 4105 |
. . . . . 6
|
16 | 15 | mpt2eq3dv 6721 |
. . . . 5
|
17 | 16 | fveq2d 6195 |
. . . 4
|
18 | 17 | eqeq2d 2632 |
. . 3
|
19 | | eleq2 2690 |
. . . . . . . 8
|
20 | 19 | ifbid 4108 |
. . . . . . 7
|
21 | 20 | ifeq2d 4105 |
. . . . . 6
|
22 | 21 | mpt2eq3dv 6721 |
. . . . 5
|
23 | 22 | fveq2d 6195 |
. . . 4
|
24 | 23 | eqeq2d 2632 |
. . 3
|
25 | | madufval.a |
. . . . . 6
Mat |
26 | | madufval.d |
. . . . . 6
maDet |
27 | | madufval.j |
. . . . . 6
maAdju |
28 | | madufval.b |
. . . . . 6
|
29 | | madufval.o |
. . . . . 6
|
30 | | madufval.z |
. . . . . 6
|
31 | 25, 26, 27, 28, 29, 30 | maducoeval 20445 |
. . . . 5
|
32 | 31 | 3adant1l 1318 |
. . . 4
|
33 | | noel 3919 |
. . . . . . . 8
|
34 | | iffalse 4095 |
. . . . . . . 8
|
35 | 33, 34 | mp1i 13 |
. . . . . . 7
|
36 | 35 | ifeq2d 4105 |
. . . . . 6
|
37 | 36 | mpt2eq3ia 6720 |
. . . . 5
|
38 | 37 | fveq2i 6194 |
. . . 4
|
39 | 32, 38 | syl6eqr 2674 |
. . 3
|
40 | | eqid 2622 |
. . . . . . 7
|
41 | | eqid 2622 |
. . . . . . 7
|
42 | | eqid 2622 |
. . . . . . 7
|
43 | | simpl1l 1112 |
. . . . . . 7
|
44 | | simp1r 1086 |
. . . . . . . . 9
|
45 | 25, 28 | matrcl 20218 |
. . . . . . . . . 10
|
46 | 45 | simpld 475 |
. . . . . . . . 9
|
47 | 44, 46 | syl 17 |
. . . . . . . 8
|
48 | 47 | adantr 481 |
. . . . . . 7
|
49 | | simp1l 1085 |
. . . . . . . . . . 11
|
50 | 49 | ad2antrr 762 |
. . . . . . . . . 10
|
51 | | crngring 18558 |
. . . . . . . . . 10
|
52 | 50, 51 | syl 17 |
. . . . . . . . 9
|
53 | 40, 30 | ring0cl 18569 |
. . . . . . . . 9
|
54 | 52, 53 | syl 17 |
. . . . . . . 8
|
55 | | simpl1r 1113 |
. . . . . . . . . . 11
|
56 | 25, 40, 28 | matbas2i 20228 |
. . . . . . . . . . 11
|
57 | | elmapi 7879 |
. . . . . . . . . . 11
|
58 | 55, 56, 57 | 3syl 18 |
. . . . . . . . . 10
|
59 | 58 | adantr 481 |
. . . . . . . . 9
|
60 | | eldifi 3732 |
. . . . . . . . . . . 12
|
61 | 60 | ad2antll 765 |
. . . . . . . . . . 11
|
62 | 61 | eldifad 3586 |
. . . . . . . . . 10
|
63 | 62 | adantr 481 |
. . . . . . . . 9
|
64 | | simpr 477 |
. . . . . . . . 9
|
65 | 59, 63, 64 | fovrnd 6806 |
. . . . . . . 8
|
66 | 54, 65 | ifcld 4131 |
. . . . . . 7
|
67 | 40, 29 | ringidcl 18568 |
. . . . . . . . 9
|
68 | 52, 67 | syl 17 |
. . . . . . . 8
|
69 | 68, 54 | ifcld 4131 |
. . . . . . 7
|
70 | 54 | 3adant2 1080 |
. . . . . . . . 9
|
71 | 58 | fovrnda 6805 |
. . . . . . . . . 10
|
72 | 71 | 3impb 1260 |
. . . . . . . . 9
|
73 | 70, 72 | ifcld 4131 |
. . . . . . . 8
|
74 | 73, 72 | ifcld 4131 |
. . . . . . 7
|
75 | | simpl2 1065 |
. . . . . . . 8
|
76 | 58, 62, 75 | fovrnd 6806 |
. . . . . . 7
|
77 | | simpl3 1066 |
. . . . . . 7
|
78 | | eldifsni 4320 |
. . . . . . . 8
|
79 | 61, 78 | syl 17 |
. . . . . . 7
|
80 | 26, 40, 41, 42, 43, 48, 66, 69, 74, 76, 62, 77, 79 | mdetero 20416 |
. . . . . 6
|
81 | | ifnot 4133 |
. . . . . . . . . . . . . . . . 17
|
82 | 81 | eqcomi 2631 |
. . . . . . . . . . . . . . . 16
|
83 | 82 | a1i 11 |
. . . . . . . . . . . . . . 15
|
84 | | ovif2 6738 |
. . . . . . . . . . . . . . . 16
|
85 | 76 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
86 | 40, 42, 29 | ringridm 18572 |
. . . . . . . . . . . . . . . . . . . . 21
|
87 | 52, 85, 86 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
|
88 | 87 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
89 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
|
90 | 89 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
91 | 88, 90 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . 18
|
92 | 91 | ifeq1da 4116 |
. . . . . . . . . . . . . . . . 17
|
93 | 40, 42, 30 | ringrz 18588 |
. . . . . . . . . . . . . . . . . . 19
|
94 | 52, 85, 93 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
95 | 94 | ifeq2d 4105 |
. . . . . . . . . . . . . . . . 17
|
96 | 92, 95 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
97 | 84, 96 | syl5eq 2668 |
. . . . . . . . . . . . . . 15
|
98 | 83, 97 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
99 | | ringmnd 18556 |
. . . . . . . . . . . . . . . 16
|
100 | 52, 99 | syl 17 |
. . . . . . . . . . . . . . 15
|
101 | | id 22 |
. . . . . . . . . . . . . . . . 17
|
102 | | imnan 438 |
. . . . . . . . . . . . . . . . 17
|
103 | 101, 102 | mpbi 220 |
. . . . . . . . . . . . . . . 16
|
104 | 103 | a1i 11 |
. . . . . . . . . . . . . . 15
|
105 | 40, 30, 41 | mndifsplit 20442 |
. . . . . . . . . . . . . . 15
|
106 | 100, 65, 104, 105 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
107 | | pm2.1 433 |
. . . . . . . . . . . . . . 15
|
108 | | iftrue 4092 |
. . . . . . . . . . . . . . 15
|
109 | 107, 108 | mp1i 13 |
. . . . . . . . . . . . . 14
|
110 | 98, 106, 109 | 3eqtr2d 2662 |
. . . . . . . . . . . . 13
|
111 | 110 | 3adant2 1080 |
. . . . . . . . . . . 12
|
112 | | oveq1 6657 |
. . . . . . . . . . . . 13
|
113 | 112 | eqeq2d 2632 |
. . . . . . . . . . . 12
|
114 | 111, 113 | syl5ibrcom 237 |
. . . . . . . . . . 11
|
115 | 114 | imp 445 |
. . . . . . . . . 10
|
116 | | iftrue 4092 |
. . . . . . . . . . 11
|
117 | 116 | adantl 482 |
. . . . . . . . . 10
|
118 | 79 | neneqd 2799 |
. . . . . . . . . . . . . . 15
|
119 | 118 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
|
120 | | eqeq1 2626 |
. . . . . . . . . . . . . . 15
|
121 | 120 | notbid 308 |
. . . . . . . . . . . . . 14
|
122 | 119, 121 | syl5ibrcom 237 |
. . . . . . . . . . . . 13
|
123 | 122 | imp 445 |
. . . . . . . . . . . 12
|
124 | 123 | iffalsed 4097 |
. . . . . . . . . . 11
|
125 | | eldifn 3733 |
. . . . . . . . . . . . . . . 16
|
126 | 125 | ad2antll 765 |
. . . . . . . . . . . . . . 15
|
127 | 126 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
|
128 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
|
129 | 128 | notbid 308 |
. . . . . . . . . . . . . 14
|
130 | 127, 129 | syl5ibrcom 237 |
. . . . . . . . . . . . 13
|
131 | 130 | imp 445 |
. . . . . . . . . . . 12
|
132 | 131 | iffalsed 4097 |
. . . . . . . . . . 11
|
133 | 124, 132 | eqtrd 2656 |
. . . . . . . . . 10
|
134 | 115, 117,
133 | 3eqtr4d 2666 |
. . . . . . . . 9
|
135 | | iffalse 4095 |
. . . . . . . . . 10
|
136 | 135 | adantl 482 |
. . . . . . . . 9
|
137 | 134, 136 | pm2.61dan 832 |
. . . . . . . 8
|
138 | 137 | mpt2eq3dva 6719 |
. . . . . . 7
|
139 | 138 | fveq2d 6195 |
. . . . . 6
|
140 | | neeq2 2857 |
. . . . . . . . . . . . . . 15
|
141 | 140 | biimparc 504 |
. . . . . . . . . . . . . 14
|
142 | 141 | necomd 2849 |
. . . . . . . . . . . . 13
|
143 | 142 | neneqd 2799 |
. . . . . . . . . . . 12
|
144 | 143 | iffalsed 4097 |
. . . . . . . . . . 11
|
145 | | iftrue 4092 |
. . . . . . . . . . . . 13
|
146 | 145 | adantl 482 |
. . . . . . . . . . . 12
|
147 | 146 | ifeq2d 4105 |
. . . . . . . . . . 11
|
148 | | iftrue 4092 |
. . . . . . . . . . . 12
|
149 | 148 | adantl 482 |
. . . . . . . . . . 11
|
150 | 144, 147,
149 | 3eqtr4d 2666 |
. . . . . . . . . 10
|
151 | 112 | ifeq2d 4105 |
. . . . . . . . . . . . . 14
|
152 | | vsnid 4209 |
. . . . . . . . . . . . . . . . 17
|
153 | | elun2 3781 |
. . . . . . . . . . . . . . . . 17
|
154 | 152, 153 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
155 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
|
156 | 154, 155 | mpbiri 248 |
. . . . . . . . . . . . . . 15
|
157 | 156 | iftrued 4094 |
. . . . . . . . . . . . . 14
|
158 | | iftrue 4092 |
. . . . . . . . . . . . . 14
|
159 | 151, 157,
158 | 3eqtr4rd 2667 |
. . . . . . . . . . . . 13
|
160 | 159 | adantl 482 |
. . . . . . . . . . . 12
|
161 | | iffalse 4095 |
. . . . . . . . . . . . . 14
|
162 | | orc 400 |
. . . . . . . . . . . . . . . . 17
|
163 | | orel2 398 |
. . . . . . . . . . . . . . . . 17
|
164 | 162, 163 | impbid2 216 |
. . . . . . . . . . . . . . . 16
|
165 | | elun 3753 |
. . . . . . . . . . . . . . . . 17
|
166 | | velsn 4193 |
. . . . . . . . . . . . . . . . . 18
|
167 | 166 | orbi2i 541 |
. . . . . . . . . . . . . . . . 17
|
168 | 165, 167 | bitr2i 265 |
. . . . . . . . . . . . . . . 16
|
169 | 164, 168 | syl6bb 276 |
. . . . . . . . . . . . . . 15
|
170 | 169 | ifbid 4108 |
. . . . . . . . . . . . . 14
|
171 | 161, 170 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
172 | 171 | adantl 482 |
. . . . . . . . . . . 12
|
173 | 160, 172 | pm2.61dan 832 |
. . . . . . . . . . 11
|
174 | | iffalse 4095 |
. . . . . . . . . . . . 13
|
175 | 174 | ifeq2d 4105 |
. . . . . . . . . . . 12
|
176 | 175 | adantl 482 |
. . . . . . . . . . 11
|
177 | | iffalse 4095 |
. . . . . . . . . . . 12
|
178 | 177 | adantl 482 |
. . . . . . . . . . 11
|
179 | 173, 176,
178 | 3eqtr4d 2666 |
. . . . . . . . . 10
|
180 | 150, 179 | pm2.61dan 832 |
. . . . . . . . 9
|
181 | 180 | mpt2eq3dv 6721 |
. . . . . . . 8
|
182 | 181 | fveq2d 6195 |
. . . . . . 7
|
183 | 79, 182 | syl 17 |
. . . . . 6
|
184 | 80, 139, 183 | 3eqtr3d 2664 |
. . . . 5
|
185 | 184 | eqeq2d 2632 |
. . . 4
|
186 | 185 | biimpd 219 |
. . 3
|
187 | | difss 3737 |
. . . 4
|
188 | | ssfi 8180 |
. . . 4
|
189 | 47, 187, 188 | sylancl 694 |
. . 3
|
190 | 6, 12, 18, 24, 39, 186, 189 | findcard2d 8202 |
. 2
|
191 | | iba 524 |
. . . . . . . 8
|
192 | 191 | ifbid 4108 |
. . . . . . 7
|
193 | | iftrue 4092 |
. . . . . . 7
|
194 | | iftrue 4092 |
. . . . . . . 8
|
195 | 194 | orcs 409 |
. . . . . . 7
|
196 | 192, 193,
195 | 3eqtr4d 2666 |
. . . . . 6
|
197 | 196 | adantl 482 |
. . . . 5
|
198 | | iffalse 4095 |
. . . . . . 7
|
199 | 198 | adantl 482 |
. . . . . 6
|
200 | | id 22 |
. . . . . . . . . . 11
|
201 | 200 | neqned 2801 |
. . . . . . . . . 10
|
202 | 201 | anim2i 593 |
. . . . . . . . 9
|
203 | 202 | adantlr 751 |
. . . . . . . 8
|
204 | | eldifsn 4317 |
. . . . . . . 8
|
205 | 203, 204 | sylibr 224 |
. . . . . . 7
|
206 | 205 | iftrued 4094 |
. . . . . 6
|
207 | | biorf 420 |
. . . . . . . 8
|
208 | 200 | intnand 962 |
. . . . . . . . . 10
|
209 | 208 | iffalsed 4097 |
. . . . . . . . 9
|
210 | 209 | eqcomd 2628 |
. . . . . . . 8
|
211 | 207, 210 | ifbieq1d 4109 |
. . . . . . 7
|
212 | 211 | adantl 482 |
. . . . . 6
|
213 | 199, 206,
212 | 3eqtrd 2660 |
. . . . 5
|
214 | 197, 213 | pm2.61dan 832 |
. . . 4
|
215 | 214 | mpt2eq3ia 6720 |
. . 3
|
216 | 215 | fveq2i 6194 |
. 2
|
217 | 190, 216 | syl6eq 2672 |
1
|