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 35710
 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 35709 . 2 class 𝑃
2 vl . . 3 setvar 𝑙
3 cvv 3340 . . 3 class V
4 vm . . . 4 setvar 𝑚
52cv 1631 . . . . . 6 class 𝑙
6 catm 35071 . . . . . 6 class Atoms
75, 6cfv 6049 . . . . 5 class (Atoms‘𝑙)
87cpw 4302 . . . 4 class 𝒫 (Atoms‘𝑙)
9 vp . . . . . 6 setvar 𝑝
104cv 1631 . . . . . 6 class 𝑚
119cv 1631 . . . . . . . 8 class 𝑝
12 coc 16171 . . . . . . . . 9 class oc
135, 12cfv 6049 . . . . . . . 8 class (oc‘𝑙)
1411, 13cfv 6049 . . . . . . 7 class ((oc‘𝑙)‘𝑝)
15 cpmap 35304 . . . . . . . 8 class pmap
165, 15cfv 6049 . . . . . . 7 class (pmap‘𝑙)
1714, 16cfv 6049 . . . . . 6 class ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝))
189, 10, 17ciin 4673 . . . . 5 class 𝑝𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝))
197, 18cin 3714 . . . 4 class ((Atoms‘𝑙) ∩ 𝑝𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)))
204, 8, 19cmpt 4881 . . 3 class (𝑚 ∈ 𝒫 (Atoms‘𝑙) ↦ ((Atoms‘𝑙) ∩ 𝑝𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝))))
212, 3, 20cmpt 4881 . 2 class (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙) ↦ ((Atoms‘𝑙) ∩ 𝑝𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)))))
221, 21wceq 1632 1 wff 𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙) ↦ ((Atoms‘𝑙) ∩ 𝑝𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)))))
 Colors of variables: wff setvar class This definition is referenced by:  polfvalN  35711
 Copyright terms: Public domain W3C validator