Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . 5
|
2 | 1 | lindff 20154 |
. . . 4
LIndF |
3 | 2 | ancoms 469 |
. . 3
LIndF
|
4 | | frn 6053 |
. . 3
|
5 | 3, 4 | syl 17 |
. 2
LIndF
|
6 | | simpll 790 |
. . . . . . 7
LIndF
|
7 | | imassrn 5477 |
. . . . . . . . 9
|
8 | 7, 5 | syl5ss 3614 |
. . . . . . . 8
LIndF
|
9 | 8 | adantr 481 |
. . . . . . 7
LIndF
|
10 | | ffun 6048 |
. . . . . . . . 9
|
11 | 3, 10 | syl 17 |
. . . . . . . 8
LIndF
|
12 | | eldifsn 4317 |
. . . . . . . . . 10
|
13 | | funfn 5918 |
. . . . . . . . . . . . . 14
|
14 | | fvelrnb 6243 |
. . . . . . . . . . . . . 14
|
15 | 13, 14 | sylbi 207 |
. . . . . . . . . . . . 13
|
16 | 15 | adantr 481 |
. . . . . . . . . . . 12
|
17 | | difss 3737 |
. . . . . . . . . . . . . . . . . 18
|
18 | 17 | jctr 565 |
. . . . . . . . . . . . . . . . 17
|
19 | 18 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
20 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
|
21 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
22 | 21 | necon3i 2826 |
. . . . . . . . . . . . . . . . . . 19
|
23 | 22 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
24 | | eldifsn 4317 |
. . . . . . . . . . . . . . . . . 18
|
25 | 20, 23, 24 | sylanbrc 698 |
. . . . . . . . . . . . . . . . 17
|
26 | 25 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
27 | | funfvima2 6493 |
. . . . . . . . . . . . . . . 16
|
28 | 19, 26, 27 | sylc 65 |
. . . . . . . . . . . . . . 15
|
29 | 28 | expr 643 |
. . . . . . . . . . . . . 14
|
30 | | neeq1 2856 |
. . . . . . . . . . . . . . 15
|
31 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
|
32 | 30, 31 | imbi12d 334 |
. . . . . . . . . . . . . 14
|
33 | 29, 32 | syl5ibcom 235 |
. . . . . . . . . . . . 13
|
34 | 33 | rexlimdva 3031 |
. . . . . . . . . . . 12
|
35 | 16, 34 | sylbid 230 |
. . . . . . . . . . 11
|
36 | 35 | impd 447 |
. . . . . . . . . 10
|
37 | 12, 36 | syl5bi 232 |
. . . . . . . . 9
|
38 | 37 | ssrdv 3609 |
. . . . . . . 8
|
39 | 11, 38 | sylan 488 |
. . . . . . 7
LIndF
|
40 | | eqid 2622 |
. . . . . . . 8
|
41 | 1, 40 | lspss 18984 |
. . . . . . 7
|
42 | 6, 9, 39, 41 | syl3anc 1326 |
. . . . . 6
LIndF
|
43 | 42 | adantrr 753 |
. . . . 5
LIndF Scalar Scalar |
44 | | simplr 792 |
. . . . . 6
LIndF Scalar Scalar LIndF
|
45 | | simprl 794 |
. . . . . 6
LIndF Scalar Scalar |
46 | | eldifi 3732 |
. . . . . . 7
Scalar
Scalar Scalar |
47 | 46 | ad2antll 765 |
. . . . . 6
LIndF Scalar Scalar Scalar |
48 | | eldifsni 4320 |
. . . . . . 7
Scalar
Scalar Scalar |
49 | 48 | ad2antll 765 |
. . . . . 6
LIndF Scalar Scalar Scalar |
50 | | eqid 2622 |
. . . . . . 7
|
51 | | eqid 2622 |
. . . . . . 7
Scalar Scalar |
52 | | eqid 2622 |
. . . . . . 7
Scalar Scalar |
53 | | eqid 2622 |
. . . . . . 7
Scalar Scalar |
54 | 50, 40, 51, 52, 53 | lindfind 20155 |
. . . . . 6
LIndF
Scalar Scalar
|
55 | 44, 45, 47, 49, 54 | syl22anc 1327 |
. . . . 5
LIndF Scalar Scalar
|
56 | 43, 55 | ssneldd 3606 |
. . . 4
LIndF Scalar Scalar
|
57 | 56 | ralrimivva 2971 |
. . 3
LIndF
Scalar Scalar |
58 | 11, 13 | sylib 208 |
. . . 4
LIndF
|
59 | | oveq2 6658 |
. . . . . . . 8
|
60 | | sneq 4187 |
. . . . . . . . . 10
|
61 | 60 | difeq2d 3728 |
. . . . . . . . 9
|
62 | 61 | fveq2d 6195 |
. . . . . . . 8
|
63 | 59, 62 | eleq12d 2695 |
. . . . . . 7
|
64 | 63 | notbid 308 |
. . . . . 6
|
65 | 64 | ralbidv 2986 |
. . . . 5
Scalar Scalar
Scalar Scalar |
66 | 65 | ralrn 6362 |
. . . 4
Scalar Scalar
Scalar Scalar |
67 | 58, 66 | syl 17 |
. . 3
LIndF
Scalar Scalar
Scalar Scalar |
68 | 57, 67 | mpbird 247 |
. 2
LIndF
Scalar Scalar |
69 | 1, 50, 40, 51, 53, 52 | islinds2 20152 |
. . 3
LIndS
Scalar Scalar |
70 | 69 | adantr 481 |
. 2
LIndF
LIndS
Scalar Scalar |
71 | 5, 68, 70 | mpbir2and 957 |
1
LIndF
LIndS |