Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pol1N Structured version   Visualization version   GIF version

Theorem pol1N 37688
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.)
Hypotheses
Ref Expression
polssat.a 𝐴 = (Atoms‘𝐾)
polssat.p = (⊥𝑃𝐾)
Assertion
Ref Expression
pol1N (𝐾 ∈ HL → ( 𝐴) = ∅)

Proof of Theorem pol1N
Dummy variable 𝑝 is distinct from all other variables.
StepHypRef Expression
1 ssid 3938 . . 3 𝐴𝐴
2 eqid 2738 . . . 4 (lub‘𝐾) = (lub‘𝐾)
3 eqid 2738 . . . 4 (oc‘𝐾) = (oc‘𝐾)
4 polssat.a . . . 4 𝐴 = (Atoms‘𝐾)
5 eqid 2738 . . . 4 (pmap‘𝐾) = (pmap‘𝐾)
6 polssat.p . . . 4 = (⊥𝑃𝐾)
72, 3, 4, 5, 6polval2N 37684 . . 3 ((𝐾 ∈ HL ∧ 𝐴𝐴) → ( 𝐴) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝐴))))
81, 7mpan2 691 . 2 (𝐾 ∈ HL → ( 𝐴) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝐴))))
9 hlop 37140 . . . . . . . . . 10 (𝐾 ∈ HL → 𝐾 ∈ OP)
10 eqid 2738 . . . . . . . . . . 11 (Base‘𝐾) = (Base‘𝐾)
1110, 4atbase 37067 . . . . . . . . . 10 (𝑝𝐴𝑝 ∈ (Base‘𝐾))
12 eqid 2738 . . . . . . . . . . 11 (le‘𝐾) = (le‘𝐾)
13 eqid 2738 . . . . . . . . . . 11 (1.‘𝐾) = (1.‘𝐾)
1410, 12, 13ople1 36969 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ 𝑝 ∈ (Base‘𝐾)) → 𝑝(le‘𝐾)(1.‘𝐾))
159, 11, 14syl2an 599 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑝𝐴) → 𝑝(le‘𝐾)(1.‘𝐾))
1615ralrimiva 3106 . . . . . . . 8 (𝐾 ∈ HL → ∀𝑝𝐴 𝑝(le‘𝐾)(1.‘𝐾))
17 rabid2 3306 . . . . . . . 8 (𝐴 = {𝑝𝐴𝑝(le‘𝐾)(1.‘𝐾)} ↔ ∀𝑝𝐴 𝑝(le‘𝐾)(1.‘𝐾))
1816, 17sylibr 237 . . . . . . 7 (𝐾 ∈ HL → 𝐴 = {𝑝𝐴𝑝(le‘𝐾)(1.‘𝐾)})
1918fveq2d 6740 . . . . . 6 (𝐾 ∈ HL → ((lub‘𝐾)‘𝐴) = ((lub‘𝐾)‘{𝑝𝐴𝑝(le‘𝐾)(1.‘𝐾)}))
20 hlomcmat 37143 . . . . . . 7 (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat))
2110, 13op1cl 36963 . . . . . . . 8 (𝐾 ∈ OP → (1.‘𝐾) ∈ (Base‘𝐾))
229, 21syl 17 . . . . . . 7 (𝐾 ∈ HL → (1.‘𝐾) ∈ (Base‘𝐾))
2310, 12, 2, 4atlatmstc 37097 . . . . . . 7 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ (1.‘𝐾) ∈ (Base‘𝐾)) → ((lub‘𝐾)‘{𝑝𝐴𝑝(le‘𝐾)(1.‘𝐾)}) = (1.‘𝐾))
2420, 22, 23syl2anc 587 . . . . . 6 (𝐾 ∈ HL → ((lub‘𝐾)‘{𝑝𝐴𝑝(le‘𝐾)(1.‘𝐾)}) = (1.‘𝐾))
2519, 24eqtr2d 2779 . . . . 5 (𝐾 ∈ HL → (1.‘𝐾) = ((lub‘𝐾)‘𝐴))
2625fveq2d 6740 . . . 4 (𝐾 ∈ HL → ((oc‘𝐾)‘(1.‘𝐾)) = ((oc‘𝐾)‘((lub‘𝐾)‘𝐴)))
27 eqid 2738 . . . . . 6 (0.‘𝐾) = (0.‘𝐾)
2827, 13, 3opoc1 36980 . . . . 5 (𝐾 ∈ OP → ((oc‘𝐾)‘(1.‘𝐾)) = (0.‘𝐾))
299, 28syl 17 . . . 4 (𝐾 ∈ HL → ((oc‘𝐾)‘(1.‘𝐾)) = (0.‘𝐾))
3026, 29eqtr3d 2780 . . 3 (𝐾 ∈ HL → ((oc‘𝐾)‘((lub‘𝐾)‘𝐴)) = (0.‘𝐾))
3130fveq2d 6740 . 2 (𝐾 ∈ HL → ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝐴))) = ((pmap‘𝐾)‘(0.‘𝐾)))
32 hlatl 37138 . . 3 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
3327, 5pmap0 37543 . . 3 (𝐾 ∈ AtLat → ((pmap‘𝐾)‘(0.‘𝐾)) = ∅)
3432, 33syl 17 . 2 (𝐾 ∈ HL → ((pmap‘𝐾)‘(0.‘𝐾)) = ∅)
358, 31, 343eqtrd 2782 1 (𝐾 ∈ HL → ( 𝐴) = ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1089   = wceq 1543  wcel 2111  wral 3062  {crab 3066  wss 3881  c0 4252   class class class wbr 5068  cfv 6398  Basecbs 16785  lecple 16834  occoc 16835  lubclub 17841  0.cp0 17954  1.cp1 17955  CLatccla 18029  OPcops 36950  OMLcoml 36953  Atomscatm 37041  AtLatcal 37042  HLchlt 37128  pmapcpmap 37275  𝑃cpolN 37680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-rep 5194  ax-sep 5207  ax-nul 5214  ax-pow 5273  ax-pr 5337  ax-un 7542  ax-riotaBAD 36731
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3423  df-sbc 3710  df-csb 3827  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4253  df-if 4455  df-pw 4530  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4835  df-iun 4921  df-iin 4922  df-br 5069  df-opab 5131  df-mpt 5151  df-id 5470  df-xp 5572  df-rel 5573  df-cnv 5574  df-co 5575  df-dm 5576  df-rn 5577  df-res 5578  df-ima 5579  df-iota 6356  df-fun 6400  df-fn 6401  df-f 6402  df-f1 6403  df-fo 6404  df-f1o 6405  df-fv 6406  df-riota 7189  df-ov 7235  df-oprab 7236  df-undef 8036  df-proset 17827  df-poset 17845  df-plt 17861  df-lub 17877  df-glb 17878  df-join 17879  df-meet 17880  df-p0 17956  df-p1 17957  df-lat 17963  df-clat 18030  df-oposet 36954  df-ol 36956  df-oml 36957  df-covers 37044  df-ats 37045  df-atl 37076  df-cvlat 37100  df-hlat 37129  df-pmap 37282  df-polarityN 37681
This theorem is referenced by:  2pol0N  37689  1psubclN  37722
  Copyright terms: Public domain W3C validator