Definition df-padd

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpadd	⊢ +𝑃
1		vl	⊢ 𝑙
2		cvv	⊢ V
3		vm	⊢ 𝑚
4		catm	⊢ Atoms
5	1	cv	⊢ 𝑙
6	5 4	cfv	⊢ ( Atoms ‘ 𝑙 )
7	6	cpw	⊢ 𝒫 ( Atoms ‘ 𝑙 )
8		vn	⊢ 𝑛
9	3	cv	⊢ 𝑚
10	8	cv	⊢ 𝑛
11	9 10	cun	⊢ ( 𝑚 ∪ 𝑛 )
12		vp	⊢ 𝑝
13		vq	⊢ 𝑞
14		vr	⊢ 𝑟
15	12	cv	⊢ 𝑝
16		cple	⊢ le
17	5 16	cfv	⊢ ( le ‘ 𝑙 )
18	13	cv	⊢ 𝑞
19		cjn	⊢ join
20	5 19	cfv	⊢ ( join ‘ 𝑙 )
21	14	cv	⊢ 𝑟
22	18 21 20	co	⊢ ( 𝑞 ( join ‘ 𝑙 ) 𝑟 )
23	15 22 17	wbr	⊢ 𝑝 ( le ‘ 𝑙 ) ( 𝑞 ( join ‘ 𝑙 ) 𝑟 )
24	23 14 10	wrex	⊢ ∃ 𝑟 ∈ 𝑛 𝑝 ( le ‘ 𝑙 ) ( 𝑞 ( join ‘ 𝑙 ) 𝑟 )
25	24 13 9	wrex	⊢ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ( le ‘ 𝑙 ) ( 𝑞 ( join ‘ 𝑙 ) 𝑟 )
26	25 12 6	crab	⊢ { 𝑝 ∈ ( Atoms ‘ 𝑙 ) ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ( le ‘ 𝑙 ) ( 𝑞 ( join ‘ 𝑙 ) 𝑟 ) }
27	11 26	cun	⊢ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ ( Atoms ‘ 𝑙 ) ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ( le ‘ 𝑙 ) ( 𝑞 ( join ‘ 𝑙 ) 𝑟 ) } )
28	3 8 7 7 27	cmpo	⊢ ( 𝑚 ∈ 𝒫 ( Atoms ‘ 𝑙 ) , 𝑛 ∈ 𝒫 ( Atoms ‘ 𝑙 ) ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ ( Atoms ‘ 𝑙 ) ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ( le ‘ 𝑙 ) ( 𝑞 ( join ‘ 𝑙 ) 𝑟 ) } ) )
29	1 2 28	cmpt	⊢ ( 𝑙 ∈ V ↦ ( 𝑚 ∈ 𝒫 ( Atoms ‘ 𝑙 ) , 𝑛 ∈ 𝒫 ( Atoms ‘ 𝑙 ) ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ ( Atoms ‘ 𝑙 ) ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ( le ‘ 𝑙 ) ( 𝑞 ( join ‘ 𝑙 ) 𝑟 ) } ) ) )
30	0 29	wceq	⊢ +𝑃 = ( 𝑙 ∈ V ↦ ( 𝑚 ∈ 𝒫 ( Atoms ‘ 𝑙 ) , 𝑛 ∈ 𝒫 ( Atoms ‘ 𝑙 ) ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ ( Atoms ‘ 𝑙 ) ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ( le ‘ 𝑙 ) ( 𝑞 ( join ‘ 𝑙 ) 𝑟 ) } ) ) )