Theorem polsubN 36593

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

Step	Hyp	Ref	Expression
1		eqid 2795	. . 3 ⊢ (lub‘𝐾) = (lub‘𝐾)
2		eqid 2795	. . 3 ⊢ (oc‘𝐾) = (oc‘𝐾)
3		polsubsp.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
4		eqid 2795	. . 3 ⊢ (pmap‘𝐾) = (pmap‘𝐾)
5		polsubsp.p	. . 3 ⊢ ⊥ = (⊥𝑃‘𝐾)
6	1, 2, 3, 4, 5	polval2N 36592	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘𝑋) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))))
7		hllat 36049	. . . 4 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
8	7	adantr 481	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → 𝐾 ∈ Lat)
9		hlop 36048	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
10	9	adantr 481	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → 𝐾 ∈ OP)
11		hlclat 36044	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
12		eqid 2795	. . . . . . 7 ⊢ (Base‘𝐾) = (Base‘𝐾)
13	12, 3	atssbase 35976	. . . . . 6 ⊢ 𝐴 ⊆ (Base‘𝐾)
14		sstr 3897	. . . . . 6 ⊢ ((𝑋 ⊆ 𝐴 ∧ 𝐴 ⊆ (Base‘𝐾)) → 𝑋 ⊆ (Base‘𝐾))
15	13, 14	mpan2 687	. . . . 5 ⊢ (𝑋 ⊆ 𝐴 → 𝑋 ⊆ (Base‘𝐾))
16	12, 1	clatlubcl 17551	. . . . 5 ⊢ ((𝐾 ∈ CLat ∧ 𝑋 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾))
17	11, 15, 16	syl2an 595	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾))
18	12, 2	opoccl 35880	. . . 4 ⊢ ((𝐾 ∈ OP ∧ ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾))
19	10, 17, 18	syl2anc 584	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾))
20		polsubsp.s	. . . 4 ⊢ 𝑆 = (PSubSp‘𝐾)
21	12, 20, 4	pmapsub 36454	. . 3 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾)) → ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))) ∈ 𝑆)
22	8, 19, 21	syl2anc 584	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))) ∈ 𝑆)
23	6, 22	eqeltrd 2883	1 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘𝑋) ∈ 𝑆)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522   ∈ wcel 2081   ⊆ wss 3859  ‘cfv 6225  Basecbs 16312  occoc 16402  lubclub 17381  Latclat 17484  CLatccla 17546  OPcops 35858  Atomscatm 35949  HLchlt 36036  PSubSpcpsubsp 36182  pmapcpmap 36183  ⊥_𝑃cpolN 36588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-riotaBAD 35639

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-iun 4827  df-iin 4828  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-riota 6977  df-ov 7019  df-oprab 7020  df-undef 7790  df-proset 17367  df-poset 17385  df-lub 17413  df-glb 17414  df-join 17415  df-meet 17416  df-p1 17479  df-lat 17485  df-clat 17547  df-oposet 35862  df-ol 35864  df-oml 35865  df-ats 35953  df-atl 35984  df-cvlat 36008  df-hlat 36037  df-psubsp 36189  df-pmap 36190  df-polarityN 36589

This theorem is referenced by:  polssatN  36594  pclss2polN  36607  psubclsubN  36626  osumcllem1N  36642