Step | Hyp | Ref
| Expression |
1 | | oveq1 6315 |
. . . . . . 7
 
     |
2 | 1 | fveq2d 5883 |
. . . . . 6
          
    |
3 | | oveq1 6315 |
. . . . . 6
 
             |
4 | 2, 3 | eqeq12d 2486 |
. . . . 5
     
       
      
        |
5 | 4 | imbi2d 323 |
. . . 4
     MndHom  
      
         MndHom  
      
         |
6 | | oveq1 6315 |
. . . . . . 7
 
     |
7 | 6 | fveq2d 5883 |
. . . . . 6
          
    |
8 | | oveq1 6315 |
. . . . . 6
 
             |
9 | 7, 8 | eqeq12d 2486 |
. . . . 5
     
       
      
        |
10 | 9 | imbi2d 323 |
. . . 4
     MndHom  
      
         MndHom  
      
         |
11 | | oveq1 6315 |
. . . . . . 7
   
       |
12 | 11 | fveq2d 5883 |
. . . . . 6
                   |
13 | | oveq1 6315 |
. . . . . 6
   
               |
14 | 12, 13 | eqeq12d 2486 |
. . . . 5
       
       
          
        |
15 | 14 | imbi2d 323 |
. . . 4
       MndHom  
      
         MndHom  
          
         |
16 | | oveq1 6315 |
. . . . . . 7
 
     |
17 | 16 | fveq2d 5883 |
. . . . . 6
               |
18 | | oveq1 6315 |
. . . . . 6
 
             |
19 | 17, 18 | eqeq12d 2486 |
. . . . 5
     
       
      
        |
20 | 19 | imbi2d 323 |
. . . 4
     MndHom  
      
         MndHom  
      
         |
21 | | eqid 2471 |
. . . . . . 7
         |
22 | | eqid 2471 |
. . . . . . 7
         |
23 | 21, 22 | mhm0 16668 |
. . . . . 6
  MndHom 
              |
24 | 23 | adantr 472 |
. . . . 5
   MndHom                 |
25 | | mhmmulg.b |
. . . . . . . 8
     |
26 | | mhmmulg.s |
. . . . . . . 8
.g   |
27 | 25, 21, 26 | mulg0 16841 |
. . . . . . 7
 
       |
28 | 27 | adantl 473 |
. . . . . 6
   MndHom   
       |
29 | 28 | fveq2d 5883 |
. . . . 5
   MndHom                   |
30 | | eqid 2471 |
. . . . . . . 8
         |
31 | 25, 30 | mhmf 16665 |
. . . . . . 7
  MndHom 
          |
32 | 31 | ffvelrnda 6037 |
. . . . . 6
   MndHom             |
33 | | mhmmulg.t |
. . . . . . 7
.g   |
34 | 30, 22, 33 | mulg0 16841 |
. . . . . 6
        
            |
35 | 32, 34 | syl 17 |
. . . . 5
   MndHom   
           |
36 | 24, 29, 35 | 3eqtr4d 2515 |
. . . 4
   MndHom                 |
37 | | oveq1 6315 |
. . . . . . 7
            
                                    |
38 | | mhmrcl1 16663 |
. . . . . . . . . . . 12
  MndHom 
  |
39 | 38 | ad2antrr 740 |
. . . . . . . . . . 11
    MndHom 

   |
40 | | simpr 468 |
. . . . . . . . . . 11
    MndHom 

   |
41 | | simplr 770 |
. . . . . . . . . . 11
    MndHom 

   |
42 | | eqid 2471 |
. . . . . . . . . . . 12
       |
43 | 25, 26, 42 | mulgnn0p1 16847 |
. . . . . . . . . . 11
 
                |
44 | 39, 40, 41, 43 | syl3anc 1292 |
. . . . . . . . . 10
    MndHom 

                |
45 | 44 | fveq2d 5883 |
. . . . . . . . 9
    MndHom 

                        |
46 | | simpll 768 |
. . . . . . . . . 10
    MndHom 

  MndHom    |
47 | 38 | ad2antrr 740 |
. . . . . . . . . . . 12
    MndHom 

   |
48 | | simplr 770 |
. . . . . . . . . . . 12
    MndHom 

   |
49 | | simpr 468 |
. . . . . . . . . . . 12
    MndHom 

   |
50 | 25, 26 | mulgnn0cl 16852 |
. . . . . . . . . . . 12
 
 
   |
51 | 47, 48, 49, 50 | syl3anc 1292 |
. . . . . . . . . . 11
    MndHom 

     |
52 | 51 | an32s 821 |
. . . . . . . . . 10
    MndHom 

     |
53 | | eqid 2471 |
. . . . . . . . . . 11
       |
54 | 25, 42, 53 | mhmlin 16667 |
. . . . . . . . . 10
   MndHom  

     
  
         
              |
55 | 46, 52, 41, 54 | syl3anc 1292 |
. . . . . . . . 9
    MndHom 

                                 |
56 | 45, 55 | eqtrd 2505 |
. . . . . . . 8
    MndHom 

             
              |
57 | | mhmrcl2 16664 |
. . . . . . . . . 10
  MndHom 
  |
58 | 57 | ad2antrr 740 |
. . . . . . . . 9
    MndHom 

   |
59 | 32 | adantr 472 |
. . . . . . . . 9
    MndHom 

           |
60 | 30, 33, 53 | mulgnn0p1 16847 |
. . . . . . . . 9
 
           
                        |
61 | 58, 40, 59, 60 | syl3anc 1292 |
. . . . . . . 8
    MndHom 

          
                 |
62 | 56, 61 | eqeq12d 2486 |
. . . . . . 7
    MndHom 

                                                       |
63 | 37, 62 | syl5ibr 229 |
. . . . . 6
    MndHom 

             
          
        |
64 | 63 | expcom 442 |
. . . . 5

   MndHom       
                            |
65 | 64 | a2d 28 |
. . . 4

    MndHom 
    
            MndHom 
                     |
66 | 5, 10, 15, 20, 36, 65 | nn0ind 11053 |
. . 3

   MndHom                  |
67 | 66 | 3impib 1229 |
. 2
 
 MndHom                 |
68 | 67 | 3com12 1235 |
1
   MndHom                 |