Step | Hyp | Ref
| Expression |
1 | | difexg 4551 |
. . . . . . . . . . 11
        |
2 | 1 | 3ad2ant1 1029 |
. . . . . . . . . 10
  
       |
3 | 2 | adantl 468 |
. . . . . . . . 9
         
 
        |
4 | 3 | adantr 467 |
. . . . . . . 8
     
    
 
  finSupp       |
5 | | lincresunit.g |
. . . . . . . . 9
                         |
6 | | mptexg 6135 |
. . . . . . . . 9
                               |
7 | 5, 6 | syl5eqel 2533 |
. . . . . . . 8
       |
8 | 4, 7 | syl 17 |
. . . . . . 7
     
    
 
  finSupp   |
9 | 5 | funmpt2 5619 |
. . . . . . . 8
 |
10 | 9 | a1i 11 |
. . . . . . 7
     
    
 
  finSupp   |
11 | | lincresunit.0 |
. . . . . . . . 9
     |
12 | | fvex 5875 |
. . . . . . . . 9
     |
13 | 11, 12 | eqeltri 2525 |
. . . . . . . 8
 |
14 | 13 | a1i 11 |
. . . . . . 7
     
    
 
  finSupp   |
15 | | simpr 463 |
. . . . . . . 8
     
    
 
  finSupp finSupp  |
16 | 15 | fsuppimpd 7890 |
. . . . . . 7
     
    
 
  finSupp  supp   |
17 | | simplr 762 |
. . . . . . . . . . . . 13
     
    
 
 
    
 
   |
18 | | simpll 760 |
. . . . . . . . . . . . 13
     
    
 
 
    
  
       |
19 | | eldifi 3555 |
. . . . . . . . . . . . . 14
       |
20 | 19 | adantl 468 |
. . . . . . . . . . . . 13
     
    
 
 
    
  |
21 | | lincresunit.b |
. . . . . . . . . . . . . 14
     |
22 | | lincresunit.r |
. . . . . . . . . . . . . 14
Scalar   |
23 | | lincresunit.e |
. . . . . . . . . . . . . 14
     |
24 | | lincresunit.u |
. . . . . . . . . . . . . 14
Unit   |
25 | | lincresunit.z |
. . . . . . . . . . . . . 14
     |
26 | | lincresunit.n |
. . . . . . . . . . . . . 14
      |
27 | | lincresunit.i |
. . . . . . . . . . . . . 14
     |
28 | | lincresunit.t |
. . . . . . . . . . . . . 14
     |
29 | 21, 22, 23, 24, 11, 25, 26, 27, 28, 5 | lincresunitlem2 40322 |
. . . . . . . . . . . . 13
    
 
       
                     |
30 | 17, 18, 20, 29 | syl21anc 1267 |
. . . . . . . . . . . 12
     
    
 
 
    
                    |
31 | 30 | ralrimiva 2802 |
. . . . . . . . . . 11
         
 
  
                         |
32 | 5 | fnmpt 5704 |
. . . . . . . . . . 11
 
                             |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
         
 
 
      |
34 | | elmapfn 7494 |
. . . . . . . . . . . 12
     |
35 | 34 | adantr 467 |
. . . . . . . . . . 11
        
  |
36 | 35 | adantr 467 |
. . . . . . . . . 10
         
 
 
  |
37 | 33, 36 | jca 535 |
. . . . . . . . 9
         
 
      
   |
38 | | difssd 3561 |
. . . . . . . . . 10
         
 
        |
39 | | simpr1 1014 |
. . . . . . . . . 10
         
 
 
   |
40 | 13 | a1i 11 |
. . . . . . . . . 10
         
 
    |
41 | 38, 39, 40 | 3jca 1188 |
. . . . . . . . 9
         
 
           |
42 | 5 | a1i 11 |
. . . . . . . . . . . . 13
            

          
                          |
43 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
           |
44 | 43 | oveq2d 6306 |
. . . . . . . . . . . . . 14
                                       |
45 | 44 | adantl 468 |
. . . . . . . . . . . . 13
             
           
                                       |
46 | | simplr 762 |
. . . . . . . . . . . . 13
            

          
      |
47 | | simpllr 769 |
. . . . . . . . . . . . . 14
            

                |
48 | | simpll 760 |
. . . . . . . . . . . . . . 15
     
    
 
 
    
  
       |
49 | 48 | adantr 467 |
. . . . . . . . . . . . . 14
            

                     |
50 | | eldifi 3555 |
. . . . . . . . . . . . . . . 16
    
  |
51 | 50 | adantl 468 |
. . . . . . . . . . . . . . 15
     
    
 
 
    
  |
52 | 51 | adantr 467 |
. . . . . . . . . . . . . 14
            

          
  |
53 | 21, 22, 23, 24, 11, 25, 26, 27, 28, 5 | lincresunitlem2 40322 |
. . . . . . . . . . . . . 14
    
 
       
                     |
54 | 47, 49, 52, 53 | syl21anc 1267 |
. . . . . . . . . . . . 13
            

                               |
55 | 42, 45, 46, 54 | fvmptd 5954 |
. . . . . . . . . . . 12
            

                                   |
56 | | oveq2 6298 |
. . . . . . . . . . . . 13
                                      |
57 | 22 | lmodring 18099 |
. . . . . . . . . . . . . . . . 17

  |
58 | 57 | 3ad2ant2 1030 |
. . . . . . . . . . . . . . . 16
  
   |
59 | 58 | adantl 468 |
. . . . . . . . . . . . . . 15
         
 
 
  |
60 | 21, 22, 23, 24, 11, 25, 26, 27, 28, 5 | lincresunitlem1 40321 |
. . . . . . . . . . . . . . . 16
       
                    |
61 | 60 | ancoms 455 |
. . . . . . . . . . . . . . 15
         
 
                |
62 | 23, 28, 11 | ringrz 17818 |
. . . . . . . . . . . . . . 15
                           
 |
63 | 59, 61, 62 | syl2anc 667 |
. . . . . . . . . . . . . 14
         
 
                |
64 | 63 | adantr 467 |
. . . . . . . . . . . . 13
     
    
 
 
    
            
 |
65 | 56, 64 | sylan9eqr 2507 |
. . . . . . . . . . . 12
            

                              |
66 | 55, 65 | eqtrd 2485 |
. . . . . . . . . . 11
            

                |
67 | 66 | ex 436 |
. . . . . . . . . 10
     
    
 
 
    
    
      |
68 | 67 | ralrimiva 2802 |
. . . . . . . . 9
         
 
  
         
      |
69 | | suppfnss 6940 |
. . . . . . . . . 10
      
     
    
         
   
 supp
 supp    |
70 | 69 | imp 431 |
. . . . . . . . 9
    
        
   
              
 supp
 supp   |
71 | 37, 41, 68, 70 | syl21anc 1267 |
. . . . . . . 8
         
 
   supp
 supp   |
72 | 71 | adantr 467 |
. . . . . . 7
     
    
 
  finSupp  supp  supp   |
73 | | suppssfifsupp 7898 |
. . . . . . 7
  

  supp
 supp  supp  
finSupp  |
74 | 8, 10, 14, 16, 72, 73 | syl32anc 1276 |
. . . . . 6
     
    
 
  finSupp finSupp  |
75 | 74 | ex 436 |
. . . . 5
         
 
   finSupp
finSupp   |
76 | 75 | ex 436 |
. . . 4
           
  finSupp
finSupp    |
77 | 76 | com23 81 |
. . 3
          finSupp
   
finSupp    |
78 | 77 | 3impia 1205 |
. 2
        finSupp
 


finSupp   |
79 | 78 | impcom 432 |
1
       
   
finSupp 
finSupp  |