Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . . 7
|
2 | 1 | lindff 20154 |
. . . . . 6
LIndF |
3 | 2 | ancoms 469 |
. . . . 5
LIndF
|
4 | 3 | 3adant3 1081 |
. . . 4
LIndF |
5 | | f1f 6101 |
. . . . 5
|
6 | 5 | 3ad2ant3 1084 |
. . . 4
LIndF
|
7 | | fco 6058 |
. . . 4
|
8 | 4, 6, 7 | syl2anc 693 |
. . 3
LIndF
|
9 | | ffdm 6062 |
. . . 4
|
10 | 9 | simpld 475 |
. . 3
|
11 | 8, 10 | syl 17 |
. 2
LIndF
|
12 | | simpl2 1065 |
. . . . 5
LIndF
Scalar Scalar LIndF
|
13 | 6 | adantr 481 |
. . . . . . 7
LIndF
|
14 | | fdm 6051 |
. . . . . . . . . 10
|
15 | 8, 14 | syl 17 |
. . . . . . . . 9
LIndF
|
16 | 15 | eleq2d 2687 |
. . . . . . . 8
LIndF
|
17 | 16 | biimpa 501 |
. . . . . . 7
LIndF
|
18 | 13, 17 | ffvelrnd 6360 |
. . . . . 6
LIndF
|
19 | 18 | adantrr 753 |
. . . . 5
LIndF
Scalar Scalar |
20 | | eldifi 3732 |
. . . . . 6
Scalar
Scalar Scalar |
21 | 20 | ad2antll 765 |
. . . . 5
LIndF
Scalar Scalar Scalar |
22 | | eldifsni 4320 |
. . . . . 6
Scalar
Scalar Scalar |
23 | 22 | ad2antll 765 |
. . . . 5
LIndF
Scalar Scalar Scalar |
24 | | eqid 2622 |
. . . . . 6
|
25 | | eqid 2622 |
. . . . . 6
|
26 | | eqid 2622 |
. . . . . 6
Scalar Scalar |
27 | | eqid 2622 |
. . . . . 6
Scalar Scalar |
28 | | eqid 2622 |
. . . . . 6
Scalar Scalar |
29 | 24, 25, 26, 27, 28 | lindfind 20155 |
. . . . 5
LIndF Scalar Scalar
|
30 | 12, 19, 21, 23, 29 | syl22anc 1327 |
. . . 4
LIndF
Scalar Scalar
|
31 | | f1fn 6102 |
. . . . . . . . . . 11
|
32 | 31 | 3ad2ant3 1084 |
. . . . . . . . . 10
LIndF |
33 | 32 | adantr 481 |
. . . . . . . . 9
LIndF
|
34 | | fvco2 6273 |
. . . . . . . . 9
|
35 | 33, 17, 34 | syl2anc 693 |
. . . . . . . 8
LIndF
|
36 | 35 | oveq2d 6666 |
. . . . . . 7
LIndF
|
37 | 36 | eleq1d 2686 |
. . . . . 6
LIndF
|
38 | | simpl1 1064 |
. . . . . . . . 9
LIndF
|
39 | | imassrn 5477 |
. . . . . . . . . . 11
|
40 | | frn 6053 |
. . . . . . . . . . . 12
|
41 | 4, 40 | syl 17 |
. . . . . . . . . . 11
LIndF |
42 | 39, 41 | syl5ss 3614 |
. . . . . . . . . 10
LIndF
|
43 | 42 | adantr 481 |
. . . . . . . . 9
LIndF
|
44 | | imaco 5640 |
. . . . . . . . . 10
|
45 | 15 | difeq1d 3727 |
. . . . . . . . . . . . . . 15
LIndF
|
46 | 45 | imaeq2d 5466 |
. . . . . . . . . . . . . 14
LIndF
|
47 | | df-f1 5893 |
. . . . . . . . . . . . . . . . 17
|
48 | 47 | simprbi 480 |
. . . . . . . . . . . . . . . 16
|
49 | 48 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . 15
LIndF |
50 | | imadif 5973 |
. . . . . . . . . . . . . . 15
|
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . 14
LIndF |
52 | 46, 51 | eqtrd 2656 |
. . . . . . . . . . . . 13
LIndF
|
53 | 52 | adantr 481 |
. . . . . . . . . . . 12
LIndF
|
54 | | fnsnfv 6258 |
. . . . . . . . . . . . . . 15
|
55 | 32, 54 | sylan 488 |
. . . . . . . . . . . . . 14
LIndF
|
56 | 55 | difeq2d 3728 |
. . . . . . . . . . . . 13
LIndF
|
57 | | imassrn 5477 |
. . . . . . . . . . . . . . 15
|
58 | 6 | adantr 481 |
. . . . . . . . . . . . . . . 16
LIndF
|
59 | | frn 6053 |
. . . . . . . . . . . . . . . 16
|
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . 15
LIndF
|
61 | 57, 60 | syl5ss 3614 |
. . . . . . . . . . . . . 14
LIndF
|
62 | 61 | ssdifd 3746 |
. . . . . . . . . . . . 13
LIndF
|
63 | 56, 62 | eqsstr3d 3640 |
. . . . . . . . . . . 12
LIndF
|
64 | 53, 63 | eqsstrd 3639 |
. . . . . . . . . . 11
LIndF
|
65 | | imass2 5501 |
. . . . . . . . . . 11
|
66 | 64, 65 | syl 17 |
. . . . . . . . . 10
LIndF
|
67 | 44, 66 | syl5eqss 3649 |
. . . . . . . . 9
LIndF
|
68 | 1, 25 | lspss 18984 |
. . . . . . . . 9
|
69 | 38, 43, 67, 68 | syl3anc 1326 |
. . . . . . . 8
LIndF
|
70 | 17, 69 | syldan 487 |
. . . . . . 7
LIndF
|
71 | 70 | sseld 3602 |
. . . . . 6
LIndF
|
72 | 37, 71 | sylbid 230 |
. . . . 5
LIndF
|
73 | 72 | adantrr 753 |
. . . 4
LIndF
Scalar Scalar
|
74 | 30, 73 | mtod 189 |
. . 3
LIndF
Scalar Scalar
|
75 | 74 | ralrimivva 2971 |
. 2
LIndF Scalar Scalar
|
76 | | simp1 1061 |
. . 3
LIndF |
77 | | rellindf 20147 |
. . . . . 6
LIndF |
78 | 77 | brrelexi 5158 |
. . . . 5
LIndF
|
79 | 78 | 3ad2ant2 1083 |
. . . 4
LIndF |
80 | | simp3 1063 |
. . . . . 6
LIndF |
81 | | dmexg 7097 |
. . . . . . 7
|
82 | 79, 81 | syl 17 |
. . . . . 6
LIndF |
83 | | f1dmex 7136 |
. . . . . 6
|
84 | 80, 82, 83 | syl2anc 693 |
. . . . 5
LIndF |
85 | | fex 6490 |
. . . . 5
|
86 | 6, 84, 85 | syl2anc 693 |
. . . 4
LIndF |
87 | | coexg 7117 |
. . . 4
|
88 | 79, 86, 87 | syl2anc 693 |
. . 3
LIndF
|
89 | 1, 24, 25, 26, 28, 27 | islindf 20151 |
. . 3
LIndF
Scalar Scalar
|
90 | 76, 88, 89 | syl2anc 693 |
. 2
LIndF LIndF
Scalar Scalar
|
91 | 11, 75, 90 | mpbir2and 957 |
1
LIndF
LIndF |