Definition df-padd 40420

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 40419	. 2 class +𝑃
2		vl	. . 3 setvar 𝑙
3		cvv 3454	. . 3 class V
4		vm	. . . 4 setvar 𝑚
5		vn	. . . 4 setvar 𝑛
6	2	cv 1559	. . . . . 6 class 𝑙
7		catm 39887	. . . . . 6 class Atoms
8	6, 7	cfv 6521	. . . . 5 class (Atoms‘𝑙)
9	8	cpw 4555	. . . 4 class 𝒫 (Atoms‘𝑙)
10	4	cv 1559	. . . . . 6 class 𝑚
11	5	cv 1559	. . . . . 6 class 𝑛
12	10, 11	cun 3902	. . . . 5 class (𝑚 ∪ 𝑛)
13		vp	. . . . . . . . . 10 setvar 𝑝
14	13	cv 1559	. . . . . . . . 9 class 𝑝
15		vq	. . . . . . . . . . 11 setvar 𝑞
16	15	cv 1559	. . . . . . . . . 10 class 𝑞
17		vr	. . . . . . . . . . 11 setvar 𝑟
18	17	cv 1559	. . . . . . . . . 10 class 𝑟
19		cjn 18343	. . . . . . . . . . 11 class join
20	6, 19	cfv 6521	. . . . . . . . . 10 class (join‘𝑙)
21	16, 18, 20	co 7396	. . . . . . . . 9 class (𝑞(join‘𝑙)𝑟)
22		cple 17293	. . . . . . . . . 10 class le
23	6, 22	cfv 6521	. . . . . . . . 9 class (le‘𝑙)
24	14, 21, 23	wbr 5100	. . . . . . . 8 wff 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
25	24, 17, 11	wrex 3086	. . . . . . 7 wff ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
26	25, 15, 10	wrex 3086	. . . . . 6 wff ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
27	26, 13, 8	crab 3414	. . . . 5 class {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)}
28	12, 27	cun 3902	. . . 4 class ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})
29	4, 5, 9, 9, 28	cmpo 7398	. . 3 class (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)}))
30	2, 3, 29	cmpt 5181	. 2 class (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})))
31	1, 30	wceq 1560	1 wff +𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})))

This definition is referenced by:  paddfval  40421