Metamath Proof Explorer


Theorem pol1N

Description: The polarity of the whole projective subspace is the empty space. Remark in Holland95 p. 223. (Contributed by NM, 24-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses polssat.a 𝐴 = ( Atoms ‘ 𝐾 )
polssat.p = ( ⊥𝑃𝐾 )
Assertion pol1N ( 𝐾 ∈ HL → ( 𝐴 ) = ∅ )

Proof

Step Hyp Ref Expression
1 polssat.a 𝐴 = ( Atoms ‘ 𝐾 )
2 polssat.p = ( ⊥𝑃𝐾 )
3 ssid 𝐴𝐴
4 eqid ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
5 eqid ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
6 eqid ( pmap ‘ 𝐾 ) = ( pmap ‘ 𝐾 )
7 4 5 1 6 2 polval2N ( ( 𝐾 ∈ HL ∧ 𝐴𝐴 ) → ( 𝐴 ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
8 3 7 mpan2 ( 𝐾 ∈ HL → ( 𝐴 ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
9 hlop ( 𝐾 ∈ HL → 𝐾 ∈ OP )
10 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 10 1 atbase ( 𝑝𝐴𝑝 ∈ ( Base ‘ 𝐾 ) )
12 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
13 eqid ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
14 10 12 13 ople1 ( ( 𝐾 ∈ OP ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ) → 𝑝 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
15 9 11 14 syl2an ( ( 𝐾 ∈ HL ∧ 𝑝𝐴 ) → 𝑝 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
16 15 ralrimiva ( 𝐾 ∈ HL → ∀ 𝑝𝐴 𝑝 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
17 rabid2 ( 𝐴 = { 𝑝𝐴𝑝 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) } ↔ ∀ 𝑝𝐴 𝑝 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
18 16 17 sylibr ( 𝐾 ∈ HL → 𝐴 = { 𝑝𝐴𝑝 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) } )
19 18 fveq2d ( 𝐾 ∈ HL → ( ( lub ‘ 𝐾 ) ‘ 𝐴 ) = ( ( lub ‘ 𝐾 ) ‘ { 𝑝𝐴𝑝 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) } ) )
20 hlomcmat ( 𝐾 ∈ HL → ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) )
21 10 13 op1cl ( 𝐾 ∈ OP → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
22 9 21 syl ( 𝐾 ∈ HL → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
23 10 12 4 1 atlatmstc ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( lub ‘ 𝐾 ) ‘ { 𝑝𝐴𝑝 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) } ) = ( 1. ‘ 𝐾 ) )
24 20 22 23 syl2anc ( 𝐾 ∈ HL → ( ( lub ‘ 𝐾 ) ‘ { 𝑝𝐴𝑝 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) } ) = ( 1. ‘ 𝐾 ) )
25 19 24 eqtr2d ( 𝐾 ∈ HL → ( 1. ‘ 𝐾 ) = ( ( lub ‘ 𝐾 ) ‘ 𝐴 ) )
26 25 fveq2d ( 𝐾 ∈ HL → ( ( oc ‘ 𝐾 ) ‘ ( 1. ‘ 𝐾 ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝐴 ) ) )
27 eqid ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
28 27 13 5 opoc1 ( 𝐾 ∈ OP → ( ( oc ‘ 𝐾 ) ‘ ( 1. ‘ 𝐾 ) ) = ( 0. ‘ 𝐾 ) )
29 9 28 syl ( 𝐾 ∈ HL → ( ( oc ‘ 𝐾 ) ‘ ( 1. ‘ 𝐾 ) ) = ( 0. ‘ 𝐾 ) )
30 26 29 eqtr3d ( 𝐾 ∈ HL → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝐴 ) ) = ( 0. ‘ 𝐾 ) )
31 30 fveq2d ( 𝐾 ∈ HL → ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( 0. ‘ 𝐾 ) ) )
32 hlatl ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
33 27 6 pmap0 ( 𝐾 ∈ AtLat → ( ( pmap ‘ 𝐾 ) ‘ ( 0. ‘ 𝐾 ) ) = ∅ )
34 32 33 syl ( 𝐾 ∈ HL → ( ( pmap ‘ 𝐾 ) ‘ ( 0. ‘ 𝐾 ) ) = ∅ )
35 8 31 34 3eqtrd ( 𝐾 ∈ HL → ( 𝐴 ) = ∅ )