Definition df-padd 39798

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 39797	. 2 class +𝑃
2		vl	. . 3 setvar 𝑙
3		cvv 3480	. . 3 class V
4		vm	. . . 4 setvar 𝑚
5		vn	. . . 4 setvar 𝑛
6	2	cv 1539	. . . . . 6 class 𝑙
7		catm 39264	. . . . . 6 class Atoms
8	6, 7	cfv 6561	. . . . 5 class (Atoms‘𝑙)
9	8	cpw 4600	. . . 4 class 𝒫 (Atoms‘𝑙)
10	4	cv 1539	. . . . . 6 class 𝑚
11	5	cv 1539	. . . . . 6 class 𝑛
12	10, 11	cun 3949	. . . . 5 class (𝑚 ∪ 𝑛)
13		vp	. . . . . . . . . 10 setvar 𝑝
14	13	cv 1539	. . . . . . . . 9 class 𝑝
15		vq	. . . . . . . . . . 11 setvar 𝑞
16	15	cv 1539	. . . . . . . . . 10 class 𝑞
17		vr	. . . . . . . . . . 11 setvar 𝑟
18	17	cv 1539	. . . . . . . . . 10 class 𝑟
19		cjn 18357	. . . . . . . . . . 11 class join
20	6, 19	cfv 6561	. . . . . . . . . 10 class (join‘𝑙)
21	16, 18, 20	co 7431	. . . . . . . . 9 class (𝑞(join‘𝑙)𝑟)
22		cple 17304	. . . . . . . . . 10 class le
23	6, 22	cfv 6561	. . . . . . . . 9 class (le‘𝑙)
24	14, 21, 23	wbr 5143	. . . . . . . 8 wff 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
25	24, 17, 11	wrex 3070	. . . . . . 7 wff ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
26	25, 15, 10	wrex 3070	. . . . . 6 wff ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
27	26, 13, 8	crab 3436	. . . . 5 class {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)}
28	12, 27	cun 3949	. . . 4 class ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})
29	4, 5, 9, 9, 28	cmpo 7433	. . 3 class (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)}))
30	2, 3, 29	cmpt 5225	. 2 class (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})))
31	1, 30	wceq 1540	1 wff +𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})))

This definition is referenced by:  paddfval  39799