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

Definition df-polarityN 39300
Description: Define polarity of projective subspace, which is a kind of complement of the subspace. Item 2 in [Holland95] p. 222 bottom. For more generality, we define it for all subsets of atoms, not just projective subspaces. The intersection with Atomsβ€˜π‘™ ensures it is defined when π‘š = βˆ…. (Contributed by NM, 23-Oct-2011.)
Assertion
Ref Expression
df-polarityN βŠ₯𝑃 = (𝑙 ∈ V ↦ (π‘š ∈ 𝒫 (Atomsβ€˜π‘™) ↦ ((Atomsβ€˜π‘™) ∩ ∩ 𝑝 ∈ π‘š ((pmapβ€˜π‘™)β€˜((ocβ€˜π‘™)β€˜π‘)))))
Distinct variable group:   π‘š,𝑙,𝑝

Detailed syntax breakdown of Definition df-polarityN
StepHypRef Expression
1 cpolN 39299 . 2 class βŠ₯𝑃
2 vl . . 3 setvar 𝑙
3 cvv 3469 . . 3 class V
4 vm . . . 4 setvar π‘š
52cv 1533 . . . . . 6 class 𝑙
6 catm 38659 . . . . . 6 class Atoms
75, 6cfv 6542 . . . . 5 class (Atomsβ€˜π‘™)
87cpw 4598 . . . 4 class 𝒫 (Atomsβ€˜π‘™)
9 vp . . . . . 6 setvar 𝑝
104cv 1533 . . . . . 6 class π‘š
119cv 1533 . . . . . . . 8 class 𝑝
12 coc 17226 . . . . . . . . 9 class oc
135, 12cfv 6542 . . . . . . . 8 class (ocβ€˜π‘™)
1411, 13cfv 6542 . . . . . . 7 class ((ocβ€˜π‘™)β€˜π‘)
15 cpmap 38894 . . . . . . . 8 class pmap
165, 15cfv 6542 . . . . . . 7 class (pmapβ€˜π‘™)
1714, 16cfv 6542 . . . . . 6 class ((pmapβ€˜π‘™)β€˜((ocβ€˜π‘™)β€˜π‘))
189, 10, 17ciin 4992 . . . . 5 class ∩ 𝑝 ∈ π‘š ((pmapβ€˜π‘™)β€˜((ocβ€˜π‘™)β€˜π‘))
197, 18cin 3943 . . . 4 class ((Atomsβ€˜π‘™) ∩ ∩ 𝑝 ∈ π‘š ((pmapβ€˜π‘™)β€˜((ocβ€˜π‘™)β€˜π‘)))
204, 8, 19cmpt 5225 . . 3 class (π‘š ∈ 𝒫 (Atomsβ€˜π‘™) ↦ ((Atomsβ€˜π‘™) ∩ ∩ 𝑝 ∈ π‘š ((pmapβ€˜π‘™)β€˜((ocβ€˜π‘™)β€˜π‘))))
212, 3, 20cmpt 5225 . 2 class (𝑙 ∈ V ↦ (π‘š ∈ 𝒫 (Atomsβ€˜π‘™) ↦ ((Atomsβ€˜π‘™) ∩ ∩ 𝑝 ∈ π‘š ((pmapβ€˜π‘™)β€˜((ocβ€˜π‘™)β€˜π‘)))))
221, 21wceq 1534 1 wff βŠ₯𝑃 = (𝑙 ∈ V ↦ (π‘š ∈ 𝒫 (Atomsβ€˜π‘™) ↦ ((Atomsβ€˜π‘™) ∩ ∩ 𝑝 ∈ π‘š ((pmapβ€˜π‘™)β€˜((ocβ€˜π‘™)β€˜π‘)))))
Colors of variables: wff setvar class
This definition is referenced by:  polfvalN  39301
  Copyright terms: Public domain W3C validator