polsubclN

Description: A polarity is a closed projective subspace. (Contributed by NM, 24-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	polsubcl.a	$⊢ A = Atoms (K)$
	polsubcl.p	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
	polsubcl.c	$⊢ C = PSubCl (K)$
Assertion	polsubclN	$⊢ (K \in HL \land X \subseteq A) \to \underset{˙}{⊥} (X) \in C$

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

Metamath Proof Explorer