polsubclN - Mathbox for Norm Megill

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

Theorem polsubclN 40540

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**
Step	Hyp	Ref	Expression
1		eqid 2761	. . 3 ⊢ (lub‘𝐾) = (lub‘𝐾)
2		eqid 2761	. . 3 ⊢ (oc‘𝐾) = (oc‘𝐾)
3		polsubcl.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
4		eqid 2761	. . 3 ⊢ (pmap‘𝐾) = (pmap‘𝐾)
5		polsubcl.p	. . 3 ⊢ ⊥ = (⊥_𝑃‘𝐾)
6	1, 2, 3, 4, 5	polval2N 40494	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘𝑋) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))))
7		hlop 39950	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
8	7	adantr 484	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → 𝐾 ∈ OP)
9		hlclat 39946	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
10		eqid 2761	. . . . . . 7 ⊢ (Base‘𝐾) = (Base‘𝐾)
11	10, 3	atssbase 39878	. . . . . 6 ⊢ 𝐴 ⊆ (Base‘𝐾)
12		sstr 3944	. . . . . 6 ⊢ ((𝑋 ⊆ 𝐴 ∧ 𝐴 ⊆ (Base‘𝐾)) → 𝑋 ⊆ (Base‘𝐾))
13	11, 12	mpan2 701	. . . . 5 ⊢ (𝑋 ⊆ 𝐴 → 𝑋 ⊆ (Base‘𝐾))
14	10, 1	clatlubcl 18518	. . . . 5 ⊢ ((𝐾 ∈ CLat ∧ 𝑋 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾))
15	9, 13, 14	syl2an 605	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾))
16	10, 2	opoccl 39782	. . . 4 ⊢ ((𝐾 ∈ OP ∧ ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾))
17	8, 15, 16	syl2anc 593	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾))
18		polsubcl.c	. . . 4 ⊢ 𝐶 = (PSubCl‘𝐾)
19	10, 4, 18	pmapsubclN 40534	. . 3 ⊢ ((𝐾 ∈ HL ∧ ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾)) → ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))) ∈ 𝐶)
20	17, 19	syldan 600	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))) ∈ 𝐶)
21	6, 20	eqeltrd 2861	1 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘𝑋) ∈ 𝐶)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 = wceq 1559 ∈ wcel 2141 ⊆ wss 3904 ‘cfv 6517 Basecbs 17228 occoc 17277 lubclub 18324 CLatccla 18513 OPcops 39760 Atomscatm 39851 HLchlt 39938 pmapcpmap 40085 ⊥_𝑃cpolN 40490 PSubClcpscN 40522

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5321 ax-pr 5389 ax-un 7714

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-iun 4950 df-iin 4951 df-br 5100 df-opab 5162 df-mpt 5181 df-id 5540 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-res 5657 df-ima 5658 df-iota 6473 df-fun 6519 df-fn 6520 df-f 6521 df-f1 6522 df-fo 6523 df-f1o 6524 df-fv 6525 df-riota 7349 df-ov 7395 df-oprab 7396 df-proset 18309 df-poset 18328 df-plt 18343 df-lub 18359 df-glb 18360 df-join 18361 df-meet 18362 df-p0 18438 df-p1 18439 df-lat 18447 df-clat 18514 df-oposet 39764 df-ol 39766 df-oml 39767 df-covers 39854 df-ats 39855 df-atl 39886 df-cvlat 39910 df-hlat 39939 df-pmap 40092 df-polarityN 40491 df-psubclN 40523

This theorem is referenced by: osumcllem9N 40552 pexmidN 40557

W3C validator