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

Theorem polsubN 35795
Description: The polarity of a set of atoms is a projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
polsubsp.a 𝐴 = (Atoms‘𝐾)
polsubsp.s 𝑆 = (PSubSp‘𝐾)
polsubsp.p = (⊥𝑃𝐾)
Assertion
Ref Expression
polsubN ((𝐾 ∈ HL ∧ 𝑋𝐴) → ( 𝑋) ∈ 𝑆)

Proof of Theorem polsubN
StepHypRef Expression
1 eqid 2764 . . 3 (lub‘𝐾) = (lub‘𝐾)
2 eqid 2764 . . 3 (oc‘𝐾) = (oc‘𝐾)
3 polsubsp.a . . 3 𝐴 = (Atoms‘𝐾)
4 eqid 2764 . . 3 (pmap‘𝐾) = (pmap‘𝐾)
5 polsubsp.p . . 3 = (⊥𝑃𝐾)
61, 2, 3, 4, 5polval2N 35794 . 2 ((𝐾 ∈ HL ∧ 𝑋𝐴) → ( 𝑋) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))))
7 hllat 35251 . . . 4 (𝐾 ∈ HL → 𝐾 ∈ Lat)
87adantr 472 . . 3 ((𝐾 ∈ HL ∧ 𝑋𝐴) → 𝐾 ∈ Lat)
9 hlop 35250 . . . . 5 (𝐾 ∈ HL → 𝐾 ∈ OP)
109adantr 472 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝐴) → 𝐾 ∈ OP)
11 hlclat 35246 . . . . 5 (𝐾 ∈ HL → 𝐾 ∈ CLat)
12 eqid 2764 . . . . . . 7 (Base‘𝐾) = (Base‘𝐾)
1312, 3atssbase 35178 . . . . . 6 𝐴 ⊆ (Base‘𝐾)
14 sstr 3768 . . . . . 6 ((𝑋𝐴𝐴 ⊆ (Base‘𝐾)) → 𝑋 ⊆ (Base‘𝐾))
1513, 14mpan2 682 . . . . 5 (𝑋𝐴𝑋 ⊆ (Base‘𝐾))
1612, 1clatlubcl 17379 . . . . 5 ((𝐾 ∈ CLat ∧ 𝑋 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾))
1711, 15, 16syl2an 589 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝐴) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾))
1812, 2opoccl 35082 . . . 4 ((𝐾 ∈ OP ∧ ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾))
1910, 17, 18syl2anc 579 . . 3 ((𝐾 ∈ HL ∧ 𝑋𝐴) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾))
20 polsubsp.s . . . 4 𝑆 = (PSubSp‘𝐾)
2112, 20, 4pmapsub 35656 . . 3 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾)) → ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))) ∈ 𝑆)
228, 19, 21syl2anc 579 . 2 ((𝐾 ∈ HL ∧ 𝑋𝐴) → ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))) ∈ 𝑆)
236, 22eqeltrd 2843 1 ((𝐾 ∈ HL ∧ 𝑋𝐴) → ( 𝑋) ∈ 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652  wcel 2155  wss 3731  cfv 6067  Basecbs 16131  occoc 16223  lubclub 17209  Latclat 17312  CLatccla 17374  OPcops 35060  Atomscatm 35151  HLchlt 35238  PSubSpcpsubsp 35384  pmapcpmap 35385  𝑃cpolN 35790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-riotaBAD 34841
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-op 4340  df-uni 4594  df-iun 4677  df-iin 4678  df-br 4809  df-opab 4871  df-mpt 4888  df-id 5184  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-riota 6802  df-ov 6844  df-oprab 6845  df-undef 7601  df-proset 17195  df-poset 17213  df-lub 17241  df-glb 17242  df-join 17243  df-meet 17244  df-p1 17307  df-lat 17313  df-clat 17375  df-oposet 35064  df-ol 35066  df-oml 35067  df-ats 35155  df-atl 35186  df-cvlat 35210  df-hlat 35239  df-psubsp 35391  df-pmap 35392  df-polarityN 35791
This theorem is referenced by:  polssatN  35796  pclss2polN  35809  psubclsubN  35828  osumcllem1N  35844
  Copyright terms: Public domain W3C validator