Metamath Proof Explorer

Definition df-lpolN

Description: Define the set of all polarities of a left module or left vector space. A polarity is a kind of complementation operation on a subspace. The double polarity of a subspace is a closure operation. Based on Definition 3.2 of Holland95 p. 214 for projective geometry polarities. For convenience, we open up the domain to include all vector subsets and not just subspaces, but any more restricted polarity can be converted to this one by taking the span of its argument. (Contributed by NM, 24-Nov-2014)

Ref Expression
Assertion df-lpolN LPol = ( 𝑤 ∈ V ↦ { 𝑜 ∈ ( ( LSubSp ‘ 𝑤 ) ↑m 𝒫 ( Base ‘ 𝑤 ) ) ∣ ( ( 𝑜 ‘ ( Base ‘ 𝑤 ) ) = { ( 0g ‘ 𝑤 ) } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( LSAtoms ‘ 𝑤 ) ( ( 𝑜 ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑤 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clpoN ⊢ LPol
1 vw ⊢ 𝑤
2 cvv ⊢ V
3 vo ⊢ 𝑜
4 clss ⊢ LSubSp
5 1 cv ⊢ 𝑤
6 5 4 cfv ⊢ ( LSubSp ‘ 𝑤 )
7 cmap ⊢ ↑m
8 cbs ⊢ Base
9 5 8 cfv ⊢ ( Base ‘ 𝑤 )
10 9 cpw ⊢ 𝒫 ( Base ‘ 𝑤 )
11 6 10 7 co ⊢ ( ( LSubSp ‘ 𝑤 ) ↑m 𝒫 ( Base ‘ 𝑤 ) )
12 3 cv ⊢ 𝑜
13 9 12 cfv ⊢ ( 𝑜 ‘ ( Base ‘ 𝑤 ) )
14 c0g ⊢ 0g
15 5 14 cfv ⊢ ( 0g ‘ 𝑤 )
16 15 csn ⊢ { ( 0g ‘ 𝑤 ) }
17 13 16 wceq ⊢ ( 𝑜 ‘ ( Base ‘ 𝑤 ) ) = { ( 0g ‘ 𝑤 ) }
18 vx ⊢ 𝑥
19 vy ⊢ 𝑦
20 18 cv ⊢ 𝑥
21 20 9 wss ⊢ 𝑥 ⊆ ( Base ‘ 𝑤 )
22 19 cv ⊢ 𝑦
23 22 9 wss ⊢ 𝑦 ⊆ ( Base ‘ 𝑤 )
24 20 22 wss ⊢ 𝑥 ⊆ 𝑦
25 21 23 24 w3a ⊢ ( 𝑥 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑥 ⊆ 𝑦 )
26 22 12 cfv ⊢ ( 𝑜 ‘ 𝑦 )
27 20 12 cfv ⊢ ( 𝑜 ‘ 𝑥 )
28 26 27 wss ⊢ ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 )
29 25 28 wi ⊢ ( ( 𝑥 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) )
30 29 19 wal ⊢ ∀ 𝑦 ( ( 𝑥 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) )
31 30 18 wal ⊢ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) )
32 clsa ⊢ LSAtoms
33 5 32 cfv ⊢ ( LSAtoms ‘ 𝑤 )
34 clsh ⊢ LSHyp
35 5 34 cfv ⊢ ( LSHyp ‘ 𝑤 )
36 27 35 wcel ⊢ ( 𝑜 ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑤 )
37 27 12 cfv ⊢ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) )
38 37 20 wceq ⊢ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥
39 36 38 wa ⊢ ( ( 𝑜 ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑤 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 )
40 39 18 33 wral ⊢ ∀ 𝑥 ∈ ( LSAtoms ‘ 𝑤 ) ( ( 𝑜 ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑤 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 )
41 17 31 40 w3a ⊢ ( ( 𝑜 ‘ ( Base ‘ 𝑤 ) ) = { ( 0g ‘ 𝑤 ) } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( LSAtoms ‘ 𝑤 ) ( ( 𝑜 ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑤 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 ) )
42 41 3 11 crab ⊢ { 𝑜 ∈ ( ( LSubSp ‘ 𝑤 ) ↑m 𝒫 ( Base ‘ 𝑤 ) ) ∣ ( ( 𝑜 ‘ ( Base ‘ 𝑤 ) ) = { ( 0g ‘ 𝑤 ) } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( LSAtoms ‘ 𝑤 ) ( ( 𝑜 ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑤 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 ) ) }
43 1 2 42 cmpt ⊢ ( 𝑤 ∈ V ↦ { 𝑜 ∈ ( ( LSubSp ‘ 𝑤 ) ↑m 𝒫 ( Base ‘ 𝑤 ) ) ∣ ( ( 𝑜 ‘ ( Base ‘ 𝑤 ) ) = { ( 0g ‘ 𝑤 ) } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( LSAtoms ‘ 𝑤 ) ( ( 𝑜 ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑤 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 ) ) } )
44 0 43 wceq ⊢ LPol = ( 𝑤 ∈ V ↦ { 𝑜 ∈ ( ( LSubSp ‘ 𝑤 ) ↑m 𝒫 ( Base ‘ 𝑤 ) ) ∣ ( ( 𝑜 ‘ ( Base ‘ 𝑤 ) ) = { ( 0g ‘ 𝑤 ) } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( LSAtoms ‘ 𝑤 ) ( ( 𝑜 ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑤 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 ) ) } )