Step | Hyp | Ref
| Expression |
1 | | mdetdiag.d |
. . . 4
 maDet   |
2 | | mdetdiag.a |
. . . 4
 Mat   |
3 | | mdetdiag.b |
. . . 4
     |
4 | | eqid 2461 |
. . . 4
                 |
5 | | eqid 2461 |
. . . 4
 RHom   RHom   |
6 | | eqid 2461 |
. . . 4
pmSgn  pmSgn   |
7 | | eqid 2461 |
. . . 4
         |
8 | | eqid 2461 |
. . . 4
mulGrp  mulGrp   |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | mdetleib 19660 |
. . 3
      g              RHom  pmSgn             mulGrp  g                 |
10 | 9 | 3ad2ant3 1037 |
. 2
  
  
      g              RHom  pmSgn             mulGrp  g                 |
11 | | fveq2 5887 |
. . . . . . . . 9
               |
12 | 11 | fveq2d 5891 |
. . . . . . . 8
                       |
13 | 12 | adantr 471 |
. . . . . . 7
    
                    |
14 | 13 | 3ad2ant2 1036 |
. . . . . 6
  
  
                     |
15 | | simp2r 1041 |
. . . . . . 7
  
  
   |
16 | | eqid 2461 |
. . . . . . . 8
             |
17 | | eqid 2461 |
. . . . . . . 8
                     |
18 | | eqid 2461 |
. . . . . . . 8
 
   |
19 | 16, 17, 18 | symg1bas 17085 |
. . . . . . 7
                    |
20 | 15, 19 | syl 17 |
. . . . . 6
  
  
                    |
21 | 14, 20 | eqtrd 2495 |
. . . . 5
  
  
                  |
22 | 21 | mpteq1d 4497 |
. . . 4
  
  
              RHom  pmSgn             mulGrp  g                          RHom  pmSgn             mulGrp  g                |
23 | | snex 4654 |
. . . . . 6
      |
24 | 23 | a1i 11 |
. . . . 5
  
  
        |
25 | | ovex 6342 |
. . . . 5
    RHom  pmSgn                  mulGrp  g                   |
26 | | fveq2 5887 |
. . . . . . . 8
         RHom  pmSgn         RHom  pmSgn             |
27 | | fveq1 5886 |
. . . . . . . . . . 11
                     |
28 | 27 | oveq1d 6329 |
. . . . . . . . . 10
                             |
29 | 28 | mpteq2dv 4503 |
. . . . . . . . 9
                                 |
30 | 29 | oveq2d 6330 |
. . . . . . . 8
       mulGrp  g             mulGrp  g                   |
31 | 26, 30 | oveq12d 6332 |
. . . . . . 7
          RHom  pmSgn             mulGrp  g                 RHom  pmSgn                  mulGrp  g                    |
32 | 31 | fmptsng 6108 |
. . . . . 6
           RHom  pmSgn                  mulGrp  g                               RHom  pmSgn                  mulGrp  g                   
            RHom  pmSgn             mulGrp  g                |
33 | 32 | eqcomd 2467 |
. . . . 5
           RHom  pmSgn                  mulGrp  g                               RHom  pmSgn             mulGrp  g                          RHom  pmSgn                  mulGrp  g                      |
34 | 24, 25, 33 | sylancl 673 |
. . . 4
  
  
             RHom  pmSgn             mulGrp  g                          RHom  pmSgn                  mulGrp  g                      |
35 | | eqid 2461 |
. . . . . . . . . . . . 13
         |
36 | | eqid 2461 |
. . . . . . . . . . . . 13
          
         
  |
37 | 35, 4, 36, 6 | psgnfn 17190 |
. . . . . . . . . . . 12
pmSgn           
  |
38 | 19 | adantl 472 |
. . . . . . . . . . . . . . . . 17
    
                   |
39 | 13, 38 | eqtrd 2495 |
. . . . . . . . . . . . . . . 16
    
                 |
40 | 39 | 3ad2ant2 1036 |
. . . . . . . . . . . . . . 15
  
  
                  |
41 | | rabeq 3049 |
. . . . . . . . . . . . . . 15
                         
         
   |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . 14
  
  
           
        
   |
43 | | difeq1 3555 |
. . . . . . . . . . . . . . . . . 18
      
        |
44 | 43 | dmeqd 5055 |
. . . . . . . . . . . . . . . . 17
      
        |
45 | 44 | eleq1d 2523 |
. . . . . . . . . . . . . . . 16
       
         |
46 | 45 | rabsnif 4053 |
. . . . . . . . . . . . . . 15
        
        
           |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . 14
  
  
         
        
            |
48 | | restidsing 5179 |
. . . . . . . . . . . . . . . . . . . 20
          |
49 | | xpsng 6088 |
. . . . . . . . . . . . . . . . . . . . 21
 
              |
50 | 49 | anidms 655 |
. . . . . . . . . . . . . . . . . . . 20
              |
51 | 48, 50 | syl5req 2508 |
. . . . . . . . . . . . . . . . . . 19
     
     |
52 | | fnsng 5647 |
. . . . . . . . . . . . . . . . . . . . 21
 
          |
53 | 52 | anidms 655 |
. . . . . . . . . . . . . . . . . . . 20
          |
54 | | fnnfpeq0 6118 |
. . . . . . . . . . . . . . . . . . . 20
                          |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
       
    
      |
56 | 51, 55 | mpbird 240 |
. . . . . . . . . . . . . . . . . 18
         |
57 | | 0fin 7824 |
. . . . . . . . . . . . . . . . . 18
 |
58 | 56, 57 | syl6eqel 2547 |
. . . . . . . . . . . . . . . . 17
         |
59 | 58 | adantl 472 |
. . . . . . . . . . . . . . . 16
    
        |
60 | 59 | 3ad2ant2 1036 |
. . . . . . . . . . . . . . 15
  
  
         |
61 | 60 | iftrued 3900 |
. . . . . . . . . . . . . 14
  
  
        
                   |
62 | 42, 47, 61 | 3eqtrrd 2500 |
. . . . . . . . . . . . 13
  
  
                     |
63 | 62 | fneq2d 5688 |
. . . . . . . . . . . 12
  
  
  pmSgn        
pmSgn                |
64 | 37, 63 | mpbiri 241 |
. . . . . . . . . . 11
  
  
 pmSgn           |
65 | 23 | snid 4007 |
. . . . . . . . . . 11
             |
66 | | fvco2 5962 |
. . . . . . . . . . 11
  pmSgn                     
   RHom  pmSgn             RHom     pmSgn             |
67 | 64, 65, 66 | sylancl 673 |
. . . . . . . . . 10
  
  
    RHom  pmSgn             RHom     pmSgn             |
68 | | fveq2 5887 |
. . . . . . . . . . . . . . 15
   pmSgn  pmSgn      |
69 | 68 | adantr 471 |
. . . . . . . . . . . . . 14
    
pmSgn  pmSgn      |
70 | 69 | 3ad2ant2 1036 |
. . . . . . . . . . . . 13
  
  
 pmSgn  pmSgn      |
71 | 70 | fveq1d 5889 |
. . . . . . . . . . . 12
  
  
  pmSgn           pmSgn              |
72 | | snidg 4005 |
. . . . . . . . . . . . . . . . . 18
                    |
73 | 23, 72 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
               |
74 | 73, 19 | eleqtrrd 2542 |
. . . . . . . . . . . . . . . 16
                  |
75 | 74 | ancli 558 |
. . . . . . . . . . . . . . 15
                    |
76 | 75 | adantl 472 |
. . . . . . . . . . . . . 14
    

                  |
77 | 76 | 3ad2ant2 1036 |
. . . . . . . . . . . . 13
  
  
                    |
78 | | eqid 2461 |
. . . . . . . . . . . . . 14
pmSgn    pmSgn     |
79 | 18, 16, 17, 78 | psgnsn 17209 |
. . . . . . . . . . . . 13
                   pmSgn              |
80 | 77, 79 | syl 17 |
. . . . . . . . . . . 12
  
  
  pmSgn              |
81 | 71, 80 | eqtrd 2495 |
. . . . . . . . . . 11
  
  
  pmSgn            |
82 | 81 | fveq2d 5891 |
. . . . . . . . . 10
  
  
   RHom     pmSgn             RHom       |
83 | | crngring 17839 |
. . . . . . . . . . . 12

  |
84 | 83 | 3ad2ant1 1035 |
. . . . . . . . . . 11
  
  
   |
85 | | eqid 2461 |
. . . . . . . . . . . 12
         |
86 | 5, 85 | zrh1 19132 |
. . . . . . . . . . 11

  RHom           |
87 | 84, 86 | syl 17 |
. . . . . . . . . 10
  
  
   RHom           |
88 | 67, 82, 87 | 3eqtrd 2499 |
. . . . . . . . 9
  
  
    RHom  pmSgn                 |
89 | | simp2l 1040 |
. . . . . . . . . . . 12
  
  
     |
90 | 89 | mpteq1d 4497 |
. . . . . . . . . . 11
  
  
                                   |
91 | 90 | oveq2d 6330 |
. . . . . . . . . 10
  
  
  mulGrp  g                  mulGrp  g                     |
92 | 8 | ringmgp 17834 |
. . . . . . . . . . . . 13

mulGrp    |
93 | 83, 92 | syl 17 |
. . . . . . . . . . . 12

mulGrp    |
94 | 93 | 3ad2ant1 1035 |
. . . . . . . . . . 11
  
  
 mulGrp    |
95 | | snidg 4005 |
. . . . . . . . . . . . . . . . 17
     |
96 | 95 | adantl 472 |
. . . . . . . . . . . . . . . 16
    
    |
97 | | eleq2 2528 |
. . . . . . . . . . . . . . . . 17
         |
98 | 97 | adantr 471 |
. . . . . . . . . . . . . . . 16
    

     |
99 | 96, 98 | mpbird 240 |
. . . . . . . . . . . . . . 15
    
  |
100 | 3 | eleq2i 2531 |
. . . . . . . . . . . . . . . 16

      |
101 | 100 | biimpi 199 |
. . . . . . . . . . . . . . 15
       |
102 | | simpl 463 |
. . . . . . . . . . . . . . . 16
 
    
  |
103 | | simpr 467 |
. . . . . . . . . . . . . . . 16
 
    
      |
104 | 102, 102,
103 | 3jca 1194 |
. . . . . . . . . . . . . . 15
 
     
       |
105 | 99, 101, 104 | syl2an 484 |
. . . . . . . . . . . . . 14
       
       |
106 | 105 | 3adant1 1032 |
. . . . . . . . . . . . 13
  
  
 
       |
107 | | eqid 2461 |
. . . . . . . . . . . . . 14
         |
108 | 2, 107 | matecl 19498 |
. . . . . . . . . . . . 13
 
               |
109 | 106, 108 | syl 17 |
. . . . . . . . . . . 12
  
  
           |
110 | 8, 107 | mgpbas 17777 |
. . . . . . . . . . . 12
       mulGrp    |
111 | 109, 110 | syl6eleq 2549 |
. . . . . . . . . . 11
  
  
        mulGrp     |
112 | | eqid 2461 |
. . . . . . . . . . . 12
   mulGrp      mulGrp    |
113 | | fveq2 5887 |
. . . . . . . . . . . . . 14
                     |
114 | | eqvisset 3064 |
. . . . . . . . . . . . . . 15
   |
115 | | fvsng 6121 |
. . . . . . . . . . . . . . 15
 
            |
116 | 114, 114,
115 | syl2anc 671 |
. . . . . . . . . . . . . 14
            |
117 | 113, 116 | eqtrd 2495 |
. . . . . . . . . . . . 13
            |
118 | | id 22 |
. . . . . . . . . . . . 13
   |
119 | 117, 118 | oveq12d 6332 |
. . . . . . . . . . . 12
                    |
120 | 112, 119 | gsumsn 17635 |
. . . . . . . . . . 11
  mulGrp         mulGrp     mulGrp  g                         |
121 | 94, 15, 111, 120 | syl3anc 1276 |
. . . . . . . . . 10
  
  
  mulGrp  g                         |
122 | 91, 121 | eqtrd 2495 |
. . . . . . . . 9
  
  
  mulGrp  g                       |
123 | 88, 122 | oveq12d 6332 |
. . . . . . . 8
  
  
     RHom  pmSgn                  mulGrp  g                                    |
124 | 99 | 3ad2ant2 1036 |
. . . . . . . . . 10
  
  
   |
125 | 101 | 3ad2ant3 1037 |
. . . . . . . . . 10
  
  
       |
126 | 124, 124,
125, 108 | syl3anc 1276 |
. . . . . . . . 9
  
  
           |
127 | 107, 7, 85 | ringlidm 17852 |
. . . . . . . . 9
                                 |
128 | 84, 126, 127 | syl2anc 671 |
. . . . . . . 8
  
  
                       |
129 | 123, 128 | eqtrd 2495 |
. . . . . . 7
  
  
     RHom  pmSgn                  mulGrp  g                        |
130 | 129 | opeq2d 4186 |
. . . . . 6
  
  
            RHom  pmSgn                  mulGrp  g                  
              |
131 | 130 | sneqd 3991 |
. . . . 5
  
  
             RHom  pmSgn                  mulGrp  g                   
                |
132 | | ovex 6342 |
. . . . . 6
     |
133 | | eqidd 2462 |
. . . . . . 7
                |
134 | 133 | fmptsng 6108 |
. . . . . 6
                                         |
135 | 24, 132, 134 | sylancl 673 |
. . . . 5
  
  
                              |
136 | 131, 135 | eqtrd 2495 |
. . . 4
  
  
             RHom  pmSgn                  mulGrp  g                   
               |
137 | 22, 34, 136 | 3eqtrd 2499 |
. . 3
  
  
              RHom  pmSgn             mulGrp  g                             |
138 | 137 | oveq2d 6330 |
. 2
  
  
  g              RHom  pmSgn             mulGrp  g                g                 |
139 | | ringmnd 17837 |
. . . . 5

  |
140 | 83, 139 | syl 17 |
. . . 4

  |
141 | 140 | 3ad2ant1 1035 |
. . 3
  
  
   |
142 | 107, 133 | gsumsn 17635 |
. . 3
                 g                     |
143 | 141, 24, 126, 142 | syl3anc 1276 |
. 2
  
  
  g                     |
144 | 10, 138, 143 | 3eqtrd 2499 |
1
  
  
           |