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 37913
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 37912 . 2 class 𝑃
2 vl . . 3 setvar 𝑙
3 cvv 3431 . . 3 class V
4 vm . . . 4 setvar 𝑚
52cv 1541 . . . . . 6 class 𝑙
6 catm 37273 . . . . . 6 class Atoms
75, 6cfv 6432 . . . . 5 class (Atoms‘𝑙)
87cpw 4539 . . . 4 class 𝒫 (Atoms‘𝑙)
9 vp . . . . . 6 setvar 𝑝
104cv 1541 . . . . . 6 class 𝑚
119cv 1541 . . . . . . . 8 class 𝑝
12 coc 16968 . . . . . . . . 9 class oc
135, 12cfv 6432 . . . . . . . 8 class (oc‘𝑙)
1411, 13cfv 6432 . . . . . . 7 class ((oc‘𝑙)‘𝑝)
15 cpmap 37507 . . . . . . . 8 class pmap
165, 15cfv 6432 . . . . . . 7 class (pmap‘𝑙)
1714, 16cfv 6432 . . . . . 6 class ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝))
189, 10, 17ciin 4931 . . . . 5 class 𝑝𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝))
197, 18cin 3891 . . . 4 class ((Atoms‘𝑙) ∩ 𝑝𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)))
204, 8, 19cmpt 5162 . . 3 class (𝑚 ∈ 𝒫 (Atoms‘𝑙) ↦ ((Atoms‘𝑙) ∩ 𝑝𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝))))
212, 3, 20cmpt 5162 . 2 class (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙) ↦ ((Atoms‘𝑙) ∩ 𝑝𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)))))
221, 21wceq 1542 1 wff 𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙) ↦ ((Atoms‘𝑙) ∩ 𝑝𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)))))
Colors of variables: wff setvar class
This definition is referenced by:  polfvalN  37914
  Copyright terms: Public domain W3C validator