Step | Hyp | Ref
| Expression |
1 | | fveq1 5864 |
. . . . . 6
           |
2 | 1 | oveq1d 6305 |
. . . . 5
                   |
3 | 2 | mpt2eq3dv 6357 |
. . . 4
                         |
4 | 3 | fveq2d 5869 |
. . 3
                    
            |
5 | | fveq2 5865 |
. . . 4
    RHom  pmSgn         RHom  pmSgn        |
6 | 5 | oveq1d 6305 |
. . 3
     RHom  pmSgn               RHom  pmSgn             |
7 | 4, 6 | eqeq12d 2466 |
. 2
                     RHom  pmSgn               
              RHom  pmSgn              |
8 | | fveq1 5864 |
. . . . . 6
           
                     |
9 | 8 | oveq1d 6305 |
. . . . 5
           
                             |
10 | 9 | mpt2eq3dv 6357 |
. . . 4
           
            
                      |
11 | 10 | fveq2d 5869 |
. . 3
           
    
                                      |
12 | | fveq2 5865 |
. . . 4
           
   RHom  pmSgn         RHom  pmSgn                   |
13 | 12 | oveq1d 6305 |
. . 3
           
    RHom  pmSgn               RHom  pmSgn                        |
14 | 11, 13 | eqeq12d 2466 |
. 2
           
                    RHom  pmSgn               
                         RHom  pmSgn                         |
15 | | fveq1 5864 |
. . . . . 6
        
                  |
16 | 15 | oveq1d 6305 |
. . . . 5
        
                          |
17 | 16 | mpt2eq3dv 6357 |
. . . 4
        
            
                   |
18 | 17 | fveq2d 5869 |
. . 3
        
    
                                   |
19 | | fveq2 5865 |
. . . 4
        
   RHom  pmSgn         RHom  pmSgn                |
20 | 19 | oveq1d 6305 |
. . 3
        
    RHom  pmSgn               RHom  pmSgn                     |
21 | 18, 20 | eqeq12d 2466 |
. 2
        
                    RHom  pmSgn               
                      RHom  pmSgn                      |
22 | | fveq1 5864 |
. . . . . 6
           |
23 | 22 | oveq1d 6305 |
. . . . 5
                   |
24 | 23 | mpt2eq3dv 6357 |
. . . 4
                         |
25 | 24 | fveq2d 5869 |
. . 3
                    
            |
26 | | fveq2 5865 |
. . . 4
    RHom  pmSgn         RHom  pmSgn        |
27 | 26 | oveq1d 6305 |
. . 3
     RHom  pmSgn               RHom  pmSgn             |
28 | 25, 27 | eqeq12d 2466 |
. 2
                     RHom  pmSgn               
              RHom  pmSgn              |
29 | | eqid 2451 |
. 2
                 |
30 | | eqid 2451 |
. 2
               |
31 | | eqid 2451 |
. 2
                 |
32 | | mdetuni.n |
. . . 4
   |
33 | 32 | 3ad2ant1 1029 |
. . 3
 
    
  |
34 | | eqid 2451 |
. . . 4
         |
35 | 34 | symggrp 17041 |
. . 3
       |
36 | | grpmnd 16678 |
. . 3
           |
37 | 33, 35, 36 | 3syl 18 |
. 2
 
    
      |
38 | | eqid 2451 |
. . . 4
pmTrsp  pmTrsp   |
39 | 38, 34, 31 | symgtrf 17110 |
. . 3
pmTrsp           |
40 | 39 | a1i 11 |
. 2
 
    
pmTrsp            |
41 | | eqid 2451 |
. . . . . 6
mrCls SubMnd       mrCls SubMnd        |
42 | 38, 34, 31, 41 | symggen2 17112 |
. . . . 5
  mrCls SubMnd         pmTrsp             |
43 | 32, 42 | syl 17 |
. . . 4
  mrCls SubMnd         pmTrsp             |
44 | 43 | eqcomd 2457 |
. . 3
          mrCls SubMnd         pmTrsp     |
45 | 44 | 3ad2ant1 1029 |
. 2
 
    
         mrCls SubMnd        
pmTrsp     |
46 | | mdetuni.r |
. . . . 5
   |
47 | 46 | 3ad2ant1 1029 |
. . . 4
 
    
  |
48 | | mdetuni.ff |
. . . . . 6
       |
49 | 48 | 3ad2ant1 1029 |
. . . . 5
 
    
      |
50 | | simp3 1010 |
. . . . 5
 
    
  |
51 | 49, 50 | ffvelrnd 6023 |
. . . 4
 
    
      |
52 | | mdetuni.k |
. . . . 5
     |
53 | | mdetuni.tg |
. . . . 5
     |
54 | | mdetuni.1r |
. . . . 5
     |
55 | 52, 53, 54 | ringlidm 17804 |
. . . 4
                  |
56 | 47, 51, 55 | syl2anc 667 |
. . 3
 
    
           |
57 | | zrhpsgnmhm 19152 |
. . . . . . 7
     RHom  pmSgn        MndHom mulGrp     |
58 | 46, 32, 57 | syl2anc 667 |
. . . . . 6
   RHom  pmSgn        MndHom mulGrp     |
59 | | eqid 2451 |
. . . . . . . 8
mulGrp  mulGrp   |
60 | 59, 54 | ringidval 17737 |
. . . . . . 7
   mulGrp    |
61 | 29, 60 | mhm0 16590 |
. . . . . 6
   RHom  pmSgn        MndHom mulGrp  
   RHom  pmSgn               |
62 | 58, 61 | syl 17 |
. . . . 5
    RHom  pmSgn               |
63 | 62 | 3ad2ant1 1029 |
. . . 4
 
    
   RHom  pmSgn               |
64 | 63 | oveq1d 6305 |
. . 3
 
    
    RHom  pmSgn                          |
65 | 34 | symgid 17042 |
. . . . . . . . . . . 12
            |
66 | 32, 65 | syl 17 |
. . . . . . . . . . 11
            |
67 | 66 | 3ad2ant1 1029 |
. . . . . . . . . 10
 
    
           |
68 | 67 | 3ad2ant1 1029 |
. . . . . . . . 9
       
            |
69 | 68 | fveq1d 5867 |
. . . . . . . 8
       
                    |
70 | | simp2 1009 |
. . . . . . . . 9
       
   |
71 | | fvresi 6090 |
. . . . . . . . 9
        |
72 | 70, 71 | syl 17 |
. . . . . . . 8
       
        |
73 | 69, 72 | eqtr3d 2487 |
. . . . . . 7
       
               |
74 | 73 | oveq1d 6305 |
. . . . . 6
       
                       |
75 | 74 | mpt2eq3dva 6355 |
. . . . 5
 
    
                            |
76 | | mdetuni.a |
. . . . . . . . 9
 Mat   |
77 | | mdetuni.b |
. . . . . . . . 9
     |
78 | 76, 52, 77 | matbas2i 19447 |
. . . . . . . 8
       |
79 | 78 | 3ad2ant3 1031 |
. . . . . . 7
 
    

     |
80 | | elmapi 7493 |
. . . . . . 7
  
          |
81 | | ffn 5728 |
. . . . . . 7
      
    |
82 | 79, 80, 81 | 3syl 18 |
. . . . . 6
 
    

   |
83 | | fnov 6404 |
. . . . . 6
  
 
       |
84 | 82, 83 | sylib 200 |
. . . . 5
 
    
 
       |
85 | 75, 84 | eqtr4d 2488 |
. . . 4
 
    
                     |
86 | 85 | fveq2d 5869 |
. . 3
 
    
    
                        |
87 | 56, 64, 86 | 3eqtr4rd 2496 |
. 2
 
    
    
                      RHom  pmSgn                     |
88 | | simp2 1009 |
. . . . . . . . . . . 12
                pmTrsp             |
89 | 39 | sseli 3428 |
. . . . . . . . . . . . 13
 pmTrsp            |
90 | 89 | 3ad2ant3 1031 |
. . . . . . . . . . . 12
                pmTrsp             |
91 | 34, 31, 30 | symgov 17031 |
. . . . . . . . . . . 12
         
                        |
92 | 88, 90, 91 | syl2anc 667 |
. . . . . . . . . . 11
                pmTrsp                  |
93 | 92 | fveq1d 5867 |
. . . . . . . . . 10
                pmTrsp                          |
94 | 93 | 3ad2ant1 1029 |
. . . . . . . . 9
                 pmTrsp  

                       |
95 | 34, 31 | symgbasf1o 17024 |
. . . . . . . . . . . 12
               |
96 | | f1of 5814 |
. . . . . . . . . . . 12
    
      |
97 | 90, 95, 96 | 3syl 18 |
. . . . . . . . . . 11
                pmTrsp         |
98 | 97 | 3ad2ant1 1029 |
. . . . . . . . . 10
                 pmTrsp  

      |
99 | | simp2 1009 |
. . . . . . . . . 10
                 pmTrsp  

  |
100 | | fvco3 5942 |
. . . . . . . . . 10
     
                 |
101 | 98, 99, 100 | syl2anc 667 |
. . . . . . . . 9
                 pmTrsp  

                |
102 | 94, 101 | eqtrd 2485 |
. . . . . . . 8
                 pmTrsp  

                         |
103 | 102 | oveq1d 6305 |
. . . . . . 7
                 pmTrsp  

                                 |
104 | 103 | mpt2eq3dva 6355 |
. . . . . 6
                pmTrsp                                          |
105 | 104 | fveq2d 5869 |
. . . . 5
                pmTrsp       
                                          |
106 | 34, 31 | symgbasf 17025 |
. . . . . 6
               |
107 | | eqid 2451 |
. . . . . . . . 9
pmTrsp  pmTrsp   |
108 | 107, 38 | pmtrrn2 17101 |
. . . . . . . 8
 pmTrsp  


 pmTrsp           |
109 | | mdetuni.0g |
. . . . . . . . . . . . . 14
     |
110 | | mdetuni.pg |
. . . . . . . . . . . . . 14
    |
111 | | mdetuni.al |
. . . . . . . . . . . . . 14
  

  
               |
112 | | mdetuni.li |
. . . . . . . . . . . . . 14
  


                                                       
        
        |
113 | | mdetuni.sc |
. . . . . . . . . . . . . 14
  


                                         
             |
114 | | simpll1 1047 |
. . . . . . . . . . . . . 14
                     |
115 | | df-3an 987 |
. . . . . . . . . . . . . . . 16
 

 

   |
116 | 115 | biimpri 210 |
. . . . . . . . . . . . . . 15
  

 
   |
117 | 116 | adantl 468 |
. . . . . . . . . . . . . 14
                   
   |
118 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 
    
        |
119 | 118 | adantr 467 |
. . . . . . . . . . . . . . . . 17
                     |
120 | 119 | ad2antrr 732 |
. . . . . . . . . . . . . . . 16
        
          
         |
121 | | simpllr 769 |
. . . . . . . . . . . . . . . . 17
        
          
       |
122 | | simprlr 773 |
. . . . . . . . . . . . . . . . . 18
                     |
123 | 122 | adantr 467 |
. . . . . . . . . . . . . . . . 17
        
          
   |
124 | 121, 123 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . 16
        
          
       |
125 | | simpr 463 |
. . . . . . . . . . . . . . . 16
        
          
   |
126 | 120, 124,
125 | fovrnd 6441 |
. . . . . . . . . . . . . . 15
        
          
           |
127 | | simprll 772 |
. . . . . . . . . . . . . . . . . 18
                     |
128 | 127 | adantr 467 |
. . . . . . . . . . . . . . . . 17
        
          
   |
129 | 121, 128 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . 16
        
          
       |
130 | 120, 129,
125 | fovrnd 6441 |
. . . . . . . . . . . . . . 15
        
          
           |
131 | 126, 130 | jca 535 |
. . . . . . . . . . . . . 14
        
          
                     |
132 | 118 | ad2antrr 732 |
. . . . . . . . . . . . . . . 16
                           |
133 | 132 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . 15
        
          
         |
134 | | simp1lr 1072 |
. . . . . . . . . . . . . . . 16
        
          
       |
135 | | simp2 1009 |
. . . . . . . . . . . . . . . 16
        
          
   |
136 | 134, 135 | ffvelrnd 6023 |
. . . . . . . . . . . . . . 15
        
          
       |
137 | | simp3 1010 |
. . . . . . . . . . . . . . 15
        
          
   |
138 | 133, 136,
137 | fovrnd 6441 |
. . . . . . . . . . . . . 14
        
          
           |
139 | 76, 77, 52, 109, 54, 110, 53, 32, 46, 48, 111, 112, 113, 114, 117, 131, 138 | mdetunilem6 19642 |
. . . . . . . . . . . . 13
                                                                        
                                       |
140 | | simpl1 1011 |
. . . . . . . . . . . . . . 15
               |
141 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . 22
   pmTrsp             pmTrsp             |
142 | 32 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
 

    |
143 | | simprll 772 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
 

    |
144 | | simprlr 773 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
 

    |
145 | | simprr 766 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
 

    |
146 | 107 | pmtrprfv 17094 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
    pmTrsp             |
147 | 142, 143,
144, 145, 146 | syl13anc 1270 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 

    pmTrsp             |
148 | 147 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
    

 
   pmTrsp             |
149 | 141, 148 | sylan9eqr 2507 |
. . . . . . . . . . . . . . . . . . . . 21
        


  pmTrsp             |
150 | 149 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . 20
        


     pmTrsp                  |
151 | 150 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . 19
        


      pmTrsp                         |
152 | | iftrue 3887 |
. . . . . . . . . . . . . . . . . . . 20
                                             |
153 | 152 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
        


                                            |
154 | 151, 153 | eqtr4d 2488 |
. . . . . . . . . . . . . . . . . 18
        


      pmTrsp                                                   |
155 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   pmTrsp             pmTrsp             |
156 | | prcom 4050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
157 | 156 | fveq2i 5868 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 pmTrsp         pmTrsp         |
158 | 157 | fveq1i 5866 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  pmTrsp             pmTrsp            |
159 | 32 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    

 
   |
160 | | simplrl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    

 
 
   |
161 | 160 | simprd 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    

 
   |
162 | 160 | simpld 461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    

 
   |
163 | | simplrr 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    

 
   |
164 | 163 | necomd 2679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    

 
   |
165 | 107 | pmtrprfv 17094 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
    pmTrsp             |
166 | 159, 161,
162, 164, 165 | syl13anc 1270 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    

 
   pmTrsp             |
167 | 158, 166 | syl5eq 2497 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    

 
   pmTrsp             |
168 | 155, 167 | sylan9eqr 2507 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        


  pmTrsp             |
169 | 168 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . . 23
        


     pmTrsp                  |
170 | 169 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . . 22
        


      pmTrsp                         |
171 | | iftrue 3887 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                |
172 | 171 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
        


                               |
173 | 170, 172 | eqtr4d 2488 |
. . . . . . . . . . . . . . . . . . . . 21
        


      pmTrsp                                      |
174 | 173 | adantlr 721 |
. . . . . . . . . . . . . . . . . . . 20
         
         pmTrsp                                      |
175 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 |
176 | 175 | elpr 3986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   

   |
177 | 176 | notbii 298 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
    |
178 | | ioran 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
   |
179 | 177, 178 | bitr2i 254 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
     |
180 | 179 | biimpi 198 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
     |
181 | 180 | adantll 720 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
  
     |
182 | | prssi 4128 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   
  |
183 | 160, 182 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    

 
   
  |
184 | | pr2ne 8436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
        |
185 | 160, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    

 
        |
186 | 163, 185 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    

 
      |
187 | 107 | pmtrmvd 17097 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
           pmTrsp             |
188 | 159, 183,
186, 187 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    

 
   pmTrsp             |
189 | 188 | eleq2d 2514 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    

 
    pmTrsp              |
190 | 189 | notbid 296 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    

 
    pmTrsp              |
191 | 190 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
      pmTrsp              |
192 | 181, 191 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
  
  pmTrsp          |
193 | 107 | pmtrf 17096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
          pmTrsp              |
194 | 159, 183,
186, 193 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    

 
  pmTrsp              |
195 | | ffn 5728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  pmTrsp             pmTrsp          |
196 | 194, 195 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    

 
  pmTrsp          |
197 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    

 
   |
198 | | fnelnfp 6094 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   pmTrsp            pmTrsp       
  pmTrsp              |
199 | 198 | necon2bbid 2667 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   pmTrsp            pmTrsp          
  pmTrsp           |
200 | 196, 197,
199 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    

 
    pmTrsp          
  pmTrsp           |
201 | 200 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
      pmTrsp          
  pmTrsp           |
202 | 192, 201 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
     pmTrsp             |
203 | 202 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . 22
         
        pmTrsp                  |
204 | 203 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . 21
         
         pmTrsp                         |
205 | | iffalse 3890 |
. . . . . . . . . . . . . . . . . . . . . 22
                                |
206 | 205 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
         
                                  |
207 | 204, 206 | eqtr4d 2488 |
. . . . . . . . . . . . . . . . . . . 20
         
         pmTrsp                                      |
208 | 174, 207 | pm2.61dan 800 |
. . . . . . . . . . . . . . . . . . 19
        
 
      pmTrsp                                      |
209 | | iffalse 3890 |
. . . . . . . . . . . . . . . . . . . 20
                                                          |
210 | 209 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
        
 
                                                         |
211 | 208, 210 | eqtr4d 2488 |
. . . . . . . . . . . . . . . . . 18
        
 
      pmTrsp                                                   |
212 | 154, 211 | pm2.61dan 800 |
. . . . . . . . . . . . . . . . 17
    

 
       pmTrsp                                                   |
213 | 212 | 3adant3 1028 |
. . . . . . . . . . . . . . . 16
    

 
       pmTrsp                                                   |
214 | 213 | mpt2eq3dva 6355 |
. . . . . . . . . . . . . . 15
 
 

          pmTrsp                                                       |
215 | 140, 214 | sylan 474 |
. . . . . . . . . . . . . 14
                    
      pmTrsp                                                       |
216 | 215 | fveq2d 5869 |
. . . . . . . . . . . . 13
                              pmTrsp                                                            |
217 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . 21
           |
218 | 217 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . 20
                   |
219 | | iftrue 3887 |
. . . . . . . . . . . . . . . . . . . 20
                                             |
220 | 218, 219 | eqtr4d 2488 |
. . . . . . . . . . . . . . . . . . 19
                                             |
221 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
222 | 221 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   |
223 | | iftrue 3887 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                |
224 | 222, 223 | eqtr4d 2488 |
. . . . . . . . . . . . . . . . . . . . . 22
                                |
225 | 224 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
  
                               |
226 | | iffalse 3890 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                |
227 | 226 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . 22
                                |
228 | 227 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
                                  |
229 | 225, 228 | pm2.61dan 800 |
. . . . . . . . . . . . . . . . . . . 20
                                |
230 | | iffalse 3890 |
. . . . . . . . . . . . . . . . . . . 20
                                                          |
231 | 229, 230 | eqtr4d 2488 |
. . . . . . . . . . . . . . . . . . 19
                                             |
232 | 220, 231 | pm2.61i 168 |
. . . . . . . . . . . . . . . . . 18
                                           |
233 | 232 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
                                             |
234 | 233 | mpt2eq3ia 6356 |
. . . . . . . . . . . . . . . 16
                                                 |
235 | 234 | fveq2i 5868 |
. . . . . . . . . . . . . . 15
                   
                                     |
236 | 235 | fveq2i 5868 |
. . . . . . . . . . . . . 14
            
                       
                                      |
237 | 236 | a1i 11 |
. . . . . . . . . . . . 13
                                                       
                                       |
238 | 139, 216,
237 | 3eqtr4d 2495 |
. . . . . . . . . . . 12
                              pmTrsp                             
             |
239 | | fveq1 5864 |
. . . . . . . . . . . . . . . . 17
  pmTrsp       
      pmTrsp             |
240 | 239 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
  pmTrsp       
             pmTrsp              |
241 | 240 | oveq1d 6305 |
. . . . . . . . . . . . . . 15
  pmTrsp       
                  pmTrsp                 |
242 | 241 | mpt2eq3dv 6357 |
. . . . . . . . . . . . . 14
  pmTrsp       
                
      pmTrsp                  |
243 | 242 | fveq2d 5869 |
. . . . . . . . . . . . 13
  pmTrsp       
    
                         pmTrsp                   |
244 | 243 | eqeq1d 2453 |
. . . . . . . . . . . 12
  pmTrsp       
                                
                      pmTrsp                             
              |
245 | 238, 244 | syl5ibrcom 226 |
. . . . . . . . . . 11
                     pmTrsp                                       
              |
246 | 245 | expr 620 |
. . . . . . . . . 10
              
     pmTrsp                                       
               |
247 | 246 | impd 433 |
. . . . . . . . 9
              
   
 pmTrsp                                                       |
248 | 247 | rexlimdvva 2886 |
. . . . . . . 8
                  pmTrsp        
    
                                         |
249 | 108, 248 | syl5 33 |
. . . . . . 7
              pmTrsp                                                |
250 | 249 | 3impia 1205 |
. . . . . 6
            pmTrsp                                  
             |
251 | 106, 250 | syl3an2 1302 |
. . . . 5
                pmTrsp       
                                        |
252 | 105, 251 | eqtrd 2485 |
. . . 4
                pmTrsp       
                                               |
253 | 252 | adantr 467 |
. . 3
                 pmTrsp       
              RHom  pmSgn                                                  
             |
254 | | fveq2 5865 |
. . . 4
                    RHom  pmSgn          
            
                       RHom  pmSgn              |
255 | 254 | adantl 468 |
. . 3
                 pmTrsp       
              RHom  pmSgn                                                RHom  pmSgn              |
256 | | eqid 2451 |
. . . . . 6
           |
257 | 47 | 3ad2ant1 1029 |
. . . . . 6
                pmTrsp     |
258 | 58 | 3ad2ant1 1029 |
. . . . . . . . 9
 
    
  RHom  pmSgn        MndHom mulGrp     |
259 | 258 | 3ad2ant1 1029 |
. . . . . . . 8
                pmTrsp     RHom  pmSgn        MndHom mulGrp     |
260 | 59, 52 | mgpbas 17729 |
. . . . . . . . 9
   mulGrp    |
261 | 31, 260 | mhmf 16587 |
. . . . . . . 8
   RHom  pmSgn        MndHom mulGrp  
  RHom  pmSgn                 |
262 | 259, 261 | syl 17 |
. . . . . . 7
                pmTrsp     RHom  pmSgn                 |
263 | 262, 88 | ffvelrnd 6023 |
. . . . . 6
                pmTrsp      RHom  pmSgn        |
264 | 49 | 3ad2ant1 1029 |
. . . . . . 7
                pmTrsp         |
265 | | simp13 1040 |
. . . . . . 7
                pmTrsp     |
266 | 264, 265 | ffvelrnd 6023 |
. . . . . 6
                pmTrsp         |
267 | 52, 53, 256, 257, 263, 266 | ringmneg1 17824 |
. . . . 5
                pmTrsp               RHom  pmSgn                        RHom  pmSgn              |
268 | 59, 53 | mgpplusg 17727 |
. . . . . . . . 9
  mulGrp    |
269 | 31, 30, 268 | mhmlin 16589 |
. . . . . . . 8
    RHom  pmSgn        MndHom mulGrp  
       
            RHom  pmSgn                     RHom  pmSgn         RHom  pmSgn         |
270 | 259, 88, 90, 269 | syl3anc 1268 |
. . . . . . 7
                pmTrsp      RHom  pmSgn       
             RHom  pmSgn         RHom  pmSgn         |
271 | 33 | 3ad2ant1 1029 |
. . . . . . . . 9
                pmTrsp     |
272 | | simp3 1010 |
. . . . . . . . . 10
                pmTrsp   pmTrsp    |
273 | 34, 31, 38 | pmtrodpm 19165 |
. . . . . . . . . 10
 
pmTrsp            pmEven     |
274 | 271, 272,
273 | syl2anc 667 |
. . . . . . . . 9
                pmTrsp            pmEven     |
275 | | eqid 2451 |
. . . . . . . . . 10
 RHom   RHom   |
276 | | eqid 2451 |
. . . . . . . . . 10
pmSgn  pmSgn   |
277 | 275, 276,
54, 31, 256 | zrhpsgnodpm 19160 |
. . . . . . . . 9
           pmEven       RHom  pmSgn               |
278 | 257, 271,
274, 277 | syl3anc 1268 |
. . . . . . . 8
                pmTrsp      RHom  pmSgn               |
279 | 278 | oveq2d 6306 |
. . . . . . 7
                pmTrsp       RHom  pmSgn         RHom  pmSgn           RHom  pmSgn                |
280 | 52, 53, 54, 256, 257, 263 | rngnegr 17823 |
. . . . . . 7
                pmTrsp       RHom  pmSgn                         RHom  pmSgn         |
281 | 270, 279,
280 | 3eqtrrd 2490 |
. . . . . 6
                pmTrsp              RHom  pmSgn          RHom  pmSgn                   |
282 | 281 | oveq1d 6305 |
. . . . 5
                pmTrsp               RHom  pmSgn                RHom  pmSgn                        |
283 | 267, 282 | eqtr3d 2487 |
. . . 4
                pmTrsp               RHom  pmSgn                RHom  pmSgn                        |
284 | 283 | adantr 467 |
. . 3
                 pmTrsp       
              RHom  pmSgn                        RHom  pmSgn                RHom  pmSgn                        |
285 | 253, 255,
284 | 3eqtrd 2489 |
. 2
                 pmTrsp       
              RHom  pmSgn                                          RHom  pmSgn                        |
286 | | simp2 1009 |
. . 3
 
    
      |
287 | 34, 31 | elsymgbas 17023 |
. . . 4
 
               |
288 | 33, 287 | syl 17 |
. . 3
 
    
                |
289 | 286, 288 | mpbird 236 |
. 2
 
    
          |
290 | 7, 14, 21, 28, 29, 30, 31, 37, 40, 45, 87, 285, 289 | mrcmndind 16613 |
1
 
    
    
              RHom  pmSgn             |