Step | Hyp | Ref
| Expression |
1 | | mdetralt.x |
. . 3
   |
2 | | mdetralt.d |
. . . 4
 maDet   |
3 | | mdetralt.a |
. . . 4
 Mat   |
4 | | mdetralt.b |
. . . 4
     |
5 | | eqid 2450 |
. . . 4
                 |
6 | | eqid 2450 |
. . . 4
 RHom   RHom   |
7 | | eqid 2450 |
. . . 4
pmSgn  pmSgn   |
8 | | eqid 2450 |
. . . 4
         |
9 | | eqid 2450 |
. . . 4
mulGrp  mulGrp   |
10 | 2, 3, 4, 5, 6, 7, 8, 9 | mdetleib 19605 |
. . 3
      g              RHom  pmSgn             mulGrp  g                 |
11 | 1, 10 | syl 17 |
. 2
      g 
            RHom  pmSgn             mulGrp  g                 |
12 | | eqid 2450 |
. . 3
         |
13 | | eqid 2450 |
. . 3
       |
14 | | mdetralt.r |
. . . . 5
   |
15 | | crngring 17784 |
. . . . 5

  |
16 | 14, 15 | syl 17 |
. . . 4
   |
17 | | ringcmn 17804 |
. . . 4

CMnd |
18 | 16, 17 | syl 17 |
. . 3
 CMnd |
19 | 3, 4 | matrcl 19430 |
. . . . . 6
 
   |
20 | 1, 19 | syl 17 |
. . . . 5
     |
21 | 20 | simpld 461 |
. . . 4
   |
22 | | eqid 2450 |
. . . . 5
         |
23 | 22, 5 | symgbasfi 17020 |
. . . 4
           |
24 | 21, 23 | syl 17 |
. . 3
           |
25 | 16 | adantr 467 |
. . . 4
 
           |
26 | | zrhpsgnmhm 19145 |
. . . . . . 7
     RHom  pmSgn        MndHom mulGrp     |
27 | 16, 21, 26 | syl2anc 666 |
. . . . . 6
   RHom  pmSgn        MndHom mulGrp     |
28 | 9, 12 | mgpbas 17722 |
. . . . . . 7
       mulGrp    |
29 | 5, 28 | mhmf 16580 |
. . . . . 6
   RHom  pmSgn        MndHom mulGrp  
  RHom  pmSgn                     |
30 | 27, 29 | syl 17 |
. . . . 5
   RHom  pmSgn                     |
31 | 30 | ffvelrnda 6020 |
. . . 4
 
            RHom  pmSgn            |
32 | 9 | crngmgp 17781 |
. . . . . . 7

mulGrp 
CMnd |
33 | 14, 32 | syl 17 |
. . . . . 6
 mulGrp  CMnd |
34 | 33 | adantr 467 |
. . . . 5
 
         mulGrp  CMnd |
35 | 21 | adantr 467 |
. . . . 5
 
           |
36 | 3, 12, 4 | matbas2i 19440 |
. . . . . . . . . 10
     
     |
37 | 1, 36 | syl 17 |
. . . . . . . . 9
           |
38 | | elmapi 7490 |
. . . . . . . . 9
                     |
39 | 37, 38 | syl 17 |
. . . . . . . 8
             |
40 | 39 | ad2antrr 731 |
. . . . . . 7
                         |
41 | 22, 5 | symgbasf1o 17017 |
. . . . . . . . . 10
               |
42 | 41 | adantl 468 |
. . . . . . . . 9
 
               |
43 | | f1of 5812 |
. . . . . . . . 9
    
      |
44 | 42, 43 | syl 17 |
. . . . . . . 8
 
               |
45 | 44 | ffvelrnda 6020 |
. . . . . . 7
                   |
46 | | simpr 463 |
. . . . . . 7
               |
47 | 40, 45, 46 | fovrnd 6438 |
. . . . . 6
                           |
48 | 47 | ralrimiva 2801 |
. . . . 5
 
                        |
49 | 28, 34, 35, 48 | gsummptcl 17592 |
. . . 4
 
          mulGrp  g                  |
50 | 12, 8 | ringcl 17787 |
. . . 4
     RHom  pmSgn           mulGrp  g                     RHom  pmSgn             mulGrp  g                   |
51 | 25, 31, 49, 50 | syl3anc 1267 |
. . 3
 
             RHom  pmSgn             mulGrp  g                   |
52 | | disjdif 3838 |
. . . 4
 pmEven           pmEven     |
53 | 52 | a1i 11 |
. . 3
  pmEven 
         pmEven      |
54 | 22, 5 | evpmss 19147 |
. . . . . 6
pmEven           |
55 | | undif 3847 |
. . . . . 6
 pmEven         
 pmEven           pmEven              |
56 | 54, 55 | mpbi 212 |
. . . . 5
 pmEven           pmEven             |
57 | 56 | eqcomi 2459 |
. . . 4
         pmEven           pmEven     |
58 | 57 | a1i 11 |
. . 3
          pmEven           pmEven      |
59 | | eqid 2450 |
. . 3
             RHom  pmSgn             mulGrp  g                           RHom  pmSgn             mulGrp  g               |
60 | 12, 13, 18, 24, 51, 53, 58, 59 | gsummptfidmsplitres 17557 |
. 2
  g              RHom  pmSgn             mulGrp  g                 g               RHom  pmSgn             mulGrp  g             
pmEven          g               RHom  pmSgn             mulGrp  g             
         pmEven        |
61 | | resmpt 5153 |
. . . . . . 7
 pmEven                        RHom  pmSgn             mulGrp  g              pmEven    pmEven      RHom  pmSgn             mulGrp  g                |
62 | 54, 61 | ax-mp 5 |
. . . . . 6
              RHom  pmSgn             mulGrp  g              pmEven    pmEven      RHom  pmSgn             mulGrp  g               |
63 | 16 | adantr 467 |
. . . . . . . . . 10
 
pmEven     |
64 | 21 | adantr 467 |
. . . . . . . . . 10
 
pmEven     |
65 | | simpr 463 |
. . . . . . . . . 10
 
pmEven   pmEven    |
66 | | eqid 2450 |
. . . . . . . . . . 11
         |
67 | 6, 7, 66 | zrhpsgnevpm 19152 |
. . . . . . . . . 10
  pmEven  
   RHom  pmSgn            |
68 | 63, 64, 65, 67 | syl3anc 1267 |
. . . . . . . . 9
 
pmEven      RHom  pmSgn            |
69 | 68 | oveq1d 6303 |
. . . . . . . 8
 
pmEven       RHom  pmSgn             mulGrp  g                         mulGrp  g               |
70 | 54 | sseli 3427 |
. . . . . . . . . 10
 pmEven 
          |
71 | 70, 49 | sylan2 477 |
. . . . . . . . 9
 
pmEven    mulGrp  g                  |
72 | 12, 8, 66 | ringlidm 17797 |
. . . . . . . . 9
   mulGrp  g                
            mulGrp  g              mulGrp  g              |
73 | 63, 71, 72 | syl2anc 666 |
. . . . . . . 8
 
pmEven               mulGrp  g              mulGrp  g              |
74 | 69, 73 | eqtrd 2484 |
. . . . . . 7
 
pmEven       RHom  pmSgn             mulGrp  g              mulGrp  g              |
75 | 74 | mpteq2dva 4488 |
. . . . . 6
  pmEven      RHom  pmSgn             mulGrp  g               pmEven   mulGrp  g               |
76 | 62, 75 | syl5eq 2496 |
. . . . 5
               RHom  pmSgn             mulGrp  g             
pmEven    pmEven   mulGrp  g               |
77 | 76 | oveq2d 6304 |
. . . 4
  g               RHom  pmSgn             mulGrp  g             
pmEven     g  pmEven   mulGrp  g                |
78 | | difss 3559 |
. . . . . . . 8
         pmEven  
         |
79 | | resmpt 5153 |
. . . . . . . 8
          pmEven                         RHom  pmSgn             mulGrp  g                       pmEven              pmEven       RHom  pmSgn             mulGrp  g                |
80 | 78, 79 | ax-mp 5 |
. . . . . . 7
              RHom  pmSgn             mulGrp  g                       pmEven              pmEven       RHom  pmSgn             mulGrp  g               |
81 | 16 | adantr 467 |
. . . . . . . . . . . 12
 
         pmEven   
  |
82 | 21 | adantr 467 |
. . . . . . . . . . . 12
 
         pmEven   
  |
83 | | simpr 463 |
. . . . . . . . . . . 12
 
         pmEven   
         pmEven     |
84 | | eqid 2450 |
. . . . . . . . . . . . 13
           |
85 | 6, 7, 66, 5, 84 | zrhpsgnodpm 19153 |
. . . . . . . . . . . 12
           pmEven       RHom  pmSgn                     |
86 | 81, 82, 83, 85 | syl3anc 1267 |
. . . . . . . . . . 11
 
         pmEven       RHom  pmSgn                     |
87 | 86 | oveq1d 6303 |
. . . . . . . . . 10
 
         pmEven        RHom  pmSgn             mulGrp  g                                  mulGrp  g               |
88 | | eldifi 3554 |
. . . . . . . . . . . 12
         
pmEven             |
89 | 88, 49 | sylan2 477 |
. . . . . . . . . . 11
 
         pmEven     mulGrp  g                  |
90 | 12, 8, 66, 84, 81, 89 | ringnegl 17815 |
. . . . . . . . . 10
 
         pmEven                         mulGrp  g                      mulGrp  g               |
91 | 87, 90 | eqtrd 2484 |
. . . . . . . . 9
 
         pmEven        RHom  pmSgn             mulGrp  g                      mulGrp  g               |
92 | 91 | mpteq2dva 4488 |
. . . . . . . 8
           pmEven       RHom  pmSgn             mulGrp  g                        pmEven            mulGrp  g                |
93 | | eqidd 2451 |
. . . . . . . . 9
           pmEven    mulGrp  g                       pmEven    mulGrp  g               |
94 | | ringgrp 17778 |
. . . . . . . . . . . 12

  |
95 | 16, 94 | syl 17 |
. . . . . . . . . . 11
   |
96 | 12, 84 | grpinvf 16703 |
. . . . . . . . . . 11
                    |
97 | 95, 96 | syl 17 |
. . . . . . . . . 10
                    |
98 | 97 | feqmptd 5916 |
. . . . . . . . 9
                       |
99 | | fveq2 5863 |
. . . . . . . . 9
  mulGrp  g                              mulGrp  g               |
100 | 89, 93, 98, 99 | fmptco 6054 |
. . . . . . . 8
                 pmEven    mulGrp  g                       
pmEven            mulGrp  g                |
101 | 92, 100 | eqtr4d 2487 |
. . . . . . 7
           pmEven       RHom  pmSgn             mulGrp  g                              pmEven    mulGrp  g                |
102 | 80, 101 | syl5eq 2496 |
. . . . . 6
               RHom  pmSgn             mulGrp  g             
         pmEven                    pmEven    mulGrp  g                |
103 | 102 | oveq2d 6304 |
. . . . 5
  g               RHom  pmSgn             mulGrp  g             
         pmEven      g                 pmEven    mulGrp  g                 |
104 | | mdetralt.z |
. . . . . 6
     |
105 | | ringabl 17803 |
. . . . . . 7

  |
106 | 16, 105 | syl 17 |
. . . . . 6
   |
107 | | difssd 3560 |
. . . . . . 7
          pmEven             |
108 | | ssfi 7789 |
. . . . . . 7
                   pmEven  
                  pmEven     |
109 | 24, 107, 108 | syl2anc 666 |
. . . . . 6
          pmEven     |
110 | | eqid 2450 |
. . . . . 6
         
pmEven    mulGrp  g                       pmEven    mulGrp  g              |
111 | 12, 104, 84, 106, 109, 89, 110 | gsummptfidminv 17573 |
. . . . 5
  g                 pmEven    mulGrp  g                        g           pmEven    mulGrp  g                 |
112 | 89 | ralrimiva 2801 |
. . . . . . . 8
           pmEven     mulGrp  g                  |
113 | | mdetralt.i |
. . . . . . . . . . . 12
   |
114 | | mdetralt.j |
. . . . . . . . . . . 12
   |
115 | | prssi 4127 |
. . . . . . . . . . . 12
 
      |
116 | 113, 114,
115 | syl2anc 666 |
. . . . . . . . . . 11
      |
117 | | mdetralt.ij |
. . . . . . . . . . . 12
   |
118 | | pr2nelem 8432 |
. . . . . . . . . . . 12
 
      |
119 | 113, 114,
117, 118 | syl3anc 1267 |
. . . . . . . . . . 11
      |
120 | | eqid 2450 |
. . . . . . . . . . . 12
pmTrsp  pmTrsp   |
121 | | eqid 2450 |
. . . . . . . . . . . 12
pmTrsp  pmTrsp   |
122 | 120, 121 | pmtrrn 17091 |
. . . . . . . . . . 11
          pmTrsp        pmTrsp    |
123 | 21, 116, 119, 122 | syl3anc 1267 |
. . . . . . . . . 10
  pmTrsp        pmTrsp    |
124 | 22, 5, 121 | pmtrodpm 19158 |
. . . . . . . . . 10
   pmTrsp        pmTrsp    pmTrsp                 pmEven     |
125 | 21, 123, 124 | syl2anc 666 |
. . . . . . . . 9
  pmTrsp                 pmEven     |
126 | 22, 5 | evpmodpmf1o 19157 |
. . . . . . . . 9
   pmTrsp                 pmEven     pmEven    pmTrsp                     pmEven             pmEven     |
127 | 21, 125, 126 | syl2anc 666 |
. . . . . . . 8
  pmEven    pmTrsp                     pmEven             pmEven     |
128 | 12, 18, 109, 112, 110, 127 | gsummptfif1o 17593 |
. . . . . . 7
  g           pmEven    mulGrp  g               g            pmEven    mulGrp  g              pmEven    pmTrsp                       |
129 | | eleq1 2516 |
. . . . . . . . . . . . 13
  pmEven 
pmEven     |
130 | 129 | anbi2d 709 |
. . . . . . . . . . . 12
  
pmEven   
pmEven      |
131 | | oveq2 6296 |
. . . . . . . . . . . . 13
   pmTrsp                    pmTrsp                    |
132 | 131 | eleq1d 2512 |
. . . . . . . . . . . 12
    pmTrsp                           pmEven  
  pmTrsp                           pmEven      |
133 | 130, 132 | imbi12d 322 |
. . . . . . . . . . 11
   
pmEven     pmTrsp                           pmEven   
  pmEven     pmTrsp                           pmEven       |
134 | 22 | symggrp 17034 |
. . . . . . . . . . . . . . 15
       |
135 | 21, 134 | syl 17 |
. . . . . . . . . . . . . 14
       |
136 | 135 | adantr 467 |
. . . . . . . . . . . . 13
 
pmEven         |
137 | 121, 22, 5 | symgtrf 17103 |
. . . . . . . . . . . . . 14
pmTrsp           |
138 | 123 | adantr 467 |
. . . . . . . . . . . . . 14
 
pmEven    pmTrsp        pmTrsp    |
139 | 137, 138 | sseldi 3429 |
. . . . . . . . . . . . 13
 
pmEven    pmTrsp                  |
140 | 70 | adantl 468 |
. . . . . . . . . . . . 13
 
pmEven             |
141 | | eqid 2450 |
. . . . . . . . . . . . . 14
               |
142 | 5, 141 | grpcl 16672 |
. . . . . . . . . . . . 13
       pmTrsp               
           pmTrsp                            |
143 | 136, 139,
140, 142 | syl3anc 1267 |
. . . . . . . . . . . 12
 
pmEven     pmTrsp                            |
144 | | eqid 2450 |
. . . . . . . . . . . . . . . . 17
 mulGrp ℂfld ↾s       mulGrp ℂfld
↾s       |
145 | 22, 7, 144 | psgnghm2 19142 |
. . . . . . . . . . . . . . . 16
 pmSgn        mulGrp ℂfld
↾s         |
146 | 21, 145 | syl 17 |
. . . . . . . . . . . . . . 15
 pmSgn        mulGrp ℂfld ↾s         |
147 | 146 | adantr 467 |
. . . . . . . . . . . . . 14
 
pmEven   pmSgn        mulGrp ℂfld
↾s         |
148 | | prex 4641 |
. . . . . . . . . . . . . . . 16
     |
149 | | eqid 2450 |
. . . . . . . . . . . . . . . . . 18
mulGrp ℂfld mulGrp ℂfld |
150 | | cnfldmul 18969 |
. . . . . . . . . . . . . . . . . 18
  ℂfld |
151 | 149, 150 | mgpplusg 17720 |
. . . . . . . . . . . . . . . . 17
  mulGrp ℂfld  |
152 | 144, 151 | ressplusg 15232 |
. . . . . . . . . . . . . . . 16
    
   mulGrp ℂfld
↾s         |
153 | 148, 152 | ax-mp 5 |
. . . . . . . . . . . . . . 15
   mulGrp ℂfld ↾s        |
154 | 5, 141, 153 | ghmlin 16881 |
. . . . . . . . . . . . . 14
  pmSgn        mulGrp ℂfld ↾s        pmTrsp               
          pmSgn      pmTrsp                     pmSgn     pmTrsp          pmSgn        |
155 | 147, 139,
140, 154 | syl3anc 1267 |
. . . . . . . . . . . . 13
 
pmEven    pmSgn      pmTrsp                     pmSgn     pmTrsp          pmSgn        |
156 | 22, 121, 7 | psgnpmtr 17144 |
. . . . . . . . . . . . . . . 16
  pmTrsp        pmTrsp   pmSgn     pmTrsp            |
157 | 138, 156 | syl 17 |
. . . . . . . . . . . . . . 15
 
pmEven    pmSgn     pmTrsp            |
158 | 22, 5, 7 | psgnevpm 19150 |
. . . . . . . . . . . . . . . 16
 
pmEven    pmSgn       |
159 | 21, 158 | sylan 474 |
. . . . . . . . . . . . . . 15
 
pmEven    pmSgn       |
160 | 157, 159 | oveq12d 6306 |
. . . . . . . . . . . . . 14
 
pmEven     pmSgn     pmTrsp          pmSgn           |
161 | | neg1cn 10710 |
. . . . . . . . . . . . . . 15
  |
162 | 161 | mulid1i 9642 |
. . . . . . . . . . . . . 14
     |
163 | 160, 162 | syl6eq 2500 |
. . . . . . . . . . . . 13
 
pmEven     pmSgn     pmTrsp          pmSgn         |
164 | 155, 163 | eqtrd 2484 |
. . . . . . . . . . . 12
 
pmEven    pmSgn      pmTrsp                      |
165 | 22, 5, 7 | psgnodpmr 19151 |
. . . . . . . . . . . 12
    pmTrsp                           pmSgn      pmTrsp                       pmTrsp                           pmEven     |
166 | 64, 143, 164, 165 | syl3anc 1267 |
. . . . . . . . . . 11
 
pmEven     pmTrsp                           pmEven     |
167 | 133, 166 | chvarv 2106 |
. . . . . . . . . 10
 
pmEven     pmTrsp                           pmEven     |
168 | | eqidd 2451 |
. . . . . . . . . 10
  pmEven    pmTrsp                    pmEven    pmTrsp                     |
169 | | fveq1 5862 |
. . . . . . . . . . . . 13
   pmTrsp                         pmTrsp                       |
170 | 169 | oveq1d 6303 |
. . . . . . . . . . . 12
   pmTrsp                              pmTrsp                          |
171 | 170 | mpteq2dv 4489 |
. . . . . . . . . . 11
   pmTrsp                                 pmTrsp                           |
172 | 171 | oveq2d 6304 |
. . . . . . . . . 10
   pmTrsp                   mulGrp  g             mulGrp  g      pmTrsp                            |
173 | 167, 168,
93, 172 | fmptco 6054 |
. . . . . . . . 9
            pmEven    mulGrp  g              pmEven    pmTrsp                     pmEven   mulGrp  g      pmTrsp                             |
174 | | oveq2 6296 |
. . . . . . . . . . . . . . 15
   pmTrsp                    pmTrsp                    |
175 | 174 | fveq1d 5865 |
. . . . . . . . . . . . . 14
    pmTrsp                        pmTrsp                       |
176 | 175 | oveq1d 6303 |
. . . . . . . . . . . . 13
     pmTrsp                            pmTrsp                          |
177 | 176 | mpteq2dv 4489 |
. . . . . . . . . . . 12
      pmTrsp                              pmTrsp                           |
178 | 177 | oveq2d 6304 |
. . . . . . . . . . 11
  mulGrp  g      pmTrsp                           mulGrp  g      pmTrsp                            |
179 | 178 | cbvmptv 4494 |
. . . . . . . . . 10
 pmEven   mulGrp  g      pmTrsp                            pmEven   mulGrp  g      pmTrsp                            |
180 | 179 | a1i 11 |
. . . . . . . . 9
  pmEven   mulGrp  g      pmTrsp                            pmEven   mulGrp  g      pmTrsp                             |
181 | 139 | adantr 467 |
. . . . . . . . . . . . . . . . 17
   pmEven  
  pmTrsp                  |
182 | 140 | adantr 467 |
. . . . . . . . . . . . . . . . 17
   pmEven  
           |
183 | 22, 5, 141 | symgov 17024 |
. . . . . . . . . . . . . . . . 17
   pmTrsp                           pmTrsp                    pmTrsp           |
184 | 181, 182,
183 | syl2anc 666 |
. . . . . . . . . . . . . . . 16
   pmEven  
   pmTrsp                    pmTrsp           |
185 | 184 | fveq1d 5865 |
. . . . . . . . . . . . . . 15
   pmEven  
    pmTrsp                        pmTrsp              |
186 | 70, 44 | sylan2 477 |
. . . . . . . . . . . . . . . 16
 
pmEven         |
187 | | fvco3 5940 |
. . . . . . . . . . . . . . . 16
     
    pmTrsp              pmTrsp                 |
188 | 186, 187 | sylan 474 |
. . . . . . . . . . . . . . 15
   pmEven  
    pmTrsp              pmTrsp                 |
189 | 185, 188 | eqtrd 2484 |
. . . . . . . . . . . . . 14
   pmEven  
    pmTrsp                       pmTrsp                 |
190 | 189 | oveq1d 6303 |
. . . . . . . . . . . . 13
   pmEven  
     pmTrsp                           pmTrsp                    |
191 | 120 | pmtrprfv 17087 |
. . . . . . . . . . . . . . . . . . 19
  
    pmTrsp             |
192 | 21, 113, 114, 117, 191 | syl13anc 1269 |
. . . . . . . . . . . . . . . . . 18
   pmTrsp             |
193 | 192 | ad2antrr 731 |
. . . . . . . . . . . . . . . . 17
   pmEven  
   pmTrsp             |
194 | 193 | oveq1d 6303 |
. . . . . . . . . . . . . . . 16
   pmEven  
    pmTrsp                    |
195 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
   pmEven  
   |
196 | | mdetralt.eq |
. . . . . . . . . . . . . . . . . 18
            |
197 | 196 | ad2antrr 731 |
. . . . . . . . . . . . . . . . 17
   pmEven  
 
          |
198 | | oveq2 6296 |
. . . . . . . . . . . . . . . . . . 19
           |
199 | | oveq2 6296 |
. . . . . . . . . . . . . . . . . . 19
           |
200 | 198, 199 | eqeq12d 2465 |
. . . . . . . . . . . . . . . . . 18
         
           |
201 | 200 | rspcv 3145 |
. . . . . . . . . . . . . . . . 17
  
                   |
202 | 195, 197,
201 | sylc 62 |
. . . . . . . . . . . . . . . 16
   pmEven  
           |
203 | 194, 202 | eqtr4d 2487 |
. . . . . . . . . . . . . . 15
   pmEven  
    pmTrsp                    |
204 | | fveq2 5863 |
. . . . . . . . . . . . . . . . 17
       pmTrsp                 pmTrsp             |
205 | 204 | oveq1d 6303 |
. . . . . . . . . . . . . . . 16
        pmTrsp                     pmTrsp                |
206 | | oveq1 6295 |
. . . . . . . . . . . . . . . 16
                   |
207 | 205, 206 | eqeq12d 2465 |
. . . . . . . . . . . . . . 15
         pmTrsp                             pmTrsp                     |
208 | 203, 207 | syl5ibrcom 226 |
. . . . . . . . . . . . . 14
   pmEven  
         pmTrsp                             |
209 | | prcom 4049 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
  |
210 | 209 | fveq2i 5866 |
. . . . . . . . . . . . . . . . . . . . . 22
 pmTrsp         pmTrsp     
   |
211 | 210 | fveq1i 5864 |
. . . . . . . . . . . . . . . . . . . . 21
  pmTrsp             pmTrsp            |
212 | 117 | necomd 2678 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
213 | 120 | pmtrprfv 17087 |
. . . . . . . . . . . . . . . . . . . . . 22
  
    pmTrsp             |
214 | 21, 114, 113, 212, 213 | syl13anc 1269 |
. . . . . . . . . . . . . . . . . . . . 21
   pmTrsp     
       |
215 | 211, 214 | syl5eq 2496 |
. . . . . . . . . . . . . . . . . . . 20
   pmTrsp             |
216 | 215 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . . 19
    pmTrsp                    |
217 | 216 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . 18
   pmEven  
    pmTrsp                    |
218 | 217, 202 | eqtrd 2484 |
. . . . . . . . . . . . . . . . 17
   pmEven  
    pmTrsp                    |
219 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . 19
       pmTrsp                 pmTrsp             |
220 | 219 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . 18
        pmTrsp                     pmTrsp                |
221 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . 18
                   |
222 | 220, 221 | eqeq12d 2465 |
. . . . . . . . . . . . . . . . 17
         pmTrsp                             pmTrsp                     |
223 | 218, 222 | syl5ibrcom 226 |
. . . . . . . . . . . . . . . 16
   pmEven  
         pmTrsp                             |
224 | 223 | a1dd 47 |
. . . . . . . . . . . . . . 15
   pmEven  
              pmTrsp                              |
225 | | neanior 2715 |
. . . . . . . . . . . . . . . . . . . . 21
                       |
226 | | elpri 3984 |
. . . . . . . . . . . . . . . . . . . . . . 23
                    |
227 | 226 | orcomd 390 |
. . . . . . . . . . . . . . . . . . . . . 22
                    |
228 | 227 | con3i 141 |
. . . . . . . . . . . . . . . . . . . . 21
          
         |
229 | 225, 228 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . 20
          
         |
230 | 229 | 3adant1 1025 |
. . . . . . . . . . . . . . . . . . 19
   
pmEven                      |
231 | 120 | pmtrmvd 17090 |
. . . . . . . . . . . . . . . . . . . . . 22
        
  pmTrsp       
     |
232 | 21, 116, 119, 231 | syl3anc 1267 |
. . . . . . . . . . . . . . . . . . . . 21
   pmTrsp       
     |
233 | 232 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . 20
   pmEven  
   pmTrsp       
     |
234 | 233 | 3ad2ant1 1028 |
. . . . . . . . . . . . . . . . . . 19
   
pmEven               pmTrsp       
     |
235 | 230, 234 | neleqtrrd 2550 |
. . . . . . . . . . . . . . . . . 18
   
pmEven                   pmTrsp          |
236 | 120 | pmtrf 17089 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          pmTrsp              |
237 | 21, 116, 119, 236 | syl3anc 1267 |
. . . . . . . . . . . . . . . . . . . . . . 23
  pmTrsp              |
238 | | ffn 5726 |
. . . . . . . . . . . . . . . . . . . . . . 23
  pmTrsp             pmTrsp          |
239 | 237, 238 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
  pmTrsp          |
240 | 239 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . 21
   pmEven  
  pmTrsp          |
241 | 186 | ffvelrnda 6020 |
. . . . . . . . . . . . . . . . . . . . 21
   pmEven  
       |
242 | | fnelnfp 6092 |
. . . . . . . . . . . . . . . . . . . . 21
   pmTrsp                    pmTrsp       
  pmTrsp                      |
243 | 240, 241,
242 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . 20
   pmEven  
        pmTrsp       
  pmTrsp                      |
244 | 243 | 3ad2ant1 1028 |
. . . . . . . . . . . . . . . . . . 19
   
pmEven                    pmTrsp       
  pmTrsp                      |
245 | 244 | necon2bbid 2666 |
. . . . . . . . . . . . . . . . . 18
   
pmEven                pmTrsp                  
      pmTrsp       
   |
246 | 235, 245 | mpbird 236 |
. . . . . . . . . . . . . . . . 17
   
pmEven               pmTrsp                     |
247 | 246 | oveq1d 6303 |
. . . . . . . . . . . . . . . 16
   
pmEven                pmTrsp                            |
248 | 247 | 3exp 1206 |
. . . . . . . . . . . . . . 15
   pmEven  
              pmTrsp                              |
249 | 224, 248 | pm2.61dne 2709 |
. . . . . . . . . . . . . 14
   pmEven  
         pmTrsp                             |
250 | 208, 249 | pm2.61dne 2709 |
. . . . . . . . . . . . 13
   pmEven  
    pmTrsp                            |
251 | 190, 250 | eqtrd 2484 |
. . . . . . . . . . . 12
   pmEven  
     pmTrsp                                  |
252 | 251 | mpteq2dva 4488 |
. . . . . . . . . . 11
 
pmEven        pmTrsp                                     |
253 | 252 | oveq2d 6304 |
. . . . . . . . . 10
 
pmEven    mulGrp  g      pmTrsp                           mulGrp  g              |
254 | 253 | mpteq2dva 4488 |
. . . . . . . . 9
  pmEven   mulGrp  g      pmTrsp                            pmEven   mulGrp  g               |
255 | 173, 180,
254 | 3eqtrd 2488 |
. . . . . . . 8
            pmEven    mulGrp  g              pmEven    pmTrsp                     pmEven   mulGrp  g               |
256 | 255 | oveq2d 6304 |
. . . . . . 7
  g            pmEven    mulGrp  g              pmEven    pmTrsp                      g 
pmEven   mulGrp  g                |
257 | 128, 256 | eqtrd 2484 |
. . . . . 6
  g           pmEven    mulGrp  g               g 
pmEven   mulGrp  g                |
258 | 257 | fveq2d 5867 |
. . . . 5
          g           pmEven    mulGrp  g                        g  pmEven   mulGrp  g                 |
259 | 103, 111,
258 | 3eqtrd 2488 |
. . . 4
  g               RHom  pmSgn             mulGrp  g             
         pmEven              g  pmEven   mulGrp  g                 |
260 | 77, 259 | oveq12d 6306 |
. . 3
   g               RHom  pmSgn             mulGrp  g              pmEven          g               RHom  pmSgn             mulGrp  g             
         pmEven        g  pmEven   mulGrp  g                            g  pmEven   mulGrp  g                  |
261 | 54 | a1i 11 |
. . . . . 6
 pmEven            |
262 | | ssfi 7789 |
. . . . . 6
          pmEven           pmEven    |
263 | 24, 261, 262 | syl2anc 666 |
. . . . 5
 pmEven    |
264 | 71 | ralrimiva 2801 |
. . . . 5
  pmEven    mulGrp  g                  |
265 | 12, 18, 263, 264 | gsummptcl 17592 |
. . . 4
  g  pmEven   mulGrp  g                    |
266 | 12, 13, 104, 84 | grprinv 16706 |
. . . 4
  
g  pmEven   mulGrp  g                     g  pmEven   mulGrp  g                            g  pmEven   mulGrp  g                 |
267 | 95, 265, 266 | syl2anc 666 |
. . 3
   g  pmEven   mulGrp  g                            g  pmEven   mulGrp  g                 |
268 | 260, 267 | eqtrd 2484 |
. 2
   g               RHom  pmSgn             mulGrp  g              pmEven          g               RHom  pmSgn             mulGrp  g             
         pmEven       |
269 | 11, 60, 268 | 3eqtrd 2488 |
1
      |