Metamath Proof Explorer

Definition df-padd

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
Assertion df-padd ⊢+𝑃=l∈V⟼m∈𝒫Atoms⁡l,n∈𝒫Atoms⁡l⟼m∪n∪p∈Atoms⁡l|∃q∈m∃r∈np≤lqjoin⁡lr

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpadd class+𝑃
1 vl setvarl
2 cvv classV
3 vm setvarm
4 catm classAtoms
5 1 cv setvarl
6 5 4 cfv classAtoms⁡l
7 6 cpw class𝒫Atoms⁡l
8 vn setvarn
9 3 cv setvarm
10 8 cv setvarn
11 9 10 cun classm∪n
12 vp setvarp
13 vq setvarq
14 vr setvarr
15 12 cv setvarp
16 cple classle
17 5 16 cfv class≤l
18 13 cv setvarq
19 cjn classjoin
20 5 19 cfv classjoin⁡l
21 14 cv setvarr
22 18 21 20 co classqjoin⁡lr
23 15 22 17 wbr wffp≤lqjoin⁡lr
24 23 14 10 wrex wff∃r∈np≤lqjoin⁡lr
25 24 13 9 wrex wff∃q∈m∃r∈np≤lqjoin⁡lr
26 25 12 6 crab classp∈Atoms⁡l|∃q∈m∃r∈np≤lqjoin⁡lr
27 11 26 cun classm∪n∪p∈Atoms⁡l|∃q∈m∃r∈np≤lqjoin⁡lr
28 3 8 7 7 27 cmpo classm∈𝒫Atoms⁡l,n∈𝒫Atoms⁡l⟼m∪n∪p∈Atoms⁡l|∃q∈m∃r∈np≤lqjoin⁡lr
29 1 2 28 cmpt classl∈V⟼m∈𝒫Atoms⁡l,n∈𝒫Atoms⁡l⟼m∪n∪p∈Atoms⁡l|∃q∈m∃r∈np≤lqjoin⁡lr
30 0 29 wceq wff+𝑃=l∈V⟼m∈𝒫Atoms⁡l,n∈𝒫Atoms⁡l⟼m∪n∪p∈Atoms⁡l|∃q∈m∃r∈np≤lqjoin⁡lr