Definition df-polarityN

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 Atomsl ensures it is defined when m = (/) . (Contributed by NM, 23-Oct-2011)

	Ref	Expression
Assertion	df-polarityN	⊢ ⊥𝑃 = ( 𝑙 ∈ V ↦ ( 𝑚 ∈ 𝒫 ( Atoms ‘ 𝑙 ) ↦ ( ( Atoms ‘ 𝑙 ) ∩ ∩ 𝑝 ∈ 𝑚 ( ( pmap ‘ 𝑙 ) ‘ ( ( oc ‘ 𝑙 ) ‘ 𝑝 ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpolN	⊢ ⊥𝑃
1		vl	⊢ 𝑙
2		cvv	⊢ V
3		vm	⊢ 𝑚
4		catm	⊢ Atoms
5	1	cv	⊢ 𝑙
6	5 4	cfv	⊢ ( Atoms ‘ 𝑙 )
7	6	cpw	⊢ 𝒫 ( Atoms ‘ 𝑙 )
8		vp	⊢ 𝑝
9	3	cv	⊢ 𝑚
10		cpmap	⊢ pmap
11	5 10	cfv	⊢ ( pmap ‘ 𝑙 )
12		coc	⊢ oc
13	5 12	cfv	⊢ ( oc ‘ 𝑙 )
14	8	cv	⊢ 𝑝
15	14 13	cfv	⊢ ( ( oc ‘ 𝑙 ) ‘ 𝑝 )
16	15 11	cfv	⊢ ( ( pmap ‘ 𝑙 ) ‘ ( ( oc ‘ 𝑙 ) ‘ 𝑝 ) )
17	8 9 16	ciin	⊢ ∩ 𝑝 ∈ 𝑚 ( ( pmap ‘ 𝑙 ) ‘ ( ( oc ‘ 𝑙 ) ‘ 𝑝 ) )
18	6 17	cin	⊢ ( ( Atoms ‘ 𝑙 ) ∩ ∩ 𝑝 ∈ 𝑚 ( ( pmap ‘ 𝑙 ) ‘ ( ( oc ‘ 𝑙 ) ‘ 𝑝 ) ) )
19	3 7 18	cmpt	⊢ ( 𝑚 ∈ 𝒫 ( Atoms ‘ 𝑙 ) ↦ ( ( Atoms ‘ 𝑙 ) ∩ ∩ 𝑝 ∈ 𝑚 ( ( pmap ‘ 𝑙 ) ‘ ( ( oc ‘ 𝑙 ) ‘ 𝑝 ) ) ) )
20	1 2 19	cmpt	⊢ ( 𝑙 ∈ V ↦ ( 𝑚 ∈ 𝒫 ( Atoms ‘ 𝑙 ) ↦ ( ( Atoms ‘ 𝑙 ) ∩ ∩ 𝑝 ∈ 𝑚 ( ( pmap ‘ 𝑙 ) ‘ ( ( oc ‘ 𝑙 ) ‘ 𝑝 ) ) ) ) )
21	0 20	wceq	⊢ ⊥𝑃 = ( 𝑙 ∈ V ↦ ( 𝑚 ∈ 𝒫 ( Atoms ‘ 𝑙 ) ↦ ( ( Atoms ‘ 𝑙 ) ∩ ∩ 𝑝 ∈ 𝑚 ( ( pmap ‘ 𝑙 ) ‘ ( ( oc ‘ 𝑙 ) ‘ 𝑝 ) ) ) ) )