Definition df-padd 40288

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.)

Assertion

Ref	Expression
df-padd	⊢ +𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})))

Distinct variable group:   𝑚,𝑙,𝑛,𝑝,𝑞,𝑟

Detailed syntax breakdown of Definition df-padd

Step	Hyp	Ref	Expression
1		cpadd 40287	. 2 class +𝑃
2		vl	. . 3 setvar 𝑙
3		cvv 3431	. . 3 class V
4		vm	. . . 4 setvar 𝑚
5		vn	. . . 4 setvar 𝑛
6	2	cv 1546	. . . . . 6 class 𝑙
7		catm 39755	. . . . . 6 class Atoms
8	6, 7	cfv 6485	. . . . 5 class (Atoms‘𝑙)
9	8	cpw 4529	. . . 4 class 𝒫 (Atoms‘𝑙)
10	4	cv 1546	. . . . . 6 class 𝑚
11	5	cv 1546	. . . . . 6 class 𝑛
12	10, 11	cun 3881	. . . . 5 class (𝑚 ∪ 𝑛)
13		vp	. . . . . . . . . 10 setvar 𝑝
14	13	cv 1546	. . . . . . . . 9 class 𝑝
15		vq	. . . . . . . . . . 11 setvar 𝑞
16	15	cv 1546	. . . . . . . . . 10 class 𝑞
17		vr	. . . . . . . . . . 11 setvar 𝑟
18	17	cv 1546	. . . . . . . . . 10 class 𝑟
19		cjn 18268	. . . . . . . . . . 11 class join
20	6, 19	cfv 6485	. . . . . . . . . 10 class (join‘𝑙)
21	16, 18, 20	co 7356	. . . . . . . . 9 class (𝑞(join‘𝑙)𝑟)
22		cple 17218	. . . . . . . . . 10 class le
23	6, 22	cfv 6485	. . . . . . . . 9 class (le‘𝑙)
24	14, 21, 23	wbr 5072	. . . . . . . 8 wff 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
25	24, 17, 11	wrex 3063	. . . . . . 7 wff ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
26	25, 15, 10	wrex 3063	. . . . . 6 wff ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
27	26, 13, 8	crab 3391	. . . . 5 class {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)}
28	12, 27	cun 3881	. . . 4 class ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})
29	4, 5, 9, 9, 28	cmpo 7358	. . 3 class (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)}))
30	2, 3, 29	cmpt 5153	. 2 class (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})))
31	1, 30	wceq 1547	1 wff +𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})))

This definition is referenced by:  paddfval  40289