This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 → ( ⊥ ‘ 𝐴 ) = ∅ )