Step | Hyp | Ref
| Expression |
1 | | simpllr 534 |
. . . . . . . 8
     

 
      
    
      |
2 | | simpr 110 |
. . . . . . . 8
     

 
      
    
      |
3 | 1, 2 | oveq12d 5886 |
. . . . . . 7
     

 
      
    
          
   |
4 | | simp-5l 543 |
. . . . . . . . . 10
     

 
      
    
  |
5 | | ghmgrp.f |
. . . . . . . . . 10
 

                  |
6 | 4, 5 | syl3an1 1271 |
. . . . . . . . 9
       
 
     
     

                  |
7 | | simp-4r 542 |
. . . . . . . . 9
     

 
      
    
  |
8 | | simplr 528 |
. . . . . . . . 9
     

 
      
    
  |
9 | 6, 7, 8 | mhmlem 12854 |
. . . . . . . 8
     

 
      
    
                  |
10 | | ghmgrp.1 |
. . . . . . . . . . 11
       |
11 | | fof 5433 |
. . . . . . . . . . 11
           |
12 | 10, 11 | syl 14 |
. . . . . . . . . 10
       |
13 | 12 | ad5antr 496 |
. . . . . . . . 9
     

 
      
    
      |
14 | | mhmmnd.3 |
. . . . . . . . . . 11
   |
15 | 14 | ad5antr 496 |
. . . . . . . . . 10
     

 
      
    
  |
16 | | ghmgrp.x |
. . . . . . . . . . 11
     |
17 | | ghmgrp.p |
. . . . . . . . . . 11
    |
18 | 16, 17 | mndcl 12703 |
. . . . . . . . . 10
 
     |
19 | 15, 7, 8, 18 | syl3anc 1238 |
. . . . . . . . 9
     

 
      
    
    |
20 | 13, 19 | ffvelcdmd 5647 |
. . . . . . . 8
     

 
      
    
        |
21 | 9, 20 | eqeltrrd 2255 |
. . . . . . 7
     

 
      
    
            |
22 | 3, 21 | eqeltrrd 2255 |
. . . . . 6
     

 
      
    
    |
23 | | simpr 110 |
. . . . . . . 8
 
   |
24 | | foelcdmi 5563 |
. . . . . . . 8
     


      |
25 | 10, 23, 24 | syl2an 289 |
. . . . . . 7
 

  
      |
26 | 25 | ad2antrr 488 |
. . . . . 6
    
        
      |
27 | 22, 26 | r19.29a 2620 |
. . . . 5
    
            |
28 | | simpl 109 |
. . . . . 6
 
   |
29 | | foelcdmi 5563 |
. . . . . 6
     


      |
30 | 10, 28, 29 | syl2an 289 |
. . . . 5
 

  
      |
31 | 27, 30 | r19.29a 2620 |
. . . 4
 

      |
32 | | simpll 527 |
. . . . . 6
   
 
   |
33 | | simplrl 535 |
. . . . . 6
   
 
   |
34 | | simplrr 536 |
. . . . . 6
   
 
   |
35 | | simpr 110 |
. . . . . 6
   
 
   |
36 | 14 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
   
 
   |
37 | 36 | ad5antr 496 |
. . . . . . . . . . . . . 14
        
       
      
    
  |
38 | | simp-6r 546 |
. . . . . . . . . . . . . 14
        
       
      
    
  |
39 | | simp-4r 542 |
. . . . . . . . . . . . . 14
        
       
      
    
  |
40 | | simplr 528 |
. . . . . . . . . . . . . 14
        
       
      
    
  |
41 | 16, 17 | mndass 12704 |
. . . . . . . . . . . . . 14
  
    
       |
42 | 37, 38, 39, 40, 41 | syl13anc 1240 |
. . . . . . . . . . . . 13
        
       
      
    
 
        |
43 | 42 | fveq2d 5514 |
. . . . . . . . . . . 12
        
       
      
    
                  |
44 | | simp-7l 547 |
. . . . . . . . . . . . . 14
        
       
      
    
  |
45 | 44, 5 | syl3an1 1271 |
. . . . . . . . . . . . 13
         
       
      
                        |
46 | 37, 38, 39, 18 | syl3anc 1238 |
. . . . . . . . . . . . 13
        
       
      
    
    |
47 | 45, 46, 40 | mhmlem 12854 |
. . . . . . . . . . . 12
        
       
      
    
            
         |
48 | 16, 17 | mndcl 12703 |
. . . . . . . . . . . . . 14
 
     |
49 | 37, 39, 40, 48 | syl3anc 1238 |
. . . . . . . . . . . . 13
        
       
      
    
    |
50 | 45, 38, 49 | mhmlem 12854 |
. . . . . . . . . . . 12
        
       
      
    
    
                 |
51 | 43, 47, 50 | 3eqtr3d 2218 |
. . . . . . . . . . 11
        
       
      
    
                          |
52 | | simp1 997 |
. . . . . . . . . . . . . . 15
 

  |
53 | 52, 5 | syl3an1 1271 |
. . . . . . . . . . . . . 14
  

                   |
54 | | simp2 998 |
. . . . . . . . . . . . . 14
 

  |
55 | | simp3 999 |
. . . . . . . . . . . . . 14
 

  |
56 | 53, 54, 55 | mhmlem 12854 |
. . . . . . . . . . . . 13
 

                  |
57 | 44, 38, 39, 56 | syl3anc 1238 |
. . . . . . . . . . . 12
        
       
      
    
                  |
58 | 57 | oveq1d 5883 |
. . . . . . . . . . 11
        
       
      
    
                              |
59 | 45, 39, 40 | mhmlem 12854 |
. . . . . . . . . . . 12
        
       
      
    
                  |
60 | 59 | oveq2d 5884 |
. . . . . . . . . . 11
        
       
      
    
        
                     |
61 | 51, 58, 60 | 3eqtr3d 2218 |
. . . . . . . . . 10
        
       
      
    
                                  |
62 | | simp-5r 544 |
. . . . . . . . . . . 12
        
       
      
    
      |
63 | | simpllr 534 |
. . . . . . . . . . . 12
        
       
      
    
      |
64 | 62, 63 | oveq12d 5886 |
. . . . . . . . . . 11
        
       
      
    
          
   |
65 | | simpr 110 |
. . . . . . . . . . 11
        
       
      
    
      |
66 | 64, 65 | oveq12d 5886 |
. . . . . . . . . 10
        
       
      
    
                 
    |
67 | 63, 65 | oveq12d 5886 |
. . . . . . . . . . 11
        
       
      
    
          
   |
68 | 62, 67 | oveq12d 5886 |
. . . . . . . . . 10
        
       
      
    
                      |
69 | 61, 66, 68 | 3eqtr3d 2218 |
. . . . . . . . 9
        
       
      
    
    
     |
70 | | foelcdmi 5563 |
. . . . . . . . . . . 12
     


      |
71 | 10, 70 | sylan 283 |
. . . . . . . . . . 11
 
 
      |
72 | 71 | 3ad2antr3 1164 |
. . . . . . . . . 10
 

  
      |
73 | 72 | ad4antr 494 |
. . . . . . . . 9
     

 
      
    

      |
74 | 69, 73 | r19.29a 2620 |
. . . . . . . 8
     

 
      
    
    
     |
75 | 25 | 3adantr3 1158 |
. . . . . . . . 9
 

  
      |
76 | 75 | ad2antrr 488 |
. . . . . . . 8
    
        
      |
77 | 74, 76 | r19.29a 2620 |
. . . . . . 7
    
                  |
78 | 30 | 3adantr3 1158 |
. . . . . . 7
 

  
      |
79 | 77, 78 | r19.29a 2620 |
. . . . . 6
 

            |
80 | 32, 33, 34, 35, 79 | syl13anc 1240 |
. . . . 5
   
 
           |
81 | 80 | ralrimiva 2550 |
. . . 4
 

  
          |
82 | 31, 81 | jca 306 |
. . 3
 

                 |
83 | 82 | ralrimivva 2559 |
. 2
  
               |
84 | | eqid 2177 |
. . . . . 6
         |
85 | 16, 84 | mndidcl 12710 |
. . . . 5
       |
86 | 14, 85 | syl 14 |
. . . 4
       |
87 | 12, 86 | ffvelcdmd 5647 |
. . 3
           |
88 | | simplll 533 |
. . . . . . . . . 10
   


    
  |
89 | 88, 5 | syl3an1 1271 |
. . . . . . . . 9
      
                        |
90 | 14 | ad3antrrr 492 |
. . . . . . . . . 10
   


    
  |
91 | 90, 85 | syl 14 |
. . . . . . . . 9
   


    
      |
92 | | simplr 528 |
. . . . . . . . 9
   


    
  |
93 | 89, 91, 92 | mhmlem 12854 |
. . . . . . . 8
   


    
                          |
94 | 16, 17, 84 | mndlid 12715 |
. . . . . . . . . 10
 
         |
95 | 90, 92, 94 | syl2anc 411 |
. . . . . . . . 9
   


    
        |
96 | 95 | fveq2d 5514 |
. . . . . . . 8
   


    
                |
97 | 93, 96 | eqtr3d 2212 |
. . . . . . 7
   


    
                    |
98 | | simpr 110 |
. . . . . . . 8
   


    
      |
99 | 98 | oveq2d 5884 |
. . . . . . 7
   


    
                          |
100 | 97, 99, 98 | 3eqtr3d 2218 |
. . . . . 6
   


    
            |
101 | 89, 92, 91 | mhmlem 12854 |
. . . . . . . 8
   


    
                          |
102 | 16, 17, 84 | mndrid 12716 |
. . . . . . . . . 10
 
         |
103 | 90, 92, 102 | syl2anc 411 |
. . . . . . . . 9
   


    
        |
104 | 103 | fveq2d 5514 |
. . . . . . . 8
   


    
                |
105 | 101, 104 | eqtr3d 2212 |
. . . . . . 7
   


    
                    |
106 | 98 | oveq1d 5883 |
. . . . . . 7
   


    
                          |
107 | 105, 106,
98 | 3eqtr3d 2218 |
. . . . . 6
   


    
            |
108 | 100, 107 | jca 306 |
. . . . 5
   


    
                        |
109 | 10, 29 | sylan 283 |
. . . . 5
 
 
      |
110 | 108, 109 | r19.29a 2620 |
. . . 4
 
          

             |
111 | 110 | ralrimiva 2550 |
. . 3
                          |
112 | | oveq1 5875 |
. . . . . 6
        
              |
113 | 112 | eqeq1d 2186 |
. . . . 5
        
                |
114 | 113 | ovanraleqv 5892 |
. . . 4
        
 
     

                         |
115 | 114 | rspcev 2841 |
. . 3
          
         

            

        |
116 | 87, 111, 115 | syl2anc 411 |
. 2
  
        |
117 | | ghmgrp.y |
. . 3
     |
118 | | ghmgrp.q |
. . 3
    |
119 | 117, 118 | ismnd 12699 |
. 2

 

   
         

         |
120 | 83, 116, 119 | sylanbrc 417 |
1
   |