Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-padd Structured version   Visualization version   GIF version

Definition df-padd 36377
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
StepHypRef Expression
1 cpadd 36376 . 2 class +𝑃
2 vl . . 3 setvar 𝑙
3 cvv 3409 . . 3 class V
4 vm . . . 4 setvar 𝑚
5 vn . . . 4 setvar 𝑛
62cv 1506 . . . . . 6 class 𝑙
7 catm 35844 . . . . . 6 class Atoms
86, 7cfv 6182 . . . . 5 class (Atoms‘𝑙)
98cpw 4416 . . . 4 class 𝒫 (Atoms‘𝑙)
104cv 1506 . . . . . 6 class 𝑚
115cv 1506 . . . . . 6 class 𝑛
1210, 11cun 3821 . . . . 5 class (𝑚𝑛)
13 vp . . . . . . . . . 10 setvar 𝑝
1413cv 1506 . . . . . . . . 9 class 𝑝
15 vq . . . . . . . . . . 11 setvar 𝑞
1615cv 1506 . . . . . . . . . 10 class 𝑞
17 vr . . . . . . . . . . 11 setvar 𝑟
1817cv 1506 . . . . . . . . . 10 class 𝑟
19 cjn 17406 . . . . . . . . . . 11 class join
206, 19cfv 6182 . . . . . . . . . 10 class (join‘𝑙)
2116, 18, 20co 6970 . . . . . . . . 9 class (𝑞(join‘𝑙)𝑟)
22 cple 16422 . . . . . . . . . 10 class le
236, 22cfv 6182 . . . . . . . . 9 class (le‘𝑙)
2414, 21, 23wbr 4923 . . . . . . . 8 wff 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
2524, 17, 11wrex 3083 . . . . . . 7 wff 𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
2625, 15, 10wrex 3083 . . . . . 6 wff 𝑞𝑚𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
2726, 13, 8crab 3086 . . . . 5 class {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞𝑚𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)}
2812, 27cun 3821 . . . 4 class ((𝑚𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞𝑚𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})
294, 5, 9, 9, 28cmpo 6972 . . 3 class (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞𝑚𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)}))
302, 3, 29cmpt 5002 . 2 class (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞𝑚𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})))
311, 30wceq 1507 1 wff +𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞𝑚𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})))
Colors of variables: wff setvar class
This definition is referenced by:  paddfval  36378
  Copyright terms: Public domain W3C validator