Theorem 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	|- ._|_ = ( _|_P ` K )
	polsubcl.c	|- C = ( PSubCl ` K )
Assertion	polsubclN	|- ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` X ) e. C )

Proof

Step	Hyp	Ref	Expression
1		polsubcl.a	|- A = ( Atoms ` K )
2		polsubcl.p	|- ._|_ = ( _|_P ` 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 e. HL /\ X C_ A ) -> ( ._|_ ` X ) = ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) )
8		hlop	|- ( K e. HL -> K e. OP )
9	8	adantr	|- ( ( K e. HL /\ X C_ A ) -> K e. OP )
10		hlclat	|- ( K e. HL -> K e. CLat )
11		eqid	|- ( Base ` K ) = ( Base ` K )
12	11 1	atssbase	|- A C_ ( Base ` K )
13		sstr	|- ( ( X C_ A /\ A C_ ( Base ` K ) ) -> X C_ ( Base ` K ) )
14	12 13	mpan2	|- ( X C_ A -> X C_ ( Base ` K ) )
15	11 4	clatlubcl	|- ( ( K e. CLat /\ X C_ ( Base ` K ) ) -> ( ( lub ` K ) ` X ) e. ( Base ` K ) )
16	10 14 15	syl2an	|- ( ( K e. HL /\ X C_ A ) -> ( ( lub ` K ) ` X ) e. ( Base ` K ) )
17	11 5	opoccl	|- ( ( K e. OP /\ ( ( lub ` K ) ` X ) e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) e. ( Base ` K ) )
18	9 16 17	syl2anc	|- ( ( K e. HL /\ X C_ A ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) e. ( Base ` K ) )
19	11 6 3	pmapsubclN	|- ( ( K e. HL /\ ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) e. ( Base ` K ) ) -> ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) e. C )
20	18 19	syldan	|- ( ( K e. HL /\ X C_ A ) -> ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) e. C )
21	7 20	eqeltrd	|- ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` X ) e. C )