Description: Define the relation between a module and its linearly independent subsets. (Contributed by AV, 12-Apr-2019) (Revised by AV, 24-Apr-2019) (Revised by AV, 30-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | df-lininds | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | clininds | |
|
1 | vs | |
|
2 | vm | |
|
3 | 1 | cv | |
4 | cbs | |
|
5 | 2 | cv | |
6 | 5 4 | cfv | |
7 | 6 | cpw | |
8 | 3 7 | wcel | |
9 | vf | |
|
10 | csca | |
|
11 | 5 10 | cfv | |
12 | 11 4 | cfv | |
13 | cmap | |
|
14 | 12 3 13 | co | |
15 | 9 | cv | |
16 | cfsupp | |
|
17 | c0g | |
|
18 | 11 17 | cfv | |
19 | 15 18 16 | wbr | |
20 | clinc | |
|
21 | 5 20 | cfv | |
22 | 15 3 21 | co | |
23 | 5 17 | cfv | |
24 | 22 23 | wceq | |
25 | 19 24 | wa | |
26 | vx | |
|
27 | 26 | cv | |
28 | 27 15 | cfv | |
29 | 28 18 | wceq | |
30 | 29 26 3 | wral | |
31 | 25 30 | wi | |
32 | 31 9 14 | wral | |
33 | 8 32 | wa | |
34 | 33 1 2 | copab | |
35 | 0 34 | wceq | |