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 35677
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 35676 . 2 class 𝑃
2 vl . . 3 setvar 𝑙
3 cvv 3387 . . 3 class V
4 vm . . . 4 setvar 𝑚
52cv 1636 . . . . . 6 class 𝑙
6 catm 35037 . . . . . 6 class Atoms
75, 6cfv 6095 . . . . 5 class (Atoms‘𝑙)
87cpw 4345 . . . 4 class 𝒫 (Atoms‘𝑙)
9 vp . . . . . 6 setvar 𝑝
104cv 1636 . . . . . 6 class 𝑚
119cv 1636 . . . . . . . 8 class 𝑝
12 coc 16155 . . . . . . . . 9 class oc
135, 12cfv 6095 . . . . . . . 8 class (oc‘𝑙)
1411, 13cfv 6095 . . . . . . 7 class ((oc‘𝑙)‘𝑝)
15 cpmap 35271 . . . . . . . 8 class pmap
165, 15cfv 6095 . . . . . . 7 class (pmap‘𝑙)
1714, 16cfv 6095 . . . . . 6 class ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝))
189, 10, 17ciin 4706 . . . . 5 class 𝑝𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝))
197, 18cin 3762 . . . 4 class ((Atoms‘𝑙) ∩ 𝑝𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)))
204, 8, 19cmpt 4916 . . 3 class (𝑚 ∈ 𝒫 (Atoms‘𝑙) ↦ ((Atoms‘𝑙) ∩ 𝑝𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝))))
212, 3, 20cmpt 4916 . 2 class (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙) ↦ ((Atoms‘𝑙) ∩ 𝑝𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)))))
221, 21wceq 1637 1 wff 𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙) ↦ ((Atoms‘𝑙) ∩ 𝑝𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)))))
Colors of variables: wff setvar class
This definition is referenced by:  polfvalN  35678
  Copyright terms: Public domain W3C validator