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

 
      
    
      |
2 | | simpr 467 |
. . . . . . . 8
     

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

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

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

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

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

 
      
    
  |
8 | | simplr 767 |
. . . . . . . . 9
     

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

 
      
    
                  |
10 | | ghmgrp.1 |
. . . . . . . . . . 11
       |
11 | | fof 5776 |
. . . . . . . . . . 11
           |
12 | 10, 11 | syl 17 |
. . . . . . . . . 10
       |
13 | 12 | ad5antr 745 |
. . . . . . . . 9
     

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

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

 
      
    
    |
20 | 13, 19 | ffvelrnd 6007 |
. . . . . . . 8
     

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

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

 
      
    
    |
23 | | simpr 467 |
. . . . . . . 8
 
   |
24 | | foelrni 5896 |
. . . . . . . 8
     


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

  
      |
26 | 25 | ad2antrr 737 |
. . . . . 6
    
        
      |
27 | 22, 26 | r19.29a 2900 |
. . . . 5
    
            |
28 | | simpl 463 |
. . . . . 6
 
   |
29 | | foelrni 5896 |
. . . . . 6
     


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

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

      |
32 | | simpll 765 |
. . . . . 6
   
 
   |
33 | | simplrl 775 |
. . . . . 6
   
 
   |
34 | | simplrr 776 |
. . . . . 6
   
 
   |
35 | | simpr 467 |
. . . . . 6
   
 
   |
36 | 14 | ad2antrr 737 |
. . . . . . . . . . . . . . 15
   
 
   |
37 | 36 | ad5antr 745 |
. . . . . . . . . . . . . 14
        
       
      
    
  |
38 | | simp-6r 786 |
. . . . . . . . . . . . . 14
        
       
      
    
  |
39 | | simp-4r 782 |
. . . . . . . . . . . . . 14
        
       
      
    
  |
40 | | simplr 767 |
. . . . . . . . . . . . . 14
        
       
      
    
  |
41 | 16, 17 | mndass 16557 |
. . . . . . . . . . . . . 14
  
    
       |
42 | 37, 38, 39, 40, 41 | syl13anc 1273 |
. . . . . . . . . . . . 13
        
       
      
    
 
        |
43 | 42 | fveq2d 5852 |
. . . . . . . . . . . 12
        
       
      
    
                  |
44 | | simp-7l 787 |
. . . . . . . . . . . . . 14
        
       
      
    
  |
45 | 44, 5 | syl3an1 1304 |
. . . . . . . . . . . . 13
         
       
      
                        |
46 | 37, 38, 39, 18 | syl3anc 1271 |
. . . . . . . . . . . . 13
        
       
      
    
    |
47 | 45, 46, 40 | mhmlem 16817 |
. . . . . . . . . . . 12
        
       
      
    
            
         |
48 | 16, 17 | mndcl 16556 |
. . . . . . . . . . . . . 14
 
     |
49 | 37, 39, 40, 48 | syl3anc 1271 |
. . . . . . . . . . . . 13
        
       
      
    
    |
50 | 45, 38, 49 | mhmlem 16817 |
. . . . . . . . . . . 12
        
       
      
    
    
                 |
51 | 43, 47, 50 | 3eqtr3d 2494 |
. . . . . . . . . . 11
        
       
      
    
                          |
52 | | simp1 1009 |
. . . . . . . . . . . . . . 15
 

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

                   |
54 | | simp2 1010 |
. . . . . . . . . . . . . 14
 

  |
55 | | simp3 1011 |
. . . . . . . . . . . . . 14
 

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

                  |
57 | 44, 38, 39, 56 | syl3anc 1271 |
. . . . . . . . . . . 12
        
       
      
    
                  |
58 | 57 | oveq1d 6291 |
. . . . . . . . . . 11
        
       
      
    
                              |
59 | 45, 39, 40 | mhmlem 16817 |
. . . . . . . . . . . 12
        
       
      
    
                  |
60 | 59 | oveq2d 6292 |
. . . . . . . . . . 11
        
       
      
    
        
                     |
61 | 51, 58, 60 | 3eqtr3d 2494 |
. . . . . . . . . 10
        
       
      
    
                                  |
62 | | simp-5r 784 |
. . . . . . . . . . . 12
        
       
      
    
      |
63 | | simpllr 774 |
. . . . . . . . . . . 12
        
       
      
    
      |
64 | 62, 63 | oveq12d 6294 |
. . . . . . . . . . 11
        
       
      
    
          
   |
65 | | simpr 467 |
. . . . . . . . . . 11
        
       
      
    
      |
66 | 64, 65 | oveq12d 6294 |
. . . . . . . . . 10
        
       
      
    
                 
    |
67 | 63, 65 | oveq12d 6294 |
. . . . . . . . . . 11
        
       
      
    
          
   |
68 | 62, 67 | oveq12d 6294 |
. . . . . . . . . 10
        
       
      
    
                      |
69 | 61, 66, 68 | 3eqtr3d 2494 |
. . . . . . . . 9
        
       
      
    
    
     |
70 | | foelrni 5896 |
. . . . . . . . . . . 12
     


      |
71 | 10, 70 | sylan 478 |
. . . . . . . . . . 11
 
 
      |
72 | 71 | 3ad2antr3 1176 |
. . . . . . . . . 10
 

  
      |
73 | 72 | ad4antr 743 |
. . . . . . . . 9
     

 
      
    

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

 
      
    
    
     |
75 | 25 | 3adantr3 1170 |
. . . . . . . . 9
 

  
      |
76 | 75 | ad2antrr 737 |
. . . . . . . 8
    
        
      |
77 | 74, 76 | r19.29a 2900 |
. . . . . . 7
    
                  |
78 | 30 | 3adantr3 1170 |
. . . . . . 7
 

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

            |
80 | 32, 33, 34, 35, 79 | syl13anc 1273 |
. . . . 5
   
 
           |
81 | 80 | ralrimiva 2790 |
. . . 4
 

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

                 |
83 | 82 | ralrimivva 2795 |
. 2
  
               |
84 | | eqid 2452 |
. . . . . 6
         |
85 | 16, 84 | mndidcl 16565 |
. . . . 5
       |
86 | 14, 85 | syl 17 |
. . . 4
       |
87 | 12, 86 | ffvelrnd 6007 |
. . 3
           |
88 | | simplll 773 |
. . . . . . . . . 10
   


    
  |
89 | 88, 5 | syl3an1 1304 |
. . . . . . . . 9
      
                        |
90 | 14 | ad3antrrr 741 |
. . . . . . . . . 10
   


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


    
      |
92 | | simplr 767 |
. . . . . . . . 9
   


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


    
                          |
94 | 16, 17, 84 | mndlid 16568 |
. . . . . . . . . 10
 
         |
95 | 90, 92, 94 | syl2anc 671 |
. . . . . . . . 9
   


    
        |
96 | 95 | fveq2d 5852 |
. . . . . . . 8
   


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


    
                    |
98 | | simpr 467 |
. . . . . . . 8
   


    
      |
99 | 98 | oveq2d 6292 |
. . . . . . 7
   


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


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


    
                          |
102 | 16, 17, 84 | mndrid 16569 |
. . . . . . . . . 10
 
         |
103 | 90, 92, 102 | syl2anc 671 |
. . . . . . . . 9
   


    
        |
104 | 103 | fveq2d 5852 |
. . . . . . . 8
   


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


    
                    |
106 | 98 | oveq1d 6291 |
. . . . . . 7
   


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


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


    
                        |
109 | 10, 29 | sylan 478 |
. . . . 5
 
 
      |
110 | 108, 109 | r19.29a 2900 |
. . . 4
 
          

             |
111 | 110 | ralrimiva 2790 |
. . 3
                          |
112 | | oveq1 6283 |
. . . . . . 7
        
              |
113 | 112 | eqeq1d 2454 |
. . . . . 6
        
                |
114 | | oveq2 6284 |
. . . . . . 7
        
  
           |
115 | 114 | eqeq1d 2454 |
. . . . . 6
        
                |
116 | 113, 115 | anbi12d 722 |
. . . . 5
        
      
                         |
117 | 116 | ralbidv 2810 |
. . . 4
        
 
     

                         |
118 | 117 | rspcev 3118 |
. . 3
          
         

            

        |
119 | 87, 111, 118 | syl2anc 671 |
. 2
  
        |
120 | | ghmgrp.y |
. . 3
     |
121 | | ghmgrp.q |
. . 3
    |
122 | 120, 121 | ismnd 16550 |
. 2

 

   
         

         |
123 | 83, 119, 122 | sylanbrc 675 |
1
   |