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

Theorem polsubclN 40588
Description: A polarity is a closed projective subspace. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
polsubcl.a 𝐴 = (Atoms‘𝐾)
polsubcl.p = (⊥𝑃𝐾)
polsubcl.c 𝐶 = (PSubCl‘𝐾)
Assertion
Ref Expression
polsubclN ((𝐾 ∈ HL ∧ 𝑋𝐴) → ( 𝑋) ∈ 𝐶)

Proof of Theorem polsubclN
StepHypRef Expression
1 eqid 2765 . . 3 (lub‘𝐾) = (lub‘𝐾)
2 eqid 2765 . . 3 (oc‘𝐾) = (oc‘𝐾)
3 polsubcl.a . . 3 𝐴 = (Atoms‘𝐾)
4 eqid 2765 . . 3 (pmap‘𝐾) = (pmap‘𝐾)
5 polsubcl.p . . 3 = (⊥𝑃𝐾)
61, 2, 3, 4, 5polval2N 40542 . 2 ((𝐾 ∈ HL ∧ 𝑋𝐴) → ( 𝑋) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))))
7 hlop 39998 . . . . 5 (𝐾 ∈ HL → 𝐾 ∈ OP)
87adantr 485 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝐴) → 𝐾 ∈ OP)
9 hlclat 39994 . . . . 5 (𝐾 ∈ HL → 𝐾 ∈ CLat)
10 eqid 2765 . . . . . . 7 (Base‘𝐾) = (Base‘𝐾)
1110, 3atssbase 39926 . . . . . 6 𝐴 ⊆ (Base‘𝐾)
12 sstr 3947 . . . . . 6 ((𝑋𝐴𝐴 ⊆ (Base‘𝐾)) → 𝑋 ⊆ (Base‘𝐾))
1311, 12mpan2 703 . . . . 5 (𝑋𝐴𝑋 ⊆ (Base‘𝐾))
1410, 1clatlubcl 18549 . . . . 5 ((𝐾 ∈ CLat ∧ 𝑋 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾))
159, 13, 14syl2an 607 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝐴) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾))
1610, 2opoccl 39830 . . . 4 ((𝐾 ∈ OP ∧ ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾))
178, 15, 16syl2anc 595 . . 3 ((𝐾 ∈ HL ∧ 𝑋𝐴) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾))
18 polsubcl.c . . . 4 𝐶 = (PSubCl‘𝐾)
1910, 4, 18pmapsubclN 40582 . . 3 ((𝐾 ∈ HL ∧ ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾)) → ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))) ∈ 𝐶)
2017, 19syldan 602 . 2 ((𝐾 ∈ HL ∧ 𝑋𝐴) → ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))) ∈ 𝐶)
216, 20eqeltrd 2865 1 ((𝐾 ∈ HL ∧ 𝑋𝐴) → ( 𝑋) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 400   = wceq 1563  wcel 2145  wss 3907  cfv 6525  Basecbs 17259  occoc 17308  lubclub 18355  CLatccla 18544  OPcops 39808  Atomscatm 39899  HLchlt 39986  pmapcpmap 40133  𝑃cpolN 40538  PSubClcpscN 40570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722
This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-iin 4955  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-proset 18340  df-poset 18359  df-plt 18374  df-lub 18390  df-glb 18391  df-join 18392  df-meet 18393  df-p0 18469  df-p1 18470  df-lat 18478  df-clat 18545  df-oposet 39812  df-ol 39814  df-oml 39815  df-covers 39902  df-ats 39903  df-atl 39934  df-cvlat 39958  df-hlat 39987  df-pmap 40140  df-polarityN 40539  df-psubclN 40571
This theorem is referenced by:  osumcllem9N  40600  pexmidN  40605
  Copyright terms: Public domain W3C validator