Definition df-padd 38715

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 38714	. 2 class +𝑃
2		vl	. . 3 setvar 𝑙
3		cvv 3475	. . 3 class V
4		vm	. . . 4 setvar 𝑚
5		vn	. . . 4 setvar 𝑛
6	2	cv 1541	. . . . . 6 class 𝑙
7		catm 38181	. . . . . 6 class Atoms
8	6, 7	cfv 6544	. . . . 5 class (Atoms‘𝑙)
9	8	cpw 4603	. . . 4 class 𝒫 (Atoms‘𝑙)
10	4	cv 1541	. . . . . 6 class 𝑚
11	5	cv 1541	. . . . . 6 class 𝑛
12	10, 11	cun 3947	. . . . 5 class (𝑚 ∪ 𝑛)
13		vp	. . . . . . . . . 10 setvar 𝑝
14	13	cv 1541	. . . . . . . . 9 class 𝑝
15		vq	. . . . . . . . . . 11 setvar 𝑞
16	15	cv 1541	. . . . . . . . . 10 class 𝑞
17		vr	. . . . . . . . . . 11 setvar 𝑟
18	17	cv 1541	. . . . . . . . . 10 class 𝑟
19		cjn 18264	. . . . . . . . . . 11 class join
20	6, 19	cfv 6544	. . . . . . . . . 10 class (join‘𝑙)
21	16, 18, 20	co 7409	. . . . . . . . 9 class (𝑞(join‘𝑙)𝑟)
22		cple 17204	. . . . . . . . . 10 class le
23	6, 22	cfv 6544	. . . . . . . . 9 class (le‘𝑙)
24	14, 21, 23	wbr 5149	. . . . . . . 8 wff 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
25	24, 17, 11	wrex 3071	. . . . . . 7 wff ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
26	25, 15, 10	wrex 3071	. . . . . 6 wff ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
27	26, 13, 8	crab 3433	. . . . 5 class {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)}
28	12, 27	cun 3947	. . . 4 class ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})
29	4, 5, 9, 9, 28	cmpo 7411	. . 3 class (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)}))
30	2, 3, 29	cmpt 5232	. 2 class (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})))
31	1, 30	wceq 1542	1 wff +𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})))

This definition is referenced by:  paddfval  38716