polsubN

Description: The polarity of a set of atoms is a projective subspace. (Contributed by NM, 23-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	polsubsp.a	$⊢ A = Atoms (K)$
	polsubsp.s	$⊢ S = PSubSp (K)$
	polsubsp.p	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
Assertion	polsubN	$⊢ (K \in HL \land X \subseteq A) \to \underset{˙}{⊥} (X) \in S$

Step	Hyp	Ref	Expression
1		polsubsp.a	$⊢ A = Atoms (K)$
2		polsubsp.s	$⊢ S = PSubSp (K)$
3		polsubsp.p	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
4		eqid	$⊢ lub (K) = lub (K)$
5		eqid	$⊢ oc (K) = oc (K)$
6		eqid	$⊢ pmap (K) = pmap (K)$
7	4 5 1 6 3	polval2N	$⊢ (K \in HL \land X \subseteq A) \to \underset{˙}{⊥} (X) = pmap (K) (oc (K) (lub (K) (X)))$
8		hllat	$⊢ K \in HL \to K \in Lat$
9	8	adantr	$⊢ (K \in HL \land X \subseteq A) \to K \in Lat$
10		hlop	$⊢ K \in HL \to K \in OP$
11	10	adantr	$⊢ (K \in HL \land X \subseteq A) \to K \in OP$
12		hlclat	$⊢ K \in HL \to K \in CLat$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14	13 1	atssbase	$⊢ A \subseteq {Base}_{K}$
15		sstr	$⊢ (X \subseteq A \land A \subseteq {Base}_{K}) \to X \subseteq {Base}_{K}$
16	14 15	mpan2	$⊢ X \subseteq A \to X \subseteq {Base}_{K}$
17	13 4	clatlubcl	$⊢ (K \in CLat \land X \subseteq {Base}_{K}) \to lub (K) (X) \in {Base}_{K}$
18	12 16 17	syl2an	$⊢ (K \in HL \land X \subseteq A) \to lub (K) (X) \in {Base}_{K}$
19	13 5	opoccl	$⊢ (K \in OP \land lub (K) (X) \in {Base}_{K}) \to oc (K) (lub (K) (X)) \in {Base}_{K}$
20	11 18 19	syl2anc	$⊢ (K \in HL \land X \subseteq A) \to oc (K) (lub (K) (X)) \in {Base}_{K}$
21	13 2 6	pmapsub	$⊢ (K \in Lat \land oc (K) (lub (K) (X)) \in {Base}_{K}) \to pmap (K) (oc (K) (lub (K) (X))) \in S$
22	9 20 21	syl2anc	$⊢ (K \in HL \land X \subseteq A) \to pmap (K) (oc (K) (lub (K) (X))) \in S$
23	7 22	eqeltrd	$⊢ (K \in HL \land X \subseteq A) \to \underset{˙}{⊥} (X) \in S$

Metamath Proof Explorer