Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-padd | Structured version Visualization version Unicode version |
Description: Define projective sum of two subspaces (or more generally two sets of atoms), which is the union of all lines generated by pairs of atoms from each subspace. Lemma 16.2 of [MaedaMaeda] p. 68. For convenience, our definition is generalized to apply to empty sets. (Contributed by NM, 29-Dec-2011.) |
Ref | Expression |
---|---|
df-padd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cpadd 35081 | . 2 | |
2 | vl | . . 3 | |
3 | cvv 3200 | . . 3 | |
4 | vm | . . . 4 | |
5 | vn | . . . 4 | |
6 | 2 | cv 1482 | . . . . . 6 |
7 | catm 34550 | . . . . . 6 | |
8 | 6, 7 | cfv 5888 | . . . . 5 |
9 | 8 | cpw 4158 | . . . 4 |
10 | 4 | cv 1482 | . . . . . 6 |
11 | 5 | cv 1482 | . . . . . 6 |
12 | 10, 11 | cun 3572 | . . . . 5 |
13 | vp | . . . . . . . . . 10 | |
14 | 13 | cv 1482 | . . . . . . . . 9 |
15 | vq | . . . . . . . . . . 11 | |
16 | 15 | cv 1482 | . . . . . . . . . 10 |
17 | vr | . . . . . . . . . . 11 | |
18 | 17 | cv 1482 | . . . . . . . . . 10 |
19 | cjn 16944 | . . . . . . . . . . 11 | |
20 | 6, 19 | cfv 5888 | . . . . . . . . . 10 |
21 | 16, 18, 20 | co 6650 | . . . . . . . . 9 |
22 | cple 15948 | . . . . . . . . . 10 | |
23 | 6, 22 | cfv 5888 | . . . . . . . . 9 |
24 | 14, 21, 23 | wbr 4653 | . . . . . . . 8 |
25 | 24, 17, 11 | wrex 2913 | . . . . . . 7 |
26 | 25, 15, 10 | wrex 2913 | . . . . . 6 |
27 | 26, 13, 8 | crab 2916 | . . . . 5 |
28 | 12, 27 | cun 3572 | . . . 4 |
29 | 4, 5, 9, 9, 28 | cmpt2 6652 | . . 3 |
30 | 2, 3, 29 | cmpt 4729 | . 2 |
31 | 1, 30 | wceq 1483 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: paddfval 35083 |
Copyright terms: Public domain | W3C validator |