Description: Define set of all projective subspaces. Based on definition of subspace in Holland95 p. 212. (Contributed by NM, 2-Oct-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | df-psubsp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cpsubsp | |
|
1 | vk | |
|
2 | cvv | |
|
3 | vs | |
|
4 | 3 | cv | |
5 | catm | |
|
6 | 1 | cv | |
7 | 6 5 | cfv | |
8 | 4 7 | wss | |
9 | vp | |
|
10 | vq | |
|
11 | vr | |
|
12 | 11 | cv | |
13 | cple | |
|
14 | 6 13 | cfv | |
15 | 9 | cv | |
16 | cjn | |
|
17 | 6 16 | cfv | |
18 | 10 | cv | |
19 | 15 18 17 | co | |
20 | 12 19 14 | wbr | |
21 | 12 4 | wcel | |
22 | 20 21 | wi | |
23 | 22 11 7 | wral | |
24 | 23 10 4 | wral | |
25 | 24 9 4 | wral | |
26 | 8 25 | wa | |
27 | 26 3 | cab | |
28 | 1 2 27 | cmpt | |
29 | 0 28 | wceq | |