Definition df-padd 37092

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 37091	. 2 class +𝑃
2		vl	. . 3 setvar 𝑙
3		cvv 3441	. . 3 class V
4		vm	. . . 4 setvar 𝑚
5		vn	. . . 4 setvar 𝑛
6	2	cv 1537	. . . . . 6 class 𝑙
7		catm 36559	. . . . . 6 class Atoms
8	6, 7	cfv 6324	. . . . 5 class (Atoms‘𝑙)
9	8	cpw 4497	. . . 4 class 𝒫 (Atoms‘𝑙)
10	4	cv 1537	. . . . . 6 class 𝑚
11	5	cv 1537	. . . . . 6 class 𝑛
12	10, 11	cun 3879	. . . . 5 class (𝑚 ∪ 𝑛)
13		vp	. . . . . . . . . 10 setvar 𝑝
14	13	cv 1537	. . . . . . . . 9 class 𝑝
15		vq	. . . . . . . . . . 11 setvar 𝑞
16	15	cv 1537	. . . . . . . . . 10 class 𝑞
17		vr	. . . . . . . . . . 11 setvar 𝑟
18	17	cv 1537	. . . . . . . . . 10 class 𝑟
19		cjn 17546	. . . . . . . . . . 11 class join
20	6, 19	cfv 6324	. . . . . . . . . 10 class (join‘𝑙)
21	16, 18, 20	co 7135	. . . . . . . . 9 class (𝑞(join‘𝑙)𝑟)
22		cple 16564	. . . . . . . . . 10 class le
23	6, 22	cfv 6324	. . . . . . . . 9 class (le‘𝑙)
24	14, 21, 23	wbr 5030	. . . . . . . 8 wff 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
25	24, 17, 11	wrex 3107	. . . . . . 7 wff ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
26	25, 15, 10	wrex 3107	. . . . . 6 wff ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
27	26, 13, 8	crab 3110	. . . . 5 class {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)}
28	12, 27	cun 3879	. . . 4 class ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})
29	4, 5, 9, 9, 28	cmpo 7137	. . 3 class (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)}))
30	2, 3, 29	cmpt 5110	. 2 class (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})))
31	1, 30	wceq 1538	1 wff +𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})))

This definition is referenced by:  paddfval  37093