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 ∈ n p ≤ l q join ⁡ l r

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpadd class + 𝑃
1 vl setvar l
2 cvv class V
3 vm setvar m
4 catm class Atoms
5 1 cv setvar l
6 5 4 cfv class Atoms ⁡ l
7 6 cpw class 𝒫 Atoms ⁡ l
8 vn setvar n
9 3 cv setvar m
10 8 cv setvar n
11 9 10 cun class m ∪ n
12 vp setvar p
13 vq setvar q
14 vr setvar r
15 12 cv setvar p
16 cple class le
17 5 16 cfv class ≤ l
18 13 cv setvar q
19 cjn class join
20 5 19 cfv class join ⁡ l
21 14 cv setvar r
22 18 21 20 co class q join ⁡ l r
23 15 22 17 wbr wff p ≤ l q join ⁡ l r
24 23 14 10 wrex wff ∃ r ∈ n p ≤ l q join ⁡ l r
25 24 13 9 wrex wff ∃ q ∈ m ∃ r ∈ n p ≤ l q join ⁡ l r
26 25 12 6 crab class p ∈ Atoms ⁡ l | ∃ q ∈ m ∃ r ∈ n p ≤ l q join ⁡ l r
27 11 26 cun class m ∪ n ∪ p ∈ Atoms ⁡ l | ∃ q ∈ m ∃ r ∈ n p ≤ l q join ⁡ l r
28 3 8 7 7 27 cmpo class m ∈ 𝒫 Atoms ⁡ l , n ∈ 𝒫 Atoms ⁡ l ⟼ m ∪ n ∪ p ∈ Atoms ⁡ l | ∃ q ∈ m ∃ r ∈ n p ≤ l q join ⁡ l r
29 1 2 28 cmpt class l ∈ V ⟼ m ∈ 𝒫 Atoms ⁡ l , n ∈ 𝒫 Atoms ⁡ l ⟼ m ∪ n ∪ p ∈ Atoms ⁡ l | ∃ q ∈ m ∃ r ∈ n p ≤ l q join ⁡ l r
30 0 29 wceq wff + 𝑃 = l ∈ V ⟼ m ∈ 𝒫 Atoms ⁡ l , n ∈ 𝒫 Atoms ⁡ l ⟼ m ∪ n ∪ p ∈ Atoms ⁡ l | ∃ q ∈ m ∃ r ∈ n p ≤ l q join ⁡ l r