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 35554
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 35553 . 2 class +𝑃
2 vl . . 3 setvar 𝑙
3 cvv 3328 . . 3 class V
4 vm . . . 4 setvar 𝑚
5 vn . . . 4 setvar 𝑛
62cv 1619 . . . . . 6 class 𝑙
7 catm 35022 . . . . . 6 class Atoms
86, 7cfv 6037 . . . . 5 class (Atoms‘𝑙)
98cpw 4290 . . . 4 class 𝒫 (Atoms‘𝑙)
104cv 1619 . . . . . 6 class 𝑚
115cv 1619 . . . . . 6 class 𝑛
1210, 11cun 3701 . . . . 5 class (𝑚𝑛)
13 vp . . . . . . . . . 10 setvar 𝑝
1413cv 1619 . . . . . . . . 9 class 𝑝
15 vq . . . . . . . . . . 11 setvar 𝑞
1615cv 1619 . . . . . . . . . 10 class 𝑞
17 vr . . . . . . . . . . 11 setvar 𝑟
1817cv 1619 . . . . . . . . . 10 class 𝑟
19 cjn 17116 . . . . . . . . . . 11 class join
206, 19cfv 6037 . . . . . . . . . 10 class (join‘𝑙)
2116, 18, 20co 6801 . . . . . . . . 9 class (𝑞(join‘𝑙)𝑟)
22 cple 16121 . . . . . . . . . 10 class le
236, 22cfv 6037 . . . . . . . . 9 class (le‘𝑙)
2414, 21, 23wbr 4792 . . . . . . . 8 wff 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
2524, 17, 11wrex 3039 . . . . . . 7 wff 𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
2625, 15, 10wrex 3039 . . . . . 6 wff 𝑞𝑚𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
2726, 13, 8crab 3042 . . . . 5 class {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞𝑚𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)}
2812, 27cun 3701 . . . 4 class ((𝑚𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞𝑚𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})
294, 5, 9, 9, 28cmpt2 6803 . . 3 class (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞𝑚𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)}))
302, 3, 29cmpt 4869 . 2 class (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞𝑚𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})))
311, 30wceq 1620 1 wff +𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞𝑚𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})))
Colors of variables: wff setvar class
This definition is referenced by:  paddfval  35555
  Copyright terms: Public domain W3C validator