Step | Hyp | Ref
| Expression |
1 | | mdetmul.a |
. . 3
 Mat   |
2 | | mdetmul.b |
. . 3
     |
3 | | eqid 2452 |
. . 3
         |
4 | | eqid 2452 |
. . 3
         |
5 | | eqid 2452 |
. . 3
         |
6 | | eqid 2452 |
. . 3
       |
7 | | mdetmul.t1 |
. . 3
     |
8 | 1, 2 | matrcl 19448 |
. . . . 5
 
   |
9 | 8 | simpld 465 |
. . . 4
   |
10 | 9 | 3ad2ant2 1031 |
. . 3
 
   |
11 | | crngring 17802 |
. . . 4

  |
12 | 11 | 3ad2ant1 1030 |
. . 3
 
   |
13 | | mdetmul.d |
. . . . . . . 8
 maDet   |
14 | 13, 1, 2, 3 | mdetf 19631 |
. . . . . . 7

          |
15 | 14 | 3ad2ant1 1030 |
. . . . . 6
 
           |
16 | 15 | adantr 471 |
. . . . 5
  


          |
17 | 1 | matring 19479 |
. . . . . . . 8
 

  |
18 | 10, 12, 17 | syl2anc 671 |
. . . . . . 7
 
   |
19 | 18 | adantr 471 |
. . . . . 6
  


  |
20 | | simpr 467 |
. . . . . 6
  


  |
21 | | simpl3 1014 |
. . . . . 6
  


  |
22 | | mdetmul.t2 |
. . . . . . 7
     |
23 | 2, 22 | ringcl 17805 |
. . . . . 6
 
 
   |
24 | 19, 20, 21, 23 | syl3anc 1271 |
. . . . 5
  


    |
25 | 16, 24 | ffvelrnd 6007 |
. . . 4
  


            |
26 | | eqid 2452 |
. . . 4
                 |
27 | 25, 26 | fmptd 6030 |
. . 3
 
                   |
28 | | simp21 1042 |
. . . . . . 7
  
 



            |
29 | | oveq1 6283 |
. . . . . . . . 9
 
     |
30 | 29 | fveq2d 5852 |
. . . . . . . 8
          
    |
31 | | fvex 5858 |
. . . . . . . 8
       |
32 | 30, 26, 31 | fvmpt 5932 |
. . . . . . 7
      
              |
33 | 28, 32 | syl 17 |
. . . . . 6
  
 



                              |
34 | | simp11 1039 |
. . . . . . 7
  
 



         
  |
35 | 18 | adantr 471 |
. . . . . . . . 9
  
 
    |
36 | | simpr1 1015 |
. . . . . . . . 9
  
 
    |
37 | | simpl3 1014 |
. . . . . . . . 9
  
 
    |
38 | 2, 22 | ringcl 17805 |
. . . . . . . . 9
 
 
   |
39 | 35, 36, 37, 38 | syl3anc 1271 |
. . . . . . . 8
  
 
  
   |
40 | 39 | 3adant3 1029 |
. . . . . . 7
  
 



              |
41 | | simp22 1043 |
. . . . . . 7
  
 



            |
42 | | simp23 1044 |
. . . . . . 7
  
 



            |
43 | | simp3l 1037 |
. . . . . . 7
  
 



            |
44 | | simpl3r 1065 |
. . . . . . . . . 10
   


             

          |
45 | | eqid 2452 |
. . . . . . . . . . . 12
 |
46 | | oveq1 6283 |
. . . . . . . . . . . . 13
                               |
47 | 46 | ralimi 2777 |
. . . . . . . . . . . 12
 
        
                      |
48 | | mpteq12 4454 |
. . . . . . . . . . . 12
                                                  |
49 | 45, 47, 48 | sylancr 674 |
. . . . . . . . . . 11
 
                                  |
50 | 49 | oveq2d 6292 |
. . . . . . . . . 10
 
         g               g                |
51 | 44, 50 | syl 17 |
. . . . . . . . 9
   


             
 g               g                |
52 | | simp1 1009 |
. . . . . . . . . . . . . . 15
 
   |
53 | | eqid 2452 |
. . . . . . . . . . . . . . . . 17
 maMul       maMul       |
54 | 1, 53 | matmulr 19474 |
. . . . . . . . . . . . . . . 16
 
  maMul
  
        |
55 | 54, 22 | syl6eqr 2504 |
. . . . . . . . . . . . . . 15
 
  maMul
  
 
 |
56 | 10, 52, 55 | syl2anc 671 |
. . . . . . . . . . . . . 14
 
  maMul       |
57 | 56 | ad2antrr 737 |
. . . . . . . . . . . . 13
   


 
  maMul   
 
 |
58 | 57 | oveqd 6293 |
. . . . . . . . . . . 12
   


 
    maMul            |
59 | 58 | oveqd 6293 |
. . . . . . . . . . 11
   


 
      maMul   
        
     |
60 | | simpll1 1048 |
. . . . . . . . . . . 12
   


 
   |
61 | 10 | ad2antrr 737 |
. . . . . . . . . . . 12
   


 
   |
62 | | simplr1 1051 |
. . . . . . . . . . . . 13
   


 
   |
63 | 1, 3, 2 | matbas2i 19458 |
. . . . . . . . . . . . 13
     
     |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . 12
   


 
           |
65 | 1, 3, 2 | matbas2i 19458 |
. . . . . . . . . . . . . 14
     
     |
66 | 65 | 3ad2ant3 1032 |
. . . . . . . . . . . . 13
 
     
     |
67 | 66 | ad2antrr 737 |
. . . . . . . . . . . 12
   


 
           |
68 | | simplr2 1052 |
. . . . . . . . . . . 12
   


 
   |
69 | | simpr 467 |
. . . . . . . . . . . 12
   


 
   |
70 | 53, 3, 7, 60, 61, 61, 61, 64, 67, 68, 69 | mamufv 19423 |
. . . . . . . . . . 11
   


 
      maMul   
       g                |
71 | 59, 70 | eqtr3d 2488 |
. . . . . . . . . 10
   


 
        g                |
72 | 71 | 3adantl3 1167 |
. . . . . . . . 9
   


             
       g                |
73 | 58 | oveqd 6293 |
. . . . . . . . . . 11
   


 
      maMul   
        
     |
74 | | simplr3 1053 |
. . . . . . . . . . . 12
   


 
   |
75 | 53, 3, 7, 60, 61, 61, 61, 64, 67, 74, 69 | mamufv 19423 |
. . . . . . . . . . 11
   


 
      maMul   
       g                |
76 | 73, 75 | eqtr3d 2488 |
. . . . . . . . . 10
   


 
        g                |
77 | 76 | 3adantl3 1167 |
. . . . . . . . 9
   


             
       g                |
78 | 51, 72, 77 | 3eqtr4d 2496 |
. . . . . . . 8
   


             
              |
79 | 78 | ralrimiva 2790 |
. . . . . . 7
  
 



          
              |
80 | 13, 1, 2, 4, 34, 40, 41, 42, 43, 79 | mdetralt 19644 |
. . . . . 6
  
 



             
        |
81 | 33, 80 | eqtrd 2486 |
. . . . 5
  
 



                            |
82 | 81 | 3expia 1212 |
. . . 4
  
 
                                 |
83 | 82 | ralrimivvva 2796 |
. . 3
 
 


                               |
84 | | simp11 1039 |
. . . . . . . . 9
  
    
 
        
                                                      |
85 | 18 | adantr 471 |
. . . . . . . . . . 11
  
    
     |
86 | | simprll 777 |
. . . . . . . . . . 11
  
    
     |
87 | | simpl3 1014 |
. . . . . . . . . . 11
  
    
     |
88 | 85, 86, 87, 38 | syl3anc 1271 |
. . . . . . . . . 10
  
    
   
   |
89 | 88 | 3adant3 1029 |
. . . . . . . . 9
  
    
 
        
                                                    
   |
90 | | simprlr 778 |
. . . . . . . . . . 11
  
    
     |
91 | 2, 22 | ringcl 17805 |
. . . . . . . . . . 11
 
 
   |
92 | 85, 90, 87, 91 | syl3anc 1271 |
. . . . . . . . . 10
  
    
   
   |
93 | 92 | 3adant3 1029 |
. . . . . . . . 9
  
    
 
        
                                                    
   |
94 | | simprrl 779 |
. . . . . . . . . . 11
  
    
     |
95 | 2, 22 | ringcl 17805 |
. . . . . . . . . . 11
 
 
   |
96 | 85, 94, 87, 95 | syl3anc 1271 |
. . . . . . . . . 10
  
    
   
   |
97 | 96 | 3adant3 1029 |
. . . . . . . . 9
  
    
 
        
                                                    
   |
98 | | simp2rr 1079 |
. . . . . . . . 9
  
    
 
        
                                                      |
99 | | simp31 1045 |
. . . . . . . . . . . 12
  
    
 
        
                                                           
                    |
100 | 99 | oveq1d 6291 |
. . . . . . . . . . 11
  
    
 
        
                                                             maMul                                 maMul            |
101 | 12 | adantr 471 |
. . . . . . . . . . . . 13
  
    
     |
102 | | eqid 2452 |
. . . . . . . . . . . . 13
 maMul     
   maMul         |
103 | | snfi 7637 |
. . . . . . . . . . . . . 14
   |
104 | 103 | a1i 11 |
. . . . . . . . . . . . 13
  
    
       |
105 | 10 | adantr 471 |
. . . . . . . . . . . . 13
  
    
     |
106 | 1, 3, 2 | matbas2i 19458 |
. . . . . . . . . . . . . . 15
     
     |
107 | 90, 106 | syl 17 |
. . . . . . . . . . . . . 14
  
    
       
     |
108 | | simprrr 780 |
. . . . . . . . . . . . . . . 16
  
    
     |
109 | 108 | snssd 4086 |
. . . . . . . . . . . . . . 15
  
    
    
  |
110 | | xpss1 4921 |
. . . . . . . . . . . . . . 15
       
   |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . 14
  
    
           |
112 | | elmapssres 7483 |
. . . . . . . . . . . . . 14
                           
       |
113 | 107, 111,
112 | syl2anc 671 |
. . . . . . . . . . . . 13
  
    
                     |
114 | 1, 3, 2 | matbas2i 19458 |
. . . . . . . . . . . . . . 15
     
     |
115 | 94, 114 | syl 17 |
. . . . . . . . . . . . . 14
  
    
       
     |
116 | | elmapssres 7483 |
. . . . . . . . . . . . . 14
                           
       |
117 | 115, 111,
116 | syl2anc 671 |
. . . . . . . . . . . . 13
  
    
                     |
118 | 66 | adantr 471 |
. . . . . . . . . . . . 13
  
    
       
     |
119 | 3, 101, 102, 104, 105, 105, 6, 113, 117, 118 | mamudi 19439 |
. . . . . . . . . . . 12
  
    
                          maMul            
       maMul     
                   maMul             |
120 | 119 | 3adant3 1029 |
. . . . . . . . . . 11
  
    
 
        
                                                                           maMul            
       maMul     
                   maMul             |
121 | 100, 120 | eqtrd 2486 |
. . . . . . . . . 10
  
    
 
        
                                                             maMul                    maMul                 
       maMul     
       |
122 | 56 | adantr 471 |
. . . . . . . . . . . . . 14
  
    
    maMul       |
123 | 122 | oveqd 6293 |
. . . . . . . . . . . . 13
  
    
      maMul   
    
   |
124 | 123 | reseq1d 5082 |
. . . . . . . . . . . 12
  
    
       maMul                       |
125 | | simpl1 1012 |
. . . . . . . . . . . . 13
  
    
     |
126 | 86, 63 | syl 17 |
. . . . . . . . . . . . 13
  
    
       
     |
127 | 53, 102, 3, 125, 105, 105, 105, 109, 126, 118 | mamures 19426 |
. . . . . . . . . . . 12
  
    
       maMul                      maMul            |
128 | 124, 127 | eqtr3d 2488 |
. . . . . . . . . . 11
  
    
            
       maMul     
      |
129 | 128 | 3adant3 1029 |
. . . . . . . . . 10
  
    
 
        
                                                             
       maMul     
      |
130 | 122 | oveqd 6293 |
. . . . . . . . . . . . . 14
  
    
      maMul   
    
   |
131 | 130 | reseq1d 5082 |
. . . . . . . . . . . . 13
  
    
       maMul                       |
132 | 53, 102, 3, 125, 105, 105, 105, 109, 107, 118 | mamures 19426 |
. . . . . . . . . . . . 13
  
    
       maMul                      maMul            |
133 | 131, 132 | eqtr3d 2488 |
. . . . . . . . . . . 12
  
    
            
       maMul     
      |
134 | 122 | oveqd 6293 |
. . . . . . . . . . . . . 14
  
    
      maMul   
    
   |
135 | 134 | reseq1d 5082 |
. . . . . . . . . . . . 13
  
    
       maMul                       |
136 | 53, 102, 3, 125, 105, 105, 105, 109, 115, 118 | mamures 19426 |
. . . . . . . . . . . . 13
  
    
       maMul                      maMul            |
137 | 135, 136 | eqtr3d 2488 |
. . . . . . . . . . . 12
  
    
            
       maMul     
      |
138 | 133, 137 | oveq12d 6294 |
. . . . . . . . . . 11
  
    
                             
       maMul     
                   maMul             |
139 | 138 | 3adant3 1029 |
. . . . . . . . . 10
  
    
 
        
                                                                              
       maMul     
                   maMul             |
140 | 121, 129,
139 | 3eqtr4d 2496 |
. . . . . . . . 9
  
    
 
        
                                                                                      |
141 | | simp32 1046 |
. . . . . . . . . . 11
  
    
 
        
                                                                      |
142 | 141 | oveq1d 6291 |
. . . . . . . . . 10
  
    
 
        
                                                               maMul                       maMul              |
143 | 123 | reseq1d 5082 |
. . . . . . . . . . . 12
  
    
       maMul                           |
144 | | eqid 2452 |
. . . . . . . . . . . . 13
 maMul           maMul           |
145 | | difssd 3529 |
. . . . . . . . . . . . 13
  
    
      
  |
146 | 53, 144, 3, 125, 105, 105, 105, 145, 126, 118 | mamures 19426 |
. . . . . . . . . . . 12
  
    
       maMul                          maMul              |
147 | 143, 146 | eqtr3d 2488 |
. . . . . . . . . . 11
  
    
              
         maMul              |
148 | 147 | 3adant3 1029 |
. . . . . . . . . 10
  
    
 
        
                                                               
         maMul              |
149 | 130 | reseq1d 5082 |
. . . . . . . . . . . 12
  
    
       maMul                           |
150 | 53, 144, 3, 125, 105, 105, 105, 145, 107, 118 | mamures 19426 |
. . . . . . . . . . . 12
  
    
       maMul                          maMul              |
151 | 149, 150 | eqtr3d 2488 |
. . . . . . . . . . 11
  
    
              
         maMul              |
152 | 151 | 3adant3 1029 |
. . . . . . . . . 10
  
    
 
        
                                                               
         maMul              |
153 | 142, 148,
152 | 3eqtr4d 2496 |
. . . . . . . . 9
  
    
 
        
                                                               
          |
154 | | simp33 1047 |
. . . . . . . . . . 11
  
    
 
        
                                                                      |
155 | 154 | oveq1d 6291 |
. . . . . . . . . 10
  
    
 
        
                                                               maMul                       maMul              |
156 | 134 | reseq1d 5082 |
. . . . . . . . . . . 12
  
    
       maMul                           |
157 | 53, 144, 3, 125, 105, 105, 105, 145, 115, 118 | mamures 19426 |
. . . . . . . . . . . 12
  
    
       maMul                          maMul              |
158 | 156, 157 | eqtr3d 2488 |
. . . . . . . . . . 11
  
    
              
         maMul              |
159 | 158 | 3adant3 1029 |
. . . . . . . . . 10
  
    
 
        
                                                               
         maMul              |
160 | 155, 148,
159 | 3eqtr4d 2496 |
. . . . . . . . 9
  
    
 
        
                                                               
          |
161 | 13, 1, 2, 6, 84, 89, 93, 97, 98, 140, 153, 160 | mdetrlin 19638 |
. . . . . . . 8
  
    
 
        
                                                                               |
162 | 86, 32 | syl 17 |
. . . . . . . . 9
  
    
        
              |
163 | 162 | 3adant3 1029 |
. . . . . . . 8
  
    
 
        
                                                         
              |
164 | | oveq1 6283 |
. . . . . . . . . . . . 13
 
     |
165 | 164 | fveq2d 5852 |
. . . . . . . . . . . 12
          
    |
166 | | fvex 5858 |
. . . . . . . . . . . 12
       |
167 | 165, 26, 166 | fvmpt 5932 |
. . . . . . . . . . 11
      
              |
168 | 90, 167 | syl 17 |
. . . . . . . . . 10
  
    
        
              |
169 | | oveq1 6283 |
. . . . . . . . . . . . 13
 
     |
170 | 169 | fveq2d 5852 |
. . . . . . . . . . . 12
          
    |
171 | | fvex 5858 |
. . . . . . . . . . . 12
       |
172 | 170, 26, 171 | fvmpt 5932 |
. . . . . . . . . . 11
      
              |
173 | 94, 172 | syl 17 |
. . . . . . . . . 10
  
    
        
              |
174 | 168, 173 | oveq12d 6294 |
. . . . . . . . 9
  
    
                                                       |
175 | 174 | 3adant3 1029 |
. . . . . . . 8
  
    
 
        
                                                                                                        |
176 | 161, 163,
175 | 3eqtr4d 2496 |
. . . . . . 7
  
    
 
        
                                                         
            
                          |
177 | 176 | 3expia 1212 |
. . . . . 6
  
    
                                                               
                                              |
178 | 177 | anassrs 658 |
. . . . 5
   


  
                                                              
                                              |
179 | 178 | ralrimivva 2795 |
. . . 4
  
 
  

                                                            
                                              |
180 | 179 | ralrimivva 2795 |
. . 3
 
 



                                                            
                                              |
181 | | simp11 1039 |
. . . . . . . . 9
  
        
 
                                            |
182 | 18 | adantr 471 |
. . . . . . . . . . 11
  
        
     |
183 | | simprll 777 |
. . . . . . . . . . 11
  
        
     |
184 | | simpl3 1014 |
. . . . . . . . . . 11
  
        
     |
185 | 182, 183,
184, 38 | syl3anc 1271 |
. . . . . . . . . 10
  
        
   
   |
186 | 185 | 3adant3 1029 |
. . . . . . . . 9
  
        
 
                                          
   |
187 | | simp2lr 1077 |
. . . . . . . . 9
  
        
 
                                                |
188 | | simprrl 779 |
. . . . . . . . . . 11
  
        
     |
189 | 182, 188,
184, 95 | syl3anc 1271 |
. . . . . . . . . 10
  
        
   
   |
190 | 189 | 3adant3 1029 |
. . . . . . . . 9
  
        
 
                                          
   |
191 | | simp2rr 1079 |
. . . . . . . . 9
  
        
 
                                            |
192 | | simp3l 1037 |
. . . . . . . . . . 11
  
        
 
                                                                   |
193 | 192 | oveq1d 6291 |
. . . . . . . . . 10
  
        
 
                                                   maMul                              maMul            |
194 | 56 | adantr 471 |
. . . . . . . . . . . . . 14
  
        
    maMul       |
195 | 194 | oveqd 6293 |
. . . . . . . . . . . . 13
  
        
      maMul   
    
   |
196 | 195 | reseq1d 5082 |
. . . . . . . . . . . 12
  
        
       maMul                       |
197 | | simpl1 1012 |
. . . . . . . . . . . . 13
  
        
     |
198 | 10 | adantr 471 |
. . . . . . . . . . . . 13
  
        
     |
199 | | simprrr 780 |
. . . . . . . . . . . . . 14
  
        
     |
200 | 199 | snssd 4086 |
. . . . . . . . . . . . 13
  
        
    
  |
201 | 183, 63 | syl 17 |
. . . . . . . . . . . . 13
  
        
       
     |
202 | 66 | adantr 471 |
. . . . . . . . . . . . 13
  
        
       
     |
203 | 53, 102, 3, 197, 198, 198, 198, 200, 201, 202 | mamures 19426 |
. . . . . . . . . . . 12
  
        
       maMul                      maMul            |
204 | 196, 203 | eqtr3d 2488 |
. . . . . . . . . . 11
  
        
            
       maMul     
      |
205 | 204 | 3adant3 1029 |
. . . . . . . . . 10
  
        
 
                                                   
       maMul     
      |
206 | 194 | oveqd 6293 |
. . . . . . . . . . . . . . 15
  
        
      maMul   
    
   |
207 | 206 | reseq1d 5082 |
. . . . . . . . . . . . . 14
  
        
       maMul                       |
208 | 188, 114 | syl 17 |
. . . . . . . . . . . . . . 15
  
        
       
     |
209 | 53, 102, 3, 197, 198, 198, 198, 200, 208, 202 | mamures 19426 |
. . . . . . . . . . . . . 14
  
        
       maMul                      maMul            |
210 | 207, 209 | eqtr3d 2488 |
. . . . . . . . . . . . 13
  
        
            
       maMul     
      |
211 | 210 | oveq2d 6292 |
. . . . . . . . . . . 12
  
        
                                 
       maMul     
       |
212 | 12 | adantr 471 |
. . . . . . . . . . . . 13
  
        
     |
213 | 103 | a1i 11 |
. . . . . . . . . . . . 13
  
        
       |
214 | | simprlr 778 |
. . . . . . . . . . . . 13
  
        
         |
215 | 200, 110 | syl 17 |
. . . . . . . . . . . . . 14
  
        
           |
216 | 208, 215,
116 | syl2anc 671 |
. . . . . . . . . . . . 13
  
        
                     |
217 | 3, 212, 102, 213, 198, 198, 7, 214, 216, 202 | mamuvs1 19441 |
. . . . . . . . . . . 12
  
        
                       maMul                     
       maMul     
       |
218 | 211, 217 | eqtr4d 2489 |
. . . . . . . . . . 11
  
        
                                          maMul     
      |
219 | 218 | 3adant3 1029 |
. . . . . . . . . 10
  
        
 
                                       |