Step | Hyp | Ref
| Expression |
1 | | fvex 5802 |
. . . . . . . . 9
     |
2 | 1 | rabex 4544 |
. . . . . . . 8
             
 |
3 | | simp2l 1014 |
. . . . . . . . . . 11
   IDomn   SubGrp  SubGrp  
           SubGrp    |
4 | | eqid 2451 |
. . . . . . . . . . . 12
         |
5 | 4 | subgss 15793 |
. . . . . . . . . . 11
 SubGrp 
      |
6 | 3, 5 | syl 16 |
. . . . . . . . . 10
   IDomn   SubGrp  SubGrp  
                 |
7 | | simpl2l 1041 |
. . . . . . . . . . . 12
    IDomn
  SubGrp 
SubGrp              
SubGrp    |
8 | | simp3l 1016 |
. . . . . . . . . . . . . . 15
   IDomn   SubGrp  SubGrp  
                 |
9 | | simp1r 1013 |
. . . . . . . . . . . . . . . 16
   IDomn   SubGrp  SubGrp  
             |
10 | 9 | nnnn0d 10740 |
. . . . . . . . . . . . . . 15
   IDomn   SubGrp  SubGrp  
             |
11 | 8, 10 | eqeltrd 2539 |
. . . . . . . . . . . . . 14
   IDomn   SubGrp  SubGrp  
                 |
12 | | vex 3074 |
. . . . . . . . . . . . . . 15
 |
13 | | hashclb 12238 |
. . . . . . . . . . . . . . 15
 
       |
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . . . . . 14

      |
15 | 11, 14 | sylibr 212 |
. . . . . . . . . . . . 13
   IDomn   SubGrp  SubGrp  
             |
16 | 15 | adantr 465 |
. . . . . . . . . . . 12
    IDomn
  SubGrp 
SubGrp              
  |
17 | | simpr 461 |
. . . . . . . . . . . 12
    IDomn
  SubGrp 
SubGrp              
  |
18 | | eqid 2451 |
. . . . . . . . . . . . 13
         |
19 | 18 | odsubdvds 16183 |
. . . . . . . . . . . 12
  SubGrp                 |
20 | 7, 16, 17, 19 | syl3anc 1219 |
. . . . . . . . . . 11
    IDomn
  SubGrp 
SubGrp              
              |
21 | 8 | adantr 465 |
. . . . . . . . . . 11
    IDomn
  SubGrp 
SubGrp              
      |
22 | 20, 21 | breqtrd 4417 |
. . . . . . . . . 10
    IDomn
  SubGrp 
SubGrp              
          |
23 | 6, 22 | ssrabdv 3532 |
. . . . . . . . 9
   IDomn   SubGrp  SubGrp  
                           |
24 | | simp2r 1015 |
. . . . . . . . . . 11
   IDomn   SubGrp  SubGrp  
           SubGrp    |
25 | 4 | subgss 15793 |
. . . . . . . . . . 11
 SubGrp 
      |
26 | 24, 25 | syl 16 |
. . . . . . . . . 10
   IDomn   SubGrp  SubGrp  
                 |
27 | | simpl2r 1042 |
. . . . . . . . . . . 12
    IDomn
  SubGrp 
SubGrp              
SubGrp    |
28 | | simp3r 1017 |
. . . . . . . . . . . . . . 15
   IDomn   SubGrp  SubGrp  
                 |
29 | 28, 10 | eqeltrd 2539 |
. . . . . . . . . . . . . 14
   IDomn   SubGrp  SubGrp  
                 |
30 | | vex 3074 |
. . . . . . . . . . . . . . 15
 |
31 | | hashclb 12238 |
. . . . . . . . . . . . . . 15
 
       |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . . . . 14

      |
33 | 29, 32 | sylibr 212 |
. . . . . . . . . . . . 13
   IDomn   SubGrp  SubGrp  
             |
34 | 33 | adantr 465 |
. . . . . . . . . . . 12
    IDomn
  SubGrp 
SubGrp              
  |
35 | | simpr 461 |
. . . . . . . . . . . 12
    IDomn
  SubGrp 
SubGrp              
  |
36 | 18 | odsubdvds 16183 |
. . . . . . . . . . . 12
  SubGrp                 |
37 | 27, 34, 35, 36 | syl3anc 1219 |
. . . . . . . . . . 11
    IDomn
  SubGrp 
SubGrp              
              |
38 | 28 | adantr 465 |
. . . . . . . . . . 11
    IDomn
  SubGrp 
SubGrp              
      |
39 | 37, 38 | breqtrd 4417 |
. . . . . . . . . 10
    IDomn
  SubGrp 
SubGrp              
          |
40 | 26, 39 | ssrabdv 3532 |
. . . . . . . . 9
   IDomn   SubGrp  SubGrp  
                           |
41 | 23, 40 | unssd 3633 |
. . . . . . . 8
   IDomn   SubGrp  SubGrp  
                             |
42 | | ssdomg 7458 |
. . . . . . . 8
                               
                   |
43 | 2, 41, 42 | mpsyl 63 |
. . . . . . 7
   IDomn   SubGrp  SubGrp  
                             |
44 | | idomsubgmo.g |
. . . . . . . . . . 11
 mulGrp  ↾s Unit    |
45 | 44, 4, 18 | idomodle 29702 |
. . . . . . . . . 10
  IDomn
                     |
46 | 45 | 3ad2ant1 1009 |
. . . . . . . . 9
   IDomn   SubGrp  SubGrp  
                               |
47 | 46, 8 | breqtrrd 4419 |
. . . . . . . 8
   IDomn   SubGrp  SubGrp  
                                   |
48 | 2 | a1i 11 |
. . . . . . . . . 10
   IDomn   SubGrp  SubGrp  
                        
  |
49 | | hashbnd 12219 |
. . . . . . . . . 10
               
   
                      
             
  |
50 | 48, 11, 47, 49 | syl3anc 1219 |
. . . . . . . . 9
   IDomn   SubGrp  SubGrp  
                        
  |
51 | | hashdom 12253 |
. . . . . . . . 9
               
                       
             
   |
52 | 50, 12, 51 | sylancl 662 |
. . . . . . . 8
   IDomn   SubGrp  SubGrp  
                                 
             
   |
53 | 47, 52 | mpbid 210 |
. . . . . . 7
   IDomn   SubGrp  SubGrp  
                        
  |
54 | | domtr 7465 |
. . . . . . 7
                 
             
     |
55 | 43, 53, 54 | syl2anc 661 |
. . . . . 6
   IDomn   SubGrp  SubGrp  
               |
56 | 12, 30 | unex 6481 |
. . . . . . 7
   |
57 | | ssun1 3620 |
. . . . . . 7
   |
58 | | ssdomg 7458 |
. . . . . . 7
   
       |
59 | 56, 57, 58 | mp2 9 |
. . . . . 6
   |
60 | | sbth 7534 |
. . . . . 6
           |
61 | 55, 59, 60 | sylancl 662 |
. . . . 5
   IDomn   SubGrp  SubGrp  
               |
62 | 8, 28 | eqtr4d 2495 |
. . . . . . 7
   IDomn   SubGrp  SubGrp  
                     |
63 | | hashen 12228 |
. . . . . . . 8
 
         
   |
64 | 15, 33, 63 | syl2anc 661 |
. . . . . . 7
   IDomn   SubGrp  SubGrp  
                       |
65 | 62, 64 | mpbid 210 |
. . . . . 6
   IDomn   SubGrp  SubGrp  
             |
66 | | fiuneneq 29703 |
. . . . . 6
 
       |
67 | 65, 15, 66 | syl2anc 661 |
. . . . 5
   IDomn   SubGrp  SubGrp  
             
   |
68 | 61, 67 | mpbid 210 |
. . . 4
   IDomn   SubGrp  SubGrp  
             |
69 | 68 | 3expia 1190 |
. . 3
   IDomn   SubGrp  SubGrp                  |
70 | 69 | ralrimivva 2907 |
. 2
  IDomn
  SubGrp   
SubGrp                 |
71 | | fveq2 5792 |
. . . 4
           |
72 | 71 | eqeq1d 2453 |
. . 3
     
       |
73 | 72 | rmo4 3252 |
. 2
  SubGrp       
SubGrp    SubGrp                 |
74 | 70, 73 | sylibr 212 |
1
  IDomn
 
SubGrp         |