Step | Hyp | Ref
| Expression |
1 | | eqid 2450 |
. . . . . . 7
         |
2 | 1 | lindff 19366 |
. . . . . 6
  LIndF            |
3 | 2 | ancoms 455 |
. . . . 5
  LIndF 
          |
4 | 3 | 3adant3 1027 |
. . . 4
  LIndF                |
5 | | f1f 5777 |
. . . . 5
           |
6 | 5 | 3ad2ant3 1030 |
. . . 4
  LIndF         
  |
7 | | fco 5737 |
. . . 4
              
            |
8 | 4, 6, 7 | syl2anc 666 |
. . 3
  LIndF      
           |
9 | | ffdm 5741 |
. . . 4
                
            |
10 | 9 | simpld 461 |
. . 3
           
             |
11 | 8, 10 | syl 17 |
. 2
  LIndF      
             |
12 | | simpl2 1011 |
. . . . 5
   LIndF      


    Scalar       Scalar       LIndF
  |
13 | 6 | adantr 467 |
. . . . . . 7
   LIndF     
         |
14 | | fdm 5731 |
. . . . . . . . . 10
           
   |
15 | 8, 14 | syl 17 |
. . . . . . . . 9
  LIndF      
   |
16 | 15 | eleq2d 2513 |
. . . . . . . 8
  LIndF       
    |
17 | 16 | biimpa 487 |
. . . . . . 7
   LIndF     
     |
18 | 13, 17 | ffvelrnd 6021 |
. . . . . 6
   LIndF     
         |
19 | 18 | adantrr 722 |
. . . . 5
   LIndF      


    Scalar       Scalar             |
20 | | eldifi 3554 |
. . . . . 6
     Scalar  
    Scalar        Scalar     |
21 | 20 | ad2antll 734 |
. . . . 5
   LIndF      


    Scalar       Scalar          Scalar     |
22 | | eldifsni 4097 |
. . . . . 6
     Scalar  
    Scalar        Scalar     |
23 | 22 | ad2antll 734 |
. . . . 5
   LIndF      


    Scalar       Scalar          Scalar     |
24 | | eqid 2450 |
. . . . . 6
         |
25 | | eqid 2450 |
. . . . . 6
         |
26 | | eqid 2450 |
. . . . . 6
Scalar  Scalar   |
27 | | eqid 2450 |
. . . . . 6
   Scalar      Scalar    |
28 | | eqid 2450 |
. . . . . 6
   Scalar      Scalar    |
29 | 24, 25, 26, 27, 28 | lindfind 19367 |
. . . . 5
   LIndF          Scalar      Scalar                               
           |
30 | 12, 19, 21, 23, 29 | syl22anc 1268 |
. . . 4
   LIndF      


    Scalar       Scalar      
                                      |
31 | | f1fn 5778 |
. . . . . . . . . . 11
       |
32 | 31 | 3ad2ant3 1030 |
. . . . . . . . . 10
  LIndF        |
33 | 32 | adantr 467 |
. . . . . . . . 9
   LIndF     
     |
34 | | fvco2 5938 |
. . . . . . . . 9
 
                 |
35 | 33, 17, 34 | syl2anc 666 |
. . . . . . . 8
   LIndF     
                   |
36 | 35 | oveq2d 6304 |
. . . . . . 7
   LIndF     
                                   |
37 | 36 | eleq1d 2512 |
. . . . . 6
   LIndF     
                          
    
     
                              
        |
38 | | simpl1 1010 |
. . . . . . . . 9
   LIndF     
   |
39 | | imassrn 5178 |
. . . . . . . . . . 11
           
 |
40 | | frn 5733 |
. . . . . . . . . . . 12
               |
41 | 4, 40 | syl 17 |
. . . . . . . . . . 11
  LIndF            |
42 | 39, 41 | syl5ss 3442 |
. . . . . . . . . 10
  LIndF                 
      |
43 | 42 | adantr 467 |
. . . . . . . . 9
   LIndF     
                   |
44 | | imaco 5339 |
. . . . . . . . . 10
      
           
        |
45 | 15 | difeq1d 3549 |
. . . . . . . . . . . . . . 15
  LIndF        
         |
46 | 45 | imaeq2d 5167 |
. . . . . . . . . . . . . 14
  LIndF          
               |
47 | | df-f1 5586 |
. . . . . . . . . . . . . . . . 17
              |
48 | 47 | simprbi 466 |
. . . . . . . . . . . . . . . 16
        |
49 | 48 | 3ad2ant3 1030 |
. . . . . . . . . . . . . . 15
  LIndF         |
50 | | imadif 5656 |
. . . . . . . . . . . . . . 15
 
                      |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . 14
  LIndF                            |
52 | 46, 51 | eqtrd 2484 |
. . . . . . . . . . . . 13
  LIndF          
                   |
53 | 52 | adantr 467 |
. . . . . . . . . . . 12
   LIndF     
      
                  |
54 | | fnsnfv 5923 |
. . . . . . . . . . . . . . 15
 
               |
55 | 32, 54 | sylan 474 |
. . . . . . . . . . . . . 14
   LIndF     
               |
56 | 55 | difeq2d 3550 |
. . . . . . . . . . . . 13
   LIndF     
                           |
57 | | imassrn 5178 |
. . . . . . . . . . . . . . 15
     |
58 | 6 | adantr 467 |
. . . . . . . . . . . . . . . 16
   LIndF     
       |
59 | | frn 5733 |
. . . . . . . . . . . . . . . 16
       |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . 15
   LIndF     
   |
61 | 57, 60 | syl5ss 3442 |
. . . . . . . . . . . . . 14
   LIndF     
    
  |
62 | 61 | ssdifd 3568 |
. . . . . . . . . . . . 13
   LIndF     
                       |
63 | 56, 62 | eqsstr3d 3466 |
. . . . . . . . . . . 12
   LIndF     
                       |
64 | 53, 63 | eqsstrd 3465 |
. . . . . . . . . . 11
   LIndF     
      
              |
65 | | imass2 5203 |
. . . . . . . . . . 11
      
                   
                    |
66 | 64, 65 | syl 17 |
. . . . . . . . . 10
   LIndF     
        
                    |
67 | 44, 66 | syl5eqss 3475 |
. . . . . . . . 9
   LIndF     
        
       
          |
68 | 1, 25 | lspss 18200 |
. . . . . . . . 9
             
           
       
                       
                           |
69 | 38, 43, 67, 68 | syl3anc 1267 |
. . . . . . . 8
   LIndF     
         
    
                            |
70 | 17, 69 | syldan 473 |
. . . . . . 7
   LIndF     
                 
                           |
71 | 70 | sseld 3430 |
. . . . . 6
   LIndF     
                                  
                                            |
72 | 37, 71 | sylbid 219 |
. . . . 5
   LIndF     
                          
    
                                             |
73 | 72 | adantrr 722 |
. . . 4
   LIndF      


    Scalar       Scalar                              
    
                                             |
74 | 30, 73 | mtod 181 |
. . 3
   LIndF      


    Scalar       Scalar      
                      
    
        |
75 | 74 | ralrimivva 2808 |
. 2
  LIndF               Scalar       Scalar                                 
       |
76 | | simp1 1007 |
. . 3
  LIndF        |
77 | | rellindf 19359 |
. . . . . 6
LIndF |
78 | 77 | brrelexi 4874 |
. . . . 5
 LIndF
  |
79 | 78 | 3ad2ant2 1029 |
. . . 4
  LIndF        |
80 | | simp3 1009 |
. . . . . 6
  LIndF            |
81 | | dmexg 6721 |
. . . . . . 7
   |
82 | 79, 81 | syl 17 |
. . . . . 6
  LIndF        |
83 | | f1dmex 6760 |
. . . . . 6
         |
84 | 80, 82, 83 | syl2anc 666 |
. . . . 5
  LIndF        |
85 | | fex 6136 |
. . . . 5
     
   |
86 | 6, 84, 85 | syl2anc 666 |
. . . 4
  LIndF        |
87 | | coexg 6741 |
. . . 4
 
     |
88 | 79, 86, 87 | syl2anc 666 |
. . 3
  LIndF      
   |
89 | 1, 24, 25, 26, 28, 27 | islindf 19363 |
. . 3
  
     LIndF
             
   
    Scalar       Scalar                           
    
          |
90 | 76, 88, 89 | syl2anc 666 |
. 2
  LIndF         LIndF
             
   
    Scalar       Scalar                           
    
          |
91 | 11, 75, 90 | mpbir2and 932 |
1
  LIndF      
 LIndF   |