Step | Hyp | Ref
| Expression |
1 | | raldifsni 4102 |
. . . . 5
 
                                      
                
                    
   |
2 | | simpll1 1047 |
. . . . . . . . . . . . . . . 16
         
          
      finSupp     |
3 | | simprll 772 |
. . . . . . . . . . . . . . . 16
         
          
      finSupp         |
4 | | ffvelrn 6020 |
. . . . . . . . . . . . . . . . . 18
     
       |
5 | 4 | 3ad2antl3 1172 |
. . . . . . . . . . . . . . . . 17
        
      |
6 | 5 | adantr 467 |
. . . . . . . . . . . . . . . 16
         
          
      finSupp         |
7 | | islindf4.b |
. . . . . . . . . . . . . . . . 17
     |
8 | | islindf4.r |
. . . . . . . . . . . . . . . . 17
Scalar   |
9 | | islindf4.t |
. . . . . . . . . . . . . . . . 17
     |
10 | | eqid 2451 |
. . . . . . . . . . . . . . . . 17
           |
11 | | eqid 2451 |
. . . . . . . . . . . . . . . . 17
           |
12 | | eqid 2451 |
. . . . . . . . . . . . . . . . 17
         |
13 | 7, 8, 9, 10, 11, 12 | lmodvsinv 18259 |
. . . . . . . . . . . . . . . 16
     
    
         
             
        |
14 | 2, 3, 6, 13 | syl3anc 1268 |
. . . . . . . . . . . . . . 15
         
          
      finSupp            
             
        |
15 | 14 | eqeq1d 2453 |
. . . . . . . . . . . . . 14
         
          
      finSupp                    g    
                      g    
         |
16 | | lmodgrp 18098 |
. . . . . . . . . . . . . . . 16

  |
17 | 2, 16 | syl 17 |
. . . . . . . . . . . . . . 15
         
          
      finSupp     |
18 | 7, 8, 9, 12 | lmodvscl 18108 |
. . . . . . . . . . . . . . . 16
     
    
        |
19 | 2, 3, 6, 18 | syl3anc 1268 |
. . . . . . . . . . . . . . 15
         
          
      finSupp   
       |
20 | | islindf4.z |
. . . . . . . . . . . . . . . 16
     |
21 | | lmodcmn 18136 |
. . . . . . . . . . . . . . . . 17

CMnd |
22 | 2, 21 | syl 17 |
. . . . . . . . . . . . . . . 16
         
          
      finSupp   CMnd |
23 | | simpll2 1048 |
. . . . . . . . . . . . . . . . 17
         
          
      finSupp     |
24 | | difexg 4551 |
. . . . . . . . . . . . . . . . 17
 
     |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . 16
         
          
      finSupp   
     |
26 | | simprlr 773 |
. . . . . . . . . . . . . . . . . 18
         
          
      finSupp       
       |
27 | | elmapi 7493 |
. . . . . . . . . . . . . . . . . 18
      
                  |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
         
          
      finSupp                 |
29 | | simpll3 1049 |
. . . . . . . . . . . . . . . . . 18
         
          
      finSupp         |
30 | | difss 3560 |
. . . . . . . . . . . . . . . . . 18
   
 |
31 | | fssres 5749 |
. . . . . . . . . . . . . . . . . 18
      
   
                |
32 | 29, 30, 31 | sylancl 668 |
. . . . . . . . . . . . . . . . 17
         
          
      finSupp                   |
33 | 8, 12, 9, 7, 2, 28,
32, 25 | lcomf 18127 |
. . . . . . . . . . . . . . . 16
         
          
      finSupp     
                |
34 | | islindf4.y |
. . . . . . . . . . . . . . . . 17
     |
35 | | simprr 766 |
. . . . . . . . . . . . . . . . 17
         
          
      finSupp   finSupp   |
36 | 8, 12, 9, 7, 2, 28,
32, 25, 20, 34, 35 | lcomfsupp 18128 |
. . . . . . . . . . . . . . . 16
         
          
      finSupp     
      finSupp  |
37 | 7, 20, 22, 25, 33, 36 | gsumcl 17549 |
. . . . . . . . . . . . . . 15
         
          
      finSupp    g    
        |
38 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
       |
39 | 7, 38, 20, 10 | grpinvid2 16715 |
. . . . . . . . . . . . . . 15
        
g    
                        g    
        g    
                    |
40 | 17, 19, 37, 39 | syl3anc 1268 |
. . . . . . . . . . . . . 14
         
          
      finSupp            
       g          
  g    
                    |
41 | | simplr 762 |
. . . . . . . . . . . . . . . . . . 19
         
          
      finSupp     |
42 | | fsnunf2 6103 |
. . . . . . . . . . . . . . . . . . 19
             
    
                 |
43 | 28, 41, 3, 42 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . 18
         
          
      finSupp                    |
44 | 8, 12, 9, 7, 2, 43,
29, 23 | lcomf 18127 |
. . . . . . . . . . . . . . . . 17
         
          
      finSupp                   |
45 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
  |
46 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . . 23
          
            |
47 | 45, 46 | anim12i 570 |
. . . . . . . . . . . . . . . . . . . . . 22
         
    
    
       
       |
48 | | elmapfun 7495 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
      |
49 | | fdm 5733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
            
      |
50 | | neldifsnd 4100 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
      |
51 | | df-nel 2625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

  |
52 | | eleq2 2518 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    


      |
53 | 52 | notbid 296 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    

       |
54 | 51, 53 | syl5bb 261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    

       |
55 | 50, 54 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
  |
56 | 49, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
            
  |
57 | 27, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
   
  |
58 | 48, 57 | jca 535 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
    
   |
59 | 58 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . 23
          
      
   |
60 | 59 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
         
    
    
       
   |
61 | 47, 60 | jca 535 |
. . . . . . . . . . . . . . . . . . . . 21
         
    
    
              
    |
62 | | funsnfsupp 7907 |
. . . . . . . . . . . . . . . . . . . . . 22
  
     
         
finSupp
finSupp    |
63 | 62 | bicomd 205 |
. . . . . . . . . . . . . . . . . . . . 21
  
     
   finSupp
       finSupp    |
64 | 61, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
         
    
    
        finSupp
       finSupp    |
65 | 64 | biimpd 211 |
. . . . . . . . . . . . . . . . . . 19
         
    
    
        finSupp
       finSupp    |
66 | 65 | impr 625 |
. . . . . . . . . . . . . . . . . 18
         
          
      finSupp          finSupp   |
67 | 8, 12, 9, 7, 2, 43,
29, 23, 20, 34, 66 | lcomfsupp 18128 |
. . . . . . . . . . . . . . . . 17
         
          
      finSupp             finSupp  |
68 | | incom 3625 |
. . . . . . . . . . . . . . . . . . 19
                 |
69 | | disjdif 3839 |
. . . . . . . . . . . . . . . . . . 19
   
     |
70 | 68, 69 | eqtri 2473 |
. . . . . . . . . . . . . . . . . 18
         |
71 | 70 | a1i 11 |
. . . . . . . . . . . . . . . . 17
         
          
      finSupp             |
72 | | difsnid 4118 |
. . . . . . . . . . . . . . . . . . 19
           |
73 | 72 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . 18
           |
74 | 41, 73 | syl 17 |
. . . . . . . . . . . . . . . . 17
         
          
      finSupp             |
75 | 7, 20, 38, 22, 23, 44, 67, 71, 74 | gsumsplit 17561 |
. . . . . . . . . . . . . . . 16
         
          
      finSupp    g              g                        g                   |
76 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . 21
 |
77 | | snex 4641 |
. . . . . . . . . . . . . . . . . . . . 21
      |
78 | 76, 77 | unex 6589 |
. . . . . . . . . . . . . . . . . . . 20
        |
79 | | simpl3 1013 |
. . . . . . . . . . . . . . . . . . . . . 22
        
      |
80 | | simpl2 1012 |
. . . . . . . . . . . . . . . . . . . . . 22
        
  |
81 | | fex 6138 |
. . . . . . . . . . . . . . . . . . . . . 22
     
   |
82 | 79, 80, 81 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . 21
        
  |
83 | 82 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
         
          
      finSupp     |
84 | | offres 6788 |
. . . . . . . . . . . . . . . . . . . 20
                                   
              |
85 | 78, 83, 84 | sylancr 669 |
. . . . . . . . . . . . . . . . . . 19
         
          
      finSupp              
                            |
86 | | ffn 5728 |
. . . . . . . . . . . . . . . . . . . . . 22
            

     |
87 | 28, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
         
          
      finSupp         |
88 | | neldifsn 4099 |
. . . . . . . . . . . . . . . . . . . . 21
     |
89 | | fsnunres 6105 |
. . . . . . . . . . . . . . . . . . . . 21
                          |
90 | 87, 88, 89 | sylancl 668 |
. . . . . . . . . . . . . . . . . . . 20
         
          
      finSupp           
      |
91 | 90 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . 19
         
          
      finSupp            
                       |
92 | 85, 91 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . 18
         
          
      finSupp              
       
       |
93 | 92 | oveq2d 6306 |
. . . . . . . . . . . . . . . . 17
         
          
      finSupp    g                   g    
        |
94 | | ffn 5728 |
. . . . . . . . . . . . . . . . . . . . . 22
                           |
95 | 44, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
         
          
      finSupp               |
96 | | fnressn 6076 |
. . . . . . . . . . . . . . . . . . . . 21
                                                |
97 | 95, 41, 96 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . 20
         
          
      finSupp                                      |
98 | | ffn 5728 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                         |
99 | 43, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
          
      finSupp            |
100 | | ffn 5728 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
  |
101 | 29, 100 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
          
      finSupp     |
102 | | fnfvof 6545 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         


                                   |
103 | 99, 101, 23, 41, 102 | syl22anc 1269 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
          
      finSupp                            
       |
104 | | fndm 5675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    

     |
105 | 104 | eleq2d 2514 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     

      |
106 | 88, 105 | mtbiri 305 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
  |
107 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
108 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
109 | | fsnunfv 6104 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
              |
110 | 107, 108,
109 | mp3an12 1354 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
              |
111 | 87, 106, 110 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
          
      finSupp                |
112 | 111 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
          
      finSupp              
             |
113 | 103, 112 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . . . . 22
         
          
      finSupp                         |
114 | 113 | opeq2d 4173 |
. . . . . . . . . . . . . . . . . . . . 21
         
          
      finSupp                               |
115 | 114 | sneqd 3980 |
. . . . . . . . . . . . . . . . . . . 20
         
          
      finSupp                                   |
116 | | ovex 6318 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
117 | | fmptsn 6084 |
. . . . . . . . . . . . . . . . . . . . . 22
                                |
118 | 107, 116,
117 | mp2an 678 |
. . . . . . . . . . . . . . . . . . . . 21
                      |
119 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
         
          
      finSupp                          |
120 | 97, 115, 119 | 3eqtrd 2489 |
. . . . . . . . . . . . . . . . . . 19
         
          
      finSupp                             |
121 | 120 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . 18
         
          
      finSupp    g                 g              |
122 | | cmnmnd 17445 |
. . . . . . . . . . . . . . . . . . . 20
 CMnd   |
123 | 22, 122 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
         
          
      finSupp     |
124 | 107 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
         
          
      finSupp     |
125 | | eqidd 2452 |
. . . . . . . . . . . . . . . . . . . 20
 
             |
126 | 7, 125 | gsumsn 17587 |
. . . . . . . . . . . . . . . . . . 19
 

       g                    |
127 | 123, 124,
19, 126 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . 18
         
          
      finSupp    g                    |
128 | 121, 127 | eqtrd 2485 |
. . . . . . . . . . . . . . . . 17
         
          
      finSupp    g                        |
129 | 93, 128 | oveq12d 6308 |
. . . . . . . . . . . . . . . 16
         
          
      finSupp     g                        g                   g                         |
130 | 75, 129 | eqtr2d 2486 |
. . . . . . . . . . . . . . 15
         
          
      finSupp     g    
                   g              |
131 | 130 | eqeq1d 2453 |
. . . . . . . . . . . . . 14
         
          
      finSupp      g                        g              |
132 | 15, 40, 131 | 3bitrd 283 |
. . . . . . . . . . . . 13
         
          
      finSupp                    g    
       g              |
133 | 111 | eqcomd 2457 |
. . . . . . . . . . . . . 14
         
          
      finSupp                |
134 | 133 | eqeq1d 2453 |
. . . . . . . . . . . . 13
         
          
      finSupp   
              |
135 | 132, 134 | imbi12d 322 |
. . . . . . . . . . . 12
         
          
      finSupp                     g    
     

  g                           |
136 | 135 | anassrs 654 |
. . . . . . . . . . 11
    
    
     
            finSupp 
                  g    
     

  g                           |
137 | 136 | pm5.74da 693 |
. . . . . . . . . 10
         
    
    
         finSupp                  g    
     
 
 finSupp   g                            |
138 | | impexp 448 |
. . . . . . . . . . 11
   finSupp                 g    
       
 finSupp           
      g    
     
    |
139 | 138 | a1i 11 |
. . . . . . . . . 10
         
    
    
          finSupp                 g    
       
 finSupp           
      g    
     
     |
140 | 64 | bicomd 205 |
. . . . . . . . . . 11
         
    
    
               finSupp
finSupp    |
141 | 140 | imbi1d 319 |
. . . . . . . . . 10
         
    
    
                finSupp   g                          finSupp   g                            |
142 | 137, 139,
141 | 3bitr4d 289 |
. . . . . . . . 9
         
    
    
          finSupp                 g    
       
        finSupp   g                            |
143 | 142 | 2ralbidva 2830 |
. . . . . . . 8
        
 
          
        finSupp                 g    
       
           
              finSupp   g                            |
144 | | breq1 4405 |
. . . . . . . . . . 11
         finSupp
       finSupp    |
145 | | oveq1 6297 |
. . . . . . . . . . . . . 14
                       |
146 | 145 | oveq2d 6306 |
. . . . . . . . . . . . 13
         g      g              |
147 | 146 | eqeq1d 2453 |
. . . . . . . . . . . 12
          g    
 g              |
148 | | fveq1 5864 |
. . . . . . . . . . . . 13
                         |
149 | 148 | eqeq1d 2453 |
. . . . . . . . . . . 12
            
              |
150 | 147, 149 | imbi12d 322 |
. . . . . . . . . . 11
           g            g                           |
151 | 144, 150 | imbi12d 322 |
. . . . . . . . . 10
          finSupp
  g          
        finSupp   g                            |
152 | 151 | ralxpmap 7521 |
. . . . . . . . 9
  
        finSupp   g 
  
     
           
              finSupp   g                            |
153 | 152 | adantl 468 |
. . . . . . . 8
        
 
        finSupp   g 
  
     
           
              finSupp   g                            |
154 | 143, 153 | bitr4d 260 |
. . . . . . 7
        
 
          
        finSupp                 g    
       
     
   finSupp
  g              |
155 | | breq1 4405 |
. . . . . . . 8
  finSupp
finSupp    |
156 | 155 | ralrab 3200 |
. . . . . . 7
 
     

finSupp    g         
     
   finSupp
  g             |
157 | 154, 156 | syl6bbr 267 |
. . . . . 6
        
 
          
        finSupp                 g    
       
      

finSupp    g             |
158 | | resima 5137 |
. . . . . . . . . . . . 13
 
                     |
159 | 158 | eqcomi 2460 |
. . . . . . . . . . . 12
         
             |
160 | 159 | fveq2i 5868 |
. . . . . . . . . . 11
                                       |
161 | 160 | eleq2i 2521 |
. . . . . . . . . 10
          
                                             
              |
162 | | eqid 2451 |
. . . . . . . . . . 11
         |
163 | 79, 30, 31 | sylancl 668 |
. . . . . . . . . . 11
        
                |
164 | | simpl1 1011 |
. . . . . . . . . . 11
        
  |
165 | 24 | 3ad2ant2 1030 |
. . . . . . . . . . . 12
 
           |
166 | 165 | adantr 467 |
. . . . . . . . . . 11
        
      |
167 | 162, 7, 12, 8, 34, 9, 163, 164, 166 | ellspd 19360 |
. . . . . . . . . 10
        
          
                          
     
       finSupp                 g    
          |
168 | 161, 167 | syl5bb 261 |
. . . . . . . . 9
        
          
                          
       finSupp                 g    
          |
169 | 168 | imbi1d 319 |
. . . . . . . 8
        
                                        
       finSupp                 g    
           |
170 | | r19.23v 2867 |
. . . . . . . 8
 
     
       finSupp                 g    
       
 
     
      finSupp
         
      g    
          |
171 | 169, 170 | syl6bbr 267 |
. . . . . . 7
        
                                  
             finSupp                 g    
           |
172 | 171 | ralbidv 2827 |
. . . . . 6
        
 
               
                    

           
        finSupp                 g    
           |
173 | | fvex 5875 |
. . . . . . . . . . . 12
Scalar   |
174 | 8, 173 | eqeltri 2525 |
. . . . . . . . . . 11
 |
175 | | eqid 2451 |
. . . . . . . . . . . 12
 freeLMod   freeLMod   |
176 | | eqid 2451 |
. . . . . . . . . . . 12
       finSupp 
     

finSupp   |
177 | 175, 12, 34, 176 | frlmbas 19318 |
. . . . . . . . . . 11
 
      

finSupp      freeLMod     |
178 | 174, 177 | mpan 676 |
. . . . . . . . . 10
        finSupp 
    freeLMod
    |
179 | 178 | 3ad2ant2 1030 |
. . . . . . . . 9
 
          

finSupp      freeLMod     |
180 | 179 | adantr 467 |
. . . . . . . 8
        
     

finSupp      freeLMod     |
181 | | islindf4.l |
. . . . . . . 8
    freeLMod    |
182 | 180, 181 | syl6reqr 2504 |
. . . . . . 7
        
     

finSupp    |
183 | 182 | raleqdv 2993 |
. . . . . 6
        
 
  g         
      

finSupp    g             |
184 | 157, 172,
183 | 3bitr4d 289 |
. . . . 5
        
 
               
                    


  g             |
185 | 1, 184 | syl5bb 261 |
. . . 4
        
 
                                      

  g             |
186 | 8 | lmodfgrp 18100 |
. . . . . . . 8

  |
187 | 12, 34, 11 | grpinvnzcl 16726 |
. . . . . . . 8
 
                      
     |
188 | 186, 187 | sylan 474 |
. . . . . . 7
      
                       |
189 | 12, 34, 11 | grpinvnzcl 16726 |
. . . . . . . . 9
 
                      
     |
190 | 186, 189 | sylan 474 |
. . . . . . . 8
      
                       |
191 | | eldifi 3555 |
. . . . . . . . . 10
               |
192 | 12, 11 | grpinvinv 16721 |
. . . . . . . . . 10
 
                         |
193 | 186, 191,
192 | syl2an 480 |
. . . . . . . . 9
      
                        |
194 | 193 | eqcomd 2457 |
. . . . . . . 8
      
                        |
195 | | fveq2 5865 |
. . . . . . . . . 10
                                       |
196 | 195 | eqeq2d 2461 |
. . . . . . . . 9
                                         |
197 | 196 | rspcev 3150 |
. . . . . . . 8
                                      
                    |
198 | 190, 194,
197 | syl2anc 667 |
. . . . . . 7
      
    
                    |
199 | | oveq1 6297 |
. . . . . . . . . 10
                         
       |
200 | 199 | eleq1d 2513 |
. . . . . . . . 9
                                
         
                        |
201 | 200 | notbid 296 |
. . . . . . . 8
                                
         
                        |
202 | 201 | adantl 468 |
. . . . . . 7
             
                    
         
                        |
203 | 188, 198,
202 | ralxfrd 4614 |
. . . . . 6

 
                             
     
            
                        |
204 | 203 | 3ad2ant1 1029 |
. . . . 5
 
           
   
                          
            
                        |
205 | 204 | adantr 467 |
. . . 4
        
 
                             
     
            
                        |
206 | | simplr 762 |
. . . . . . . 8
         
   |
207 | | fvex 5875 |
. . . . . . . . . 10
     |
208 | 34, 207 | eqeltri 2525 |
. . . . . . . . 9
 |
209 | 208 | fvconst2 6120 |
. . . . . . . 8
           |
210 | 206, 209 | syl 17 |
. . . . . . 7
         
           |
211 | 210 | eqeq2d 2461 |
. . . . . 6
         
                     |
212 | 211 | imbi2d 318 |
. . . . 5
         
    g                 
  g             |
213 | 212 | ralbidva 2824 |
. . . 4
        
 
  g                     g             |
214 | 185, 205,
213 | 3bitr4d 289 |
. . 3
        
 
                             

  g                     |
215 | 214 | ralbidva 2824 |
. 2
 
            
   
                      
  g                     |
216 | 7, 9, 162, 8, 12, 34 | islindf2 19372 |
. 2
 
      LIndF

     
   
                        |
217 | 175, 12, 181 | frlmbasf 19323 |
. . . . . . . 8
 
           |
218 | 217 | 3ad2antl2 1171 |
. . . . . . 7
        
          |
219 | | ffn 5728 |
. . . . . . 7
           |
220 | 218, 219 | syl 17 |
. . . . . 6
        
  |
221 | | fnconstg 5771 |
. . . . . . 7
       |
222 | 208, 221 | ax-mp 5 |
. . . . . 6
     |
223 | | eqfnfv 5976 |
. . . . . 6
  
   
    

               |
224 | 220, 222,
223 | sylancl 668 |
. . . . 5
        
    

               |
225 | 224 | imbi2d 318 |
. . . 4
        
   g            g                      |
226 | 225 | ralbidva 2824 |
. . 3
 
         g 
  

   

  g     
                |
227 | | r19.21v 2793 |
. . . . 5
 
  g                    g 
  

               |
228 | 227 | ralbii 2819 |
. . . 4
 

  g                     g                     |
229 | | ralcom 2951 |
. . . 4
 

  g                   
  g                    |
230 | 228, 229 | bitr3i 255 |
. . 3
 
  g     
            


  g                    |
231 | 226, 230 | syl6bb 265 |
. 2
 
         g 
  

   


  g                     |
232 | 215, 216,
231 | 3bitr4d 289 |
1
 
      LIndF

  g             |