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 39269
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 39268 . 2 class +𝑃
2 vl . . 3 setvar 𝑙
3 cvv 3471 . . 3 class V
4 vm . . . 4 setvar 𝑚
5 vn . . . 4 setvar 𝑛
62cv 1533 . . . . . 6 class 𝑙
7 catm 38735 . . . . . 6 class Atoms
86, 7cfv 6548 . . . . 5 class (Atoms‘𝑙)
98cpw 4603 . . . 4 class 𝒫 (Atoms‘𝑙)
104cv 1533 . . . . . 6 class 𝑚
115cv 1533 . . . . . 6 class 𝑛
1210, 11cun 3945 . . . . 5 class (𝑚𝑛)
13 vp . . . . . . . . . 10 setvar 𝑝
1413cv 1533 . . . . . . . . 9 class 𝑝
15 vq . . . . . . . . . . 11 setvar 𝑞
1615cv 1533 . . . . . . . . . 10 class 𝑞
17 vr . . . . . . . . . . 11 setvar 𝑟
1817cv 1533 . . . . . . . . . 10 class 𝑟
19 cjn 18302 . . . . . . . . . . 11 class join
206, 19cfv 6548 . . . . . . . . . 10 class (join‘𝑙)
2116, 18, 20co 7420 . . . . . . . . 9 class (𝑞(join‘𝑙)𝑟)
22 cple 17239 . . . . . . . . . 10 class le
236, 22cfv 6548 . . . . . . . . 9 class (le‘𝑙)
2414, 21, 23wbr 5148 . . . . . . . 8 wff 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
2524, 17, 11wrex 3067 . . . . . . 7 wff 𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
2625, 15, 10wrex 3067 . . . . . 6 wff 𝑞𝑚𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)
2726, 13, 8crab 3429 . . . . 5 class {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞𝑚𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)}
2812, 27cun 3945 . . . 4 class ((𝑚𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞𝑚𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})
294, 5, 9, 9, 28cmpo 7422 . . 3 class (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞𝑚𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)}))
302, 3, 29cmpt 5231 . 2 class (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞𝑚𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})))
311, 30wceq 1534 1 wff +𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞𝑚𝑟𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})))
Colors of variables: wff setvar class
This definition is referenced by:  paddfval  39270
  Copyright terms: Public domain W3C validator