Description: Property deduction for linearly independent sets. (Contributed by Thierry Arnoux, 16-Jul-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lindfpropd.1 | |
|
lindfpropd.2 | |
||
lindfpropd.3 | |
||
lindfpropd.4 | |
||
lindfpropd.5 | |
||
lindfpropd.6 | |
||
lindfpropd.k | |
||
lindfpropd.l | |
||
Assertion | lindspropd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lindfpropd.1 | |
|
2 | lindfpropd.2 | |
|
3 | lindfpropd.3 | |
|
4 | lindfpropd.4 | |
|
5 | lindfpropd.5 | |
|
6 | lindfpropd.6 | |
|
7 | lindfpropd.k | |
|
8 | lindfpropd.l | |
|
9 | 1 | sseq2d | |
10 | vex | |
|
11 | 10 | a1i | |
12 | 11 | resiexd | |
13 | 1 2 3 4 5 6 7 8 12 | lindfpropd | |
14 | 9 13 | anbi12d | |
15 | eqid | |
|
16 | 15 | islinds | |
17 | 7 16 | syl | |
18 | eqid | |
|
19 | 18 | islinds | |
20 | 8 19 | syl | |
21 | 14 17 20 | 3bitr4d | |
22 | 21 | eqrdv | |