Step | Hyp | Ref
| Expression |
1 | | mdetrsca.eq |
. . . . . . . . . . . . . 14
                          |
2 | 1 | oveqd 6325 |
. . . . . . . . . . . . 13
                                          |
3 | 2 | adantr 472 |
. . . . . . . . . . . 12
 
           
                                      |
4 | | mdetrsca.i |
. . . . . . . . . . . . . . 15
   |
5 | 4 | adantr 472 |
. . . . . . . . . . . . . 14
 
           |
6 | | snidg 3986 |
. . . . . . . . . . . . . 14
     |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . 13
 
             |
8 | | eqid 2471 |
. . . . . . . . . . . . . . . . 17
         |
9 | | eqid 2471 |
. . . . . . . . . . . . . . . . 17
                 |
10 | 8, 9 | symgbasf1o 17102 |
. . . . . . . . . . . . . . . 16
               |
11 | 10 | adantl 473 |
. . . . . . . . . . . . . . 15
 
               |
12 | | f1of 5828 |
. . . . . . . . . . . . . . 15
    
      |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . 14
 
               |
14 | 13, 5 | ffvelrnd 6038 |
. . . . . . . . . . . . 13
 
               |
15 | | ovres 6455 |
. . . . . . . . . . . . 13
        
                        |
16 | 7, 14, 15 | syl2anc 673 |
. . . . . . . . . . . 12
 
           
                     |
17 | | opelxpi 4871 |
. . . . . . . . . . . . . . 15
        
             |
18 | 7, 14, 17 | syl2anc 673 |
. . . . . . . . . . . . . 14
 
                      |
19 | | snfi 7668 |
. . . . . . . . . . . . . . . 16
 
 |
20 | | mdetrsca.x |
. . . . . . . . . . . . . . . . . . 19
   |
21 | | mdetrsca.a |
. . . . . . . . . . . . . . . . . . . 20
 Mat   |
22 | | mdetrsca.b |
. . . . . . . . . . . . . . . . . . . 20
     |
23 | 21, 22 | matrcl 19514 |
. . . . . . . . . . . . . . . . . . 19
 
   |
24 | 20, 23 | syl 17 |
. . . . . . . . . . . . . . . . . 18
     |
25 | 24 | simpld 466 |
. . . . . . . . . . . . . . . . 17
   |
26 | 25 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
           |
27 | | xpfi 7860 |
. . . . . . . . . . . . . . . 16
           |
28 | 19, 26, 27 | sylancr 676 |
. . . . . . . . . . . . . . 15
 
               |
29 | | mdetrsca.y |
. . . . . . . . . . . . . . . 16
   |
30 | 29 | adantr 472 |
. . . . . . . . . . . . . . 15
 
           |
31 | | mdetrsca.z |
. . . . . . . . . . . . . . . . . . 19
   |
32 | | mdetrsca.k |
. . . . . . . . . . . . . . . . . . . 20
     |
33 | 21, 32, 22 | matbas2i 19524 |
. . . . . . . . . . . . . . . . . . 19
       |
34 | | elmapi 7511 |
. . . . . . . . . . . . . . . . . . 19
  
          |
35 | 31, 33, 34 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
         |
36 | 35 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
                 |
37 | | ffn 5739 |
. . . . . . . . . . . . . . . . 17
      
    |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . 16
 
             |
39 | 5 | snssd 4108 |
. . . . . . . . . . . . . . . . 17
 
             |
40 | | xpss1 4948 |
. . . . . . . . . . . . . . . . 17
           |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
 
             
   |
42 | | fnssres 5699 |
. . . . . . . . . . . . . . . 16
                       |
43 | 38, 41, 42 | syl2anc 673 |
. . . . . . . . . . . . . . 15
 
                     |
44 | | eqidd 2472 |
. . . . . . . . . . . . . . 15
                                          
                 |
45 | 28, 30, 43, 44 | ofc1 6573 |
. . . . . . . . . . . . . 14
                                                   
                     |
46 | 18, 45 | mpdan 681 |
. . . . . . . . . . . . 13
 
                                    
                     |
47 | | df-ov 6311 |
. . . . . . . . . . . . 13
                                                      |
48 | | df-ov 6311 |
. . . . . . . . . . . . . 14
               
                |
49 | 48 | oveq2i 6319 |
. . . . . . . . . . . . 13
   
                                |
50 | 46, 47, 49 | 3eqtr4g 2530 |
. . . . . . . . . . . 12
 
                                                    |
51 | 3, 16, 50 | 3eqtr3d 2513 |
. . . . . . . . . . 11
 
                                   |
52 | | ovres 6455 |
. . . . . . . . . . . . 13
        
                        |
53 | 7, 14, 52 | syl2anc 673 |
. . . . . . . . . . . 12
 
           
                     |
54 | 53 | oveq2d 6324 |
. . . . . . . . . . 11
 
                                     |
55 | 51, 54 | eqtrd 2505 |
. . . . . . . . . 10
 
                             |
56 | 55 | oveq1d 6323 |
. . . . . . . . 9
 
                   mulGrp  g                             mulGrp  g                   |
57 | | mdetrsca.r |
. . . . . . . . . . . 12
   |
58 | | crngring 17869 |
. . . . . . . . . . . 12

  |
59 | 57, 58 | syl 17 |
. . . . . . . . . . 11
   |
60 | 59 | adantr 472 |
. . . . . . . . . 10
 
           |
61 | 36, 5, 14 | fovrnd 6460 |
. . . . . . . . . 10
 
                   |
62 | | eqid 2471 |
. . . . . . . . . . . 12
mulGrp  mulGrp   |
63 | 62, 32 | mgpbas 17807 |
. . . . . . . . . . 11
   mulGrp    |
64 | 62 | crngmgp 17866 |
. . . . . . . . . . . . 13

mulGrp 
CMnd |
65 | 57, 64 | syl 17 |
. . . . . . . . . . . 12
 mulGrp  CMnd |
66 | 65 | adantr 472 |
. . . . . . . . . . 11
 
         mulGrp  CMnd |
67 | | difssd 3550 |
. . . . . . . . . . . 12
 
               |
68 | | ssfi 7810 |
. . . . . . . . . . . 12
  
   
      |
69 | 26, 67, 68 | syl2anc 673 |
. . . . . . . . . . 11
 
               |
70 | | eldifi 3544 |
. . . . . . . . . . . . 13
       |
71 | 35 | ad2antrr 740 |
. . . . . . . . . . . . . 14
                     |
72 | | simpr 468 |
. . . . . . . . . . . . . 14
               |
73 | 13 | ffvelrnda 6037 |
. . . . . . . . . . . . . 14
                   |
74 | 71, 72, 73 | fovrnd 6460 |
. . . . . . . . . . . . 13
                       |
75 | 70, 74 | sylan2 482 |
. . . . . . . . . . . 12
                           |
76 | 75 | ralrimiva 2809 |
. . . . . . . . . . 11
 
                         |
77 | 63, 66, 69, 76 | gsummptcl 17677 |
. . . . . . . . . 10
 
          mulGrp  g                  |
78 | | mdetrsca.t |
. . . . . . . . . . 11
     |
79 | 32, 78 | ringass 17875 |
. . . . . . . . . 10
  
         mulGrp  g                              mulGrp  g                            mulGrp  g                    |
80 | 60, 30, 61, 77, 79 | syl13anc 1294 |
. . . . . . . . 9
 
                     mulGrp  g                            mulGrp  g                    |
81 | 56, 80 | eqtrd 2505 |
. . . . . . . 8
 
                   mulGrp  g                            mulGrp  g                    |
82 | 62, 78 | mgpplusg 17805 |
. . . . . . . . . 10
  mulGrp    |
83 | 21, 32, 22 | matbas2i 19524 |
. . . . . . . . . . . . 13
       |
84 | | elmapi 7511 |
. . . . . . . . . . . . 13
  
          |
85 | 20, 83, 84 | 3syl 18 |
. . . . . . . . . . . 12
         |
86 | 85 | ad2antrr 740 |
. . . . . . . . . . 11
                     |
87 | 86, 72, 73 | fovrnd 6460 |
. . . . . . . . . 10
                       |
88 | | disjdif 3830 |
. . . . . . . . . . 11
         |
89 | 88 | a1i 11 |
. . . . . . . . . 10
 
                   |
90 | | undif 3839 |
. . . . . . . . . . . 12
      
      |
91 | 39, 90 | sylib 201 |
. . . . . . . . . . 11
 
           
       |
92 | 91 | eqcomd 2477 |
. . . . . . . . . 10
 
            
      |
93 | 63, 82, 66, 26, 87, 89, 92 | gsummptfidmsplit 17641 |
. . . . . . . . 9
 
          mulGrp  g              mulGrp  g               mulGrp  g                   |
94 | | cmnmnd 17523 |
. . . . . . . . . . . 12
 mulGrp  CMnd mulGrp    |
95 | 66, 94 | syl 17 |
. . . . . . . . . . 11
 
         mulGrp    |
96 | 85 | adantr 472 |
. . . . . . . . . . . 12
 
                 |
97 | 96, 5, 14 | fovrnd 6460 |
. . . . . . . . . . 11
 
                   |
98 | | id 22 |
. . . . . . . . . . . . 13
   |
99 | | fveq2 5879 |
. . . . . . . . . . . . 13
           |
100 | 98, 99 | oveq12d 6326 |
. . . . . . . . . . . 12
                   |
101 | 63, 100 | gsumsn 17665 |
. . . . . . . . . . 11
  mulGrp            mulGrp  g                        |
102 | 95, 5, 97, 101 | syl3anc 1292 |
. . . . . . . . . 10
 
          mulGrp  g                        |
103 | | mdetrsca.ne |
. . . . . . . . . . . . . . 15
                   |
104 | 103 | oveqd 6325 |
. . . . . . . . . . . . . 14
                                   |
105 | 104 | ad2antrr 740 |
. . . . . . . . . . . . 13
                   
                               |
106 | | simpr 468 |
. . . . . . . . . . . . . 14
                       |
107 | 70, 73 | sylan2 482 |
. . . . . . . . . . . . . 14
                       |
108 | | ovres 6455 |
. . . . . . . . . . . . . 14
     
    
                          |
109 | 106, 107,
108 | syl2anc 673 |
. . . . . . . . . . . . 13
                   
                       |
110 | | ovres 6455 |
. . . . . . . . . . . . . 14
     
    
                          |
111 | 106, 107,
110 | syl2anc 673 |
. . . . . . . . . . . . 13
                   
                       |
112 | 105, 109,
111 | 3eqtr3d 2513 |
. . . . . . . . . . . 12
                                   |
113 | 112 | mpteq2dva 4482 |
. . . . . . . . . . 11
 
                                       |
114 | 113 | oveq2d 6324 |
. . . . . . . . . 10
 
          mulGrp  g                 mulGrp  g                  |
115 | 102, 114 | oveq12d 6326 |
. . . . . . . . 9
 
           mulGrp  g               mulGrp  g                           mulGrp  g                   |
116 | 93, 115 | eqtrd 2505 |
. . . . . . . 8
 
          mulGrp  g                      mulGrp  g                   |
117 | 63, 82, 66, 26, 74, 89, 92 | gsummptfidmsplit 17641 |
. . . . . . . . . 10
 
          mulGrp  g              mulGrp  g               mulGrp  g                   |
118 | 98, 99 | oveq12d 6326 |
. . . . . . . . . . . . 13
                   |
119 | 63, 118 | gsumsn 17665 |
. . . . . . . . . . . 12
  mulGrp            mulGrp  g                        |
120 | 95, 5, 61, 119 | syl3anc 1292 |
. . . . . . . . . . 11
 
          mulGrp  g                        |
121 | 120 | oveq1d 6323 |
. . . . . . . . . 10
 
           mulGrp  g               mulGrp  g                           mulGrp  g                   |
122 | 117, 121 | eqtrd 2505 |
. . . . . . . . 9
 
          mulGrp  g                      mulGrp  g                   |
123 | 122 | oveq2d 6324 |
. . . . . . . 8
 
           mulGrp  g                        mulGrp  g                    |
124 | 81, 116, 123 | 3eqtr4d 2515 |
. . . . . . 7
 
          mulGrp  g              mulGrp  g               |
125 | 124 | oveq2d 6324 |
. . . . . 6
 
             RHom  pmSgn       mulGrp  g                 RHom  pmSgn        mulGrp  g                |
126 | 57 | adantr 472 |
. . . . . . . . 9
 
           |
127 | | zrhpsgnmhm 19229 |
. . . . . . . . . . . 12
     RHom  pmSgn        MndHom mulGrp     |
128 | 59, 25, 127 | syl2anc 673 |
. . . . . . . . . . 11
   RHom  pmSgn        MndHom mulGrp     |
129 | 9, 63 | mhmf 16665 |
. . . . . . . . . . 11
   RHom  pmSgn        MndHom mulGrp  
  RHom  pmSgn                 |
130 | 128, 129 | syl 17 |
. . . . . . . . . 10
   RHom  pmSgn                 |
131 | 130 | ffvelrnda 6037 |
. . . . . . . . 9
 
            RHom  pmSgn        |
132 | 32, 78 | crngcom 17873 |
. . . . . . . . 9
     RHom  pmSgn     

    RHom  pmSgn           RHom  pmSgn         |
133 | 126, 131,
30, 132 | syl3anc 1292 |
. . . . . . . 8
 
             RHom  pmSgn           RHom  pmSgn         |
134 | 133 | oveq1d 6323 |
. . . . . . 7
 
              RHom  pmSgn      
 mulGrp  g                  RHom  pmSgn      
 mulGrp  g               |
135 | 74 | ralrimiva 2809 |
. . . . . . . . 9
 
                    |
136 | 63, 66, 26, 135 | gsummptcl 17677 |
. . . . . . . 8
 
          mulGrp  g              |
137 | 32, 78 | ringass 17875 |
. . . . . . . 8
      RHom  pmSgn     
 mulGrp  g                   RHom  pmSgn      
 mulGrp  g                 RHom  pmSgn        mulGrp  g                |
138 | 60, 131, 30, 136, 137 | syl13anc 1294 |
. . . . . . 7
 
              RHom  pmSgn      
 mulGrp  g                 RHom  pmSgn        mulGrp  g                |
139 | 32, 78 | ringass 17875 |
. . . . . . . 8
  
   RHom  pmSgn       mulGrp  g                   RHom  pmSgn        mulGrp  g                  RHom  pmSgn       mulGrp  g                |
140 | 60, 30, 131, 136, 139 | syl13anc 1294 |
. . . . . . 7
 
              RHom  pmSgn      
 mulGrp  g                  RHom  pmSgn       mulGrp  g                |
141 | 134, 138,
140 | 3eqtr3d 2513 |
. . . . . 6
 
             RHom  pmSgn        mulGrp  g                   RHom  pmSgn       mulGrp  g                |
142 | 125, 141 | eqtrd 2505 |
. . . . 5
 
             RHom  pmSgn       mulGrp  g                  RHom  pmSgn       mulGrp  g                |
143 | 142 | mpteq2dva 4482 |
. . . 4
              RHom  pmSgn       mulGrp  g                            RHom  pmSgn       mulGrp  g                 |
144 | 143 | oveq2d 6324 |
. . 3
  g              RHom  pmSgn       mulGrp  g                g 
             RHom  pmSgn       mulGrp  g                  |
145 | | eqid 2471 |
. . . 4
         |
146 | | eqid 2471 |
. . . 4
       |
147 | 8, 9 | symgbasfi 17105 |
. . . . 5
           |
148 | 25, 147 | syl 17 |
. . . 4
           |
149 | 32, 78 | ringcl 17872 |
. . . . 5
     RHom  pmSgn       mulGrp  g                 RHom  pmSgn       mulGrp  g               |
150 | 60, 131, 136, 149 | syl3anc 1292 |
. . . 4
 
             RHom  pmSgn       mulGrp  g               |
151 | | eqid 2471 |
. . . . 5
             RHom  pmSgn       mulGrp  g                           RHom  pmSgn       mulGrp  g               |
152 | | ovex 6336 |
. . . . . 6
    RHom  pmSgn       mulGrp  g              |
153 | 152 | a1i 11 |
. . . . 5
 
             RHom  pmSgn       mulGrp  g               |
154 | | fvex 5889 |
. . . . . 6
     |
155 | 154 | a1i 11 |
. . . . 5
       |
156 | 151, 148,
153, 155 | fsuppmptdm 7912 |
. . . 4
              RHom  pmSgn       mulGrp  g              finSupp       |
157 | 32, 145, 146, 78, 59, 148, 29, 150, 156 | gsummulc2 17913 |
. . 3
  g               RHom  pmSgn       mulGrp  g                  g 
            RHom  pmSgn       mulGrp  g                  |
158 | 144, 157 | eqtrd 2505 |
. 2
  g              RHom  pmSgn       mulGrp  g                 g              RHom  pmSgn       mulGrp  g                  |
159 | | mdetrsca.d |
. . . 4
 maDet   |
160 | | eqid 2471 |
. . . 4
 RHom   RHom   |
161 | | eqid 2471 |
. . . 4
pmSgn  pmSgn   |
162 | 159, 21, 22, 9, 160, 161, 78, 62 | mdetleib2 19690 |
. . 3
        g              RHom  pmSgn       mulGrp  g                 |
163 | 57, 20, 162 | syl2anc 673 |
. 2
      g 
            RHom  pmSgn       mulGrp  g                 |
164 | 159, 21, 22, 9, 160, 161, 78, 62 | mdetleib2 19690 |
. . . 4
        g              RHom  pmSgn       mulGrp  g                 |
165 | 57, 31, 164 | syl2anc 673 |
. . 3
      g 
            RHom  pmSgn       mulGrp  g                 |
166 | 165 | oveq2d 6324 |
. 2
         g              RHom  pmSgn       mulGrp  g                  |
167 | 158, 163,
166 | 3eqtr4d 2515 |
1
             |