Step | Hyp | Ref
| Expression |
1 | | eqid 2462 |
. . . 4
 maDet   maDet   |
2 | | eqid 2462 |
. . . 4
 Mat   Mat   |
3 | | eqid 2462 |
. . . 4
   
Mat      
Mat    |
4 | | eqid 2462 |
. . . 4
                 |
5 | | eqid 2462 |
. . . 4
 RHom   RHom   |
6 | | eqid 2462 |
. . . 4
pmSgn  pmSgn   |
7 | | eqid 2462 |
. . . 4
         |
8 | | eqid 2462 |
. . . 4
mulGrp  mulGrp   |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | mdetfval 19666 |
. . 3
 maDet       Mat    g              RHom  pmSgn             mulGrp  g                 |
10 | 9 | a1i 11 |
. 2

 maDet       Mat    g              RHom  pmSgn             mulGrp  g                  |
11 | | mat0dimbas0 19546 |
. . 3

   
Mat       |
12 | 11 | mpteq1d 4500 |
. 2

     Mat    g              RHom  pmSgn             mulGrp  g                    g              RHom  pmSgn             mulGrp  g                  |
13 | | 0ex 4551 |
. . . . 5
 |
14 | 13 | a1i 11 |
. . . 4

  |
15 | | ovex 6348 |
. . . 4
 g 
            RHom  pmSgn             mulGrp  g                |
16 | | oveq 6326 |
. . . . . . . . . 10

                  |
17 | 16 | mpteq2dv 4506 |
. . . . . . . . 9

                      |
18 | 17 | oveq2d 6336 |
. . . . . . . 8

 mulGrp  g             mulGrp  g              |
19 | 18 | oveq2d 6336 |
. . . . . . 7

    RHom  pmSgn             mulGrp  g                 RHom  pmSgn             mulGrp  g               |
20 | 19 | mpteq2dv 4506 |
. . . . . 6

             RHom  pmSgn             mulGrp  g                           RHom  pmSgn             mulGrp  g                |
21 | 20 | oveq2d 6336 |
. . . . 5

 g 
            RHom  pmSgn             mulGrp  g                g              RHom  pmSgn             mulGrp  g                 |
22 | 21 | fmptsng 6114 |
. . . 4
 
 g              RHom  pmSgn             mulGrp  g                    g 
            RHom  pmSgn             mulGrp  g                     g              RHom  pmSgn             mulGrp  g                  |
23 | 14, 15, 22 | sylancl 673 |
. . 3

    g              RHom  pmSgn             mulGrp  g                     g              RHom  pmSgn             mulGrp  g                  |
24 | | mpt0 5731 |
. . . . . . . . . . . 12
           |
25 | 24 | a1i 11 |
. . . . . . . . . . 11

            |
26 | 25 | oveq2d 6336 |
. . . . . . . . . 10

 mulGrp  g             mulGrp  g    |
27 | | eqid 2462 |
. . . . . . . . . . 11
   mulGrp      mulGrp    |
28 | 27 | gsum0 16576 |
. . . . . . . . . 10
 mulGrp  g 
   mulGrp    |
29 | 26, 28 | syl6eq 2512 |
. . . . . . . . 9

 mulGrp  g               mulGrp     |
30 | 29 | oveq2d 6336 |
. . . . . . . 8

    RHom  pmSgn             mulGrp  g                 RHom  pmSgn               mulGrp      |
31 | 30 | mpteq2dv 4506 |
. . . . . . 7

             RHom  pmSgn             mulGrp  g                           RHom  pmSgn               mulGrp       |
32 | 31 | oveq2d 6336 |
. . . . . 6

 g 
            RHom  pmSgn             mulGrp  g                g 
            RHom  pmSgn               mulGrp        |
33 | | eqid 2462 |
. . . . . . . . . . . . 13
         |
34 | 8, 33 | ringidval 17792 |
. . . . . . . . . . . 12
       mulGrp    |
35 | 34 | eqcomi 2471 |
. . . . . . . . . . 11
   mulGrp        |
36 | 35 | a1i 11 |
. . . . . . . . . 10
              mulGrp         |
37 | 36 | oveq2d 6336 |
. . . . . . . . 9
               RHom  pmSgn               mulGrp        RHom  pmSgn                   |
38 | | 0fin 7830 |
. . . . . . . . . . 11
 |
39 | 4, 6, 5 | zrhcopsgnelbas 19218 |
. . . . . . . . . . 11
          
   RHom  pmSgn            |
40 | 38, 39 | mp3an2 1361 |
. . . . . . . . . 10
              RHom  pmSgn            |
41 | | eqid 2462 |
. . . . . . . . . . 11
         |
42 | 41, 7, 33 | ringridm 17860 |
. . . . . . . . . 10
     RHom  pmSgn               RHom  pmSgn                    RHom  pmSgn        |
43 | 40, 42 | syldan 477 |
. . . . . . . . 9
               RHom  pmSgn                    RHom  pmSgn        |
44 | 37, 43 | eqtrd 2496 |
. . . . . . . 8
               RHom  pmSgn               mulGrp       RHom  pmSgn        |
45 | 44 | mpteq2dva 4505 |
. . . . . . 7

             RHom  pmSgn               mulGrp                 RHom  pmSgn         |
46 | 45 | oveq2d 6336 |
. . . . . 6

 g 
            RHom  pmSgn               mulGrp       g             RHom  pmSgn          |
47 | | simpl 463 |
. . . . . . . . . 10
             |
48 | 38 | a1i 11 |
. . . . . . . . . 10
             |
49 | | simpr 467 |
. . . . . . . . . . 11
                     |
50 | | elsni 4005 |
. . . . . . . . . . . . . 14
     |
51 | | fveq2 5892 |
. . . . . . . . . . . . . . 15

 pmSgn      pmSgn       |
52 | | psgn0fv0 17207 |
. . . . . . . . . . . . . . 15
 pmSgn      |
53 | 51, 52 | syl6eq 2512 |
. . . . . . . . . . . . . 14

 pmSgn       |
54 | 50, 53 | syl 17 |
. . . . . . . . . . . . 13
    pmSgn       |
55 | | symgbas0 17090 |
. . . . . . . . . . . . 13
           |
56 | 54, 55 | eleq2s 2558 |
. . . . . . . . . . . 12
          pmSgn       |
57 | 56 | adantl 472 |
. . . . . . . . . . 11
            pmSgn       |
58 | | eqid 2462 |
. . . . . . . . . . . . 13
   
     |
59 | 58, 4, 6 | psgnevpmb 19210 |
. . . . . . . . . . . 12

 pmEven 
          pmSgn         |
60 | 48, 59 | syl 17 |
. . . . . . . . . . 11
            pmEven 
          pmSgn         |
61 | 49, 57, 60 | mpbir2and 938 |
. . . . . . . . . 10
           pmEven    |
62 | 5, 6, 33 | zrhpsgnevpm 19214 |
. . . . . . . . . 10
  pmEven      RHom  pmSgn            |
63 | 47, 48, 61, 62 | syl3anc 1276 |
. . . . . . . . 9
              RHom  pmSgn            |
64 | 63 | mpteq2dva 4505 |
. . . . . . . 8

            RHom  pmSgn                       |
65 | 64 | oveq2d 6336 |
. . . . . . 7

 g 
           RHom  pmSgn         g                  |
66 | 55 | a1i 11 |
. . . . . . . . 9

            |
67 | 66 | mpteq1d 4500 |
. . . . . . . 8

                        |
68 | 67 | oveq2d 6336 |
. . . . . . 7

 g 
               g            |
69 | | ringmnd 17844 |
. . . . . . . 8

  |
70 | 41, 33 | ringidcl 17856 |
. . . . . . . 8

          |
71 | | eqidd 2463 |
. . . . . . . . 9

          |
72 | 41, 71 | gsumsn 17642 |
. . . . . . . 8
 
          g                |
73 | 69, 14, 70, 72 | syl3anc 1276 |
. . . . . . 7

 g 
              |
74 | 65, 68, 73 | 3eqtrd 2500 |
. . . . . 6

 g 
           RHom  pmSgn              |
75 | 32, 46, 74 | 3eqtrd 2500 |
. . . . 5

 g 
            RHom  pmSgn             mulGrp  g                     |
76 | 75 | opeq2d 4187 |
. . . 4

   g              RHom  pmSgn             mulGrp  g               
         |
77 | 76 | sneqd 3992 |
. . 3

    g              RHom  pmSgn             mulGrp  g                   
        |
78 | 23, 77 | eqtr3d 2498 |
. 2

    g              RHom  pmSgn             mulGrp  g                           |
79 | 10, 12, 78 | 3eqtrd 2500 |
1

 maDet             |