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 38667
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 38666 . 2 class +𝑃
2 vl . . 3 setvar 𝑙
3 cvv 3475 . . 3 class V
4 vm . . . 4 setvar π‘š
5 vn . . . 4 setvar 𝑛
62cv 1541 . . . . . 6 class 𝑙
7 catm 38133 . . . . . 6 class Atoms
86, 7cfv 6544 . . . . 5 class (Atomsβ€˜π‘™)
98cpw 4603 . . . 4 class 𝒫 (Atomsβ€˜π‘™)
104cv 1541 . . . . . 6 class π‘š
115cv 1541 . . . . . 6 class 𝑛
1210, 11cun 3947 . . . . 5 class (π‘š βˆͺ 𝑛)
13 vp . . . . . . . . . 10 setvar 𝑝
1413cv 1541 . . . . . . . . 9 class 𝑝
15 vq . . . . . . . . . . 11 setvar π‘ž
1615cv 1541 . . . . . . . . . 10 class π‘ž
17 vr . . . . . . . . . . 11 setvar π‘Ÿ
1817cv 1541 . . . . . . . . . 10 class π‘Ÿ
19 cjn 18264 . . . . . . . . . . 11 class join
206, 19cfv 6544 . . . . . . . . . 10 class (joinβ€˜π‘™)
2116, 18, 20co 7409 . . . . . . . . 9 class (π‘ž(joinβ€˜π‘™)π‘Ÿ)
22 cple 17204 . . . . . . . . . 10 class le
236, 22cfv 6544 . . . . . . . . 9 class (leβ€˜π‘™)
2414, 21, 23wbr 5149 . . . . . . . 8 wff 𝑝(leβ€˜π‘™)(π‘ž(joinβ€˜π‘™)π‘Ÿ)
2524, 17, 11wrex 3071 . . . . . . 7 wff βˆƒπ‘Ÿ ∈ 𝑛 𝑝(leβ€˜π‘™)(π‘ž(joinβ€˜π‘™)π‘Ÿ)
2625, 15, 10wrex 3071 . . . . . 6 wff βˆƒπ‘ž ∈ π‘š βˆƒπ‘Ÿ ∈ 𝑛 𝑝(leβ€˜π‘™)(π‘ž(joinβ€˜π‘™)π‘Ÿ)
2726, 13, 8crab 3433 . . . . 5 class {𝑝 ∈ (Atomsβ€˜π‘™) ∣ βˆƒπ‘ž ∈ π‘š βˆƒπ‘Ÿ ∈ 𝑛 𝑝(leβ€˜π‘™)(π‘ž(joinβ€˜π‘™)π‘Ÿ)}
2812, 27cun 3947 . . . 4 class ((π‘š βˆͺ 𝑛) βˆͺ {𝑝 ∈ (Atomsβ€˜π‘™) ∣ βˆƒπ‘ž ∈ π‘š βˆƒπ‘Ÿ ∈ 𝑛 𝑝(leβ€˜π‘™)(π‘ž(joinβ€˜π‘™)π‘Ÿ)})
294, 5, 9, 9, 28cmpo 7411 . . 3 class (π‘š ∈ 𝒫 (Atomsβ€˜π‘™), 𝑛 ∈ 𝒫 (Atomsβ€˜π‘™) ↦ ((π‘š βˆͺ 𝑛) βˆͺ {𝑝 ∈ (Atomsβ€˜π‘™) ∣ βˆƒπ‘ž ∈ π‘š βˆƒπ‘Ÿ ∈ 𝑛 𝑝(leβ€˜π‘™)(π‘ž(joinβ€˜π‘™)π‘Ÿ)}))
302, 3, 29cmpt 5232 . 2 class (𝑙 ∈ V ↦ (π‘š ∈ 𝒫 (Atomsβ€˜π‘™), 𝑛 ∈ 𝒫 (Atomsβ€˜π‘™) ↦ ((π‘š βˆͺ 𝑛) βˆͺ {𝑝 ∈ (Atomsβ€˜π‘™) ∣ βˆƒπ‘ž ∈ π‘š βˆƒπ‘Ÿ ∈ 𝑛 𝑝(leβ€˜π‘™)(π‘ž(joinβ€˜π‘™)π‘Ÿ)})))
311, 30wceq 1542 1 wff +𝑃 = (𝑙 ∈ V ↦ (π‘š ∈ 𝒫 (Atomsβ€˜π‘™), 𝑛 ∈ 𝒫 (Atomsβ€˜π‘™) ↦ ((π‘š βˆͺ 𝑛) βˆͺ {𝑝 ∈ (Atomsβ€˜π‘™) ∣ βˆƒπ‘ž ∈ π‘š βˆƒπ‘Ÿ ∈ 𝑛 𝑝(leβ€˜π‘™)(π‘ž(joinβ€˜π‘™)π‘Ÿ)})))
Colors of variables: wff setvar class
This definition is referenced by:  paddfval  38668
  Copyright terms: Public domain W3C validator