Step | Hyp | Ref
| Expression |
1 | | eqid 2177 |
. . . . . . . . . . 11
         |
2 | | eqid 2177 |
. . . . . . . . . . 11
         |
3 | | opprbas.1 |
. . . . . . . . . . 11
oppr   |
4 | | eqid 2177 |
. . . . . . . . . . 11
         |
5 | 1, 2, 3, 4 | opprmulg 13055 |
. . . . . . . . . 10
 
                           |
6 | 5 | 3expa 1203 |
. . . . . . . . 9
  
         
                  |
7 | 6 | eqeq1d 2186 |
. . . . . . . 8
  
         
        
           |
8 | | simpll 527 |
. . . . . . . . . 10
  
         
  |
9 | | simpr 110 |
. . . . . . . . . 10
  
         
      |
10 | | simplr 528 |
. . . . . . . . . 10
  
         
      |
11 | 1, 2, 3, 4 | opprmulg 13055 |
. . . . . . . . . 10
 
                           |
12 | 8, 9, 10, 11 | syl3anc 1238 |
. . . . . . . . 9
  
         
                  |
13 | 12 | eqeq1d 2186 |
. . . . . . . 8
  
         
        
           |
14 | 7, 13 | anbi12d 473 |
. . . . . . 7
  
         
                                        |
15 | 14 | biancomd 271 |
. . . . . 6
  
         
                                        |
16 | 15 | ralbidva 2473 |
. . . . 5
 
                             
                           |
17 | 16 | riotabidva 5840 |
. . . 4
                                        
                          |
18 | | df-riota 5824 |
. . . 4
                                        
                          |
19 | | df-riota 5824 |
. . . 4
                                        
                          |
20 | 17, 18, 19 | 3eqtr3g 2233 |
. . 3
        
                                                              |
21 | 3 | opprex 13057 |
. . . . 5
   |
22 | | eqid 2177 |
. . . . . 6
mulGrp  mulGrp   |
23 | 22 | mgpex 12949 |
. . . . 5
 mulGrp    |
24 | | eqid 2177 |
. . . . . 6
   mulGrp      mulGrp    |
25 | | eqid 2177 |
. . . . . 6
  mulGrp     mulGrp    |
26 | | eqid 2177 |
. . . . . 6
   mulGrp      mulGrp    |
27 | 24, 25, 26 | grpidvalg 12671 |
. . . . 5
 mulGrp     mulGrp          mulGrp  
    mulGrp         mulGrp         mulGrp          |
28 | 21, 23, 27 | 3syl 17 |
. . . 4
    mulGrp          mulGrp       mulGrp         mulGrp         mulGrp          |
29 | 3, 1 | opprbasg 13059 |
. . . . . . . 8
           |
30 | | eqid 2177 |
. . . . . . . . . 10
         |
31 | 22, 30 | mgpbasg 12950 |
. . . . . . . . 9
        mulGrp     |
32 | 21, 31 | syl 14 |
. . . . . . . 8
        mulGrp     |
33 | 29, 32 | eqtrd 2210 |
. . . . . . 7
        mulGrp     |
34 | 33 | eleq2d 2247 |
. . . . . 6
     
   mulGrp      |
35 | 22, 4 | mgpplusgg 12948 |
. . . . . . . . . . 11
       mulGrp     |
36 | 21, 35 | syl 14 |
. . . . . . . . . 10
       mulGrp     |
37 | 36 | oveqd 5885 |
. . . . . . . . 9
             mulGrp       |
38 | 37 | eqeq1d 2186 |
. . . . . . . 8
         
  
 mulGrp        |
39 | 36 | oveqd 5885 |
. . . . . . . . 9
             mulGrp       |
40 | 39 | eqeq1d 2186 |
. . . . . . . 8
         
  
 mulGrp        |
41 | 38, 40 | anbi12d 473 |
. . . . . . 7
                         mulGrp         mulGrp         |
42 | 33, 41 | raleqbidv 2684 |
. . . . . 6
  
                       
   mulGrp         mulGrp         mulGrp         |
43 | 34, 42 | anbi12d 473 |
. . . . 5
                               
    mulGrp       mulGrp         mulGrp         mulGrp          |
44 | 43 | iotabidv 5194 |
. . . 4
        
                                 mulGrp   
   mulGrp         mulGrp         mulGrp          |
45 | 28, 44 | eqtr4d 2213 |
. . 3
    mulGrp          
                            |
46 | | eqid 2177 |
. . . . . 6
mulGrp  mulGrp   |
47 | 46 | mgpex 12949 |
. . . . 5
 mulGrp    |
48 | | eqid 2177 |
. . . . . 6
   mulGrp      mulGrp    |
49 | | eqid 2177 |
. . . . . 6
  mulGrp     mulGrp    |
50 | | eqid 2177 |
. . . . . 6
   mulGrp      mulGrp    |
51 | 48, 49, 50 | grpidvalg 12671 |
. . . . 5
 mulGrp     mulGrp          mulGrp  
    mulGrp         mulGrp         mulGrp          |
52 | 47, 51 | syl 14 |
. . . 4
    mulGrp          mulGrp       mulGrp         mulGrp         mulGrp          |
53 | 46, 1 | mgpbasg 12950 |
. . . . . . 7
        mulGrp     |
54 | 53 | eleq2d 2247 |
. . . . . 6
     
   mulGrp      |
55 | 46, 2 | mgpplusgg 12948 |
. . . . . . . . . 10
       mulGrp     |
56 | 55 | oveqd 5885 |
. . . . . . . . 9
             mulGrp       |
57 | 56 | eqeq1d 2186 |
. . . . . . . 8
         
  
 mulGrp        |
58 | 55 | oveqd 5885 |
. . . . . . . . 9
             mulGrp       |
59 | 58 | eqeq1d 2186 |
. . . . . . . 8
         
  
 mulGrp        |
60 | 57, 59 | anbi12d 473 |
. . . . . . 7
                         mulGrp         mulGrp         |
61 | 53, 60 | raleqbidv 2684 |
. . . . . 6
  
                       
   mulGrp         mulGrp         mulGrp         |
62 | 54, 61 | anbi12d 473 |
. . . . 5
                               
    mulGrp       mulGrp         mulGrp         mulGrp          |
63 | 62 | iotabidv 5194 |
. . . 4
        
                                 mulGrp   
   mulGrp         mulGrp         mulGrp          |
64 | 52, 63 | eqtr4d 2213 |
. . 3
    mulGrp          
                            |
65 | 20, 45, 64 | 3eqtr4d 2220 |
. 2
    mulGrp      mulGrp     |
66 | | eqid 2177 |
. . . 4
         |
67 | 22, 66 | ringidvalg 12957 |
. . 3
        mulGrp     |
68 | 21, 67 | syl 14 |
. 2
        mulGrp     |
69 | | oppr1.2 |
. . 3
     |
70 | 46, 69 | ringidvalg 12957 |
. 2
    mulGrp     |
71 | 65, 68, 70 | 3eqtr4rd 2221 |
1
       |