Step | Hyp | Ref
| Expression |
1 | | elxp2 4871 |
. . 3
  
 
     |
2 | | frgpuptinv.m |
. . . . . . . . . 10
 
       |
3 | 2 | efgmval 17411 |
. . . . . . . . 9
 
            |
4 | 3 | adantl 472 |
. . . . . . . 8
 

             |
5 | 4 | fveq2d 5892 |
. . . . . . 7
 

                     |
6 | | df-ov 6318 |
. . . . . . 7
                |
7 | 5, 6 | syl6eqr 2514 |
. . . . . 6
 

                  |
8 | | elpri 3997 |
. . . . . . . . 9
        |
9 | | df2o3 7221 |
. . . . . . . . 9
    |
10 | 8, 9 | eleq2s 2558 |
. . . . . . . 8
     |
11 | | simpr 467 |
. . . . . . . . . . . 12
 
   |
12 | | 1on 7215 |
. . . . . . . . . . . . . . 15
 |
13 | 12 | elexi 3067 |
. . . . . . . . . . . . . 14
 |
14 | 13 | prid2 4094 |
. . . . . . . . . . . . 13
 
  |
15 | 14, 9 | eleqtrri 2539 |
. . . . . . . . . . . 12
 |
16 | | 1n0 7223 |
. . . . . . . . . . . . . . . 16
 |
17 | | neeq1 2698 |
. . . . . . . . . . . . . . . 16
 
   |
18 | 16, 17 | mpbiri 241 |
. . . . . . . . . . . . . . 15
   |
19 | | ifnefalse 3905 |
. . . . . . . . . . . . . . 15

                           |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . 14
                            |
21 | | fveq2 5888 |
. . . . . . . . . . . . . . 15
           |
22 | 21 | fveq2d 5892 |
. . . . . . . . . . . . . 14
                   |
23 | 20, 22 | sylan9eqr 2518 |
. . . . . . . . . . . . 13
 
                            |
24 | | frgpup.t |
. . . . . . . . . . . . 13
 
                   |
25 | | fvex 5898 |
. . . . . . . . . . . . 13
         |
26 | 23, 24, 25 | ovmpt2a 6454 |
. . . . . . . . . . . 12
                 |
27 | 11, 15, 26 | sylancl 673 |
. . . . . . . . . . 11
 
               |
28 | | 0ex 4549 |
. . . . . . . . . . . . . . 15
 |
29 | 28 | prid1 4093 |
. . . . . . . . . . . . . 14
    |
30 | 29, 9 | eleqtrri 2539 |
. . . . . . . . . . . . 13
 |
31 | | iftrue 3899 |
. . . . . . . . . . . . . . 15

                       |
32 | 31, 21 | sylan9eqr 2518 |
. . . . . . . . . . . . . 14
 
                        |
33 | | fvex 5898 |
. . . . . . . . . . . . . 14
     |
34 | 32, 24, 33 | ovmpt2a 6454 |
. . . . . . . . . . . . 13
      
      |
35 | 11, 30, 34 | sylancl 673 |
. . . . . . . . . . . 12
 
           |
36 | 35 | fveq2d 5892 |
. . . . . . . . . . 11
 
                   |
37 | 27, 36 | eqtr4d 2499 |
. . . . . . . . . 10
 
               |
38 | | difeq2 3557 |
. . . . . . . . . . . . 13

      |
39 | | dif0 3849 |
. . . . . . . . . . . . 13
   |
40 | 38, 39 | syl6eq 2512 |
. . . . . . . . . . . 12

    |
41 | 40 | oveq2d 6331 |
. . . . . . . . . . 11

            |
42 | | oveq2 6323 |
. . . . . . . . . . . 12

          |
43 | 42 | fveq2d 5892 |
. . . . . . . . . . 11

                  |
44 | 41, 43 | eqeq12d 2477 |
. . . . . . . . . 10

              
               |
45 | 37, 44 | syl5ibrcom 230 |
. . . . . . . . 9
 
                   |
46 | 37 | fveq2d 5892 |
. . . . . . . . . . 11
 
                       |
47 | | frgpup.h |
. . . . . . . . . . . . 13
   |
48 | 47 | adantr 471 |
. . . . . . . . . . . 12
 
   |
49 | | frgpup.a |
. . . . . . . . . . . . . 14
       |
50 | 49 | ffvelrnda 6045 |
. . . . . . . . . . . . 13
 
       |
51 | 35, 50 | eqeltrd 2540 |
. . . . . . . . . . . 12
 
       |
52 | | frgpup.b |
. . . . . . . . . . . . 13
     |
53 | | frgpup.n |
. . . . . . . . . . . . 13
      |
54 | 52, 53 | grpinvinv 16770 |
. . . . . . . . . . . 12
     
                   |
55 | 48, 51, 54 | syl2anc 671 |
. . . . . . . . . . 11
 
                   |
56 | 46, 55 | eqtr2d 2497 |
. . . . . . . . . 10
 
               |
57 | | difeq2 3557 |
. . . . . . . . . . . . 13
       |
58 | | difid 3847 |
. . . . . . . . . . . . 13
   |
59 | 57, 58 | syl6eq 2512 |
. . . . . . . . . . . 12
     |
60 | 59 | oveq2d 6331 |
. . . . . . . . . . 11
             |
61 | | oveq2 6323 |
. . . . . . . . . . . 12
           |
62 | 61 | fveq2d 5892 |
. . . . . . . . . . 11
                   |
63 | 60, 62 | eqeq12d 2477 |
. . . . . . . . . 10
               
               |
64 | 56, 63 | syl5ibrcom 230 |
. . . . . . . . 9
 
                   |
65 | 45, 64 | jaod 386 |
. . . . . . . 8
 
                     |
66 | 10, 65 | syl5 33 |
. . . . . . 7
 
                   |
67 | 66 | impr 629 |
. . . . . 6
 

                  |
68 | 7, 67 | eqtrd 2496 |
. . . . 5
 

                    |
69 | | fveq2 5888 |
. . . . . . . 8
                 |
70 | | df-ov 6318 |
. . . . . . . 8
            |
71 | 69, 70 | syl6eqr 2514 |
. . . . . . 7
              |
72 | 71 | fveq2d 5892 |
. . . . . 6
                      |
73 | | fveq2 5888 |
. . . . . . . 8
                 |
74 | | df-ov 6318 |
. . . . . . . 8
            |
75 | 73, 74 | syl6eqr 2514 |
. . . . . . 7
              |
76 | 75 | fveq2d 5892 |
. . . . . 6
                      |
77 | 72, 76 | eqeq12d 2477 |
. . . . 5
                                        |
78 | 68, 77 | syl5ibrcom 230 |
. . . 4
 

                         |
79 | 78 | rexlimdvva 2898 |
. . 3
                          |
80 | 1, 79 | syl5bi 225 |
. 2
                       |
81 | 80 | imp 435 |
1
 

                    |