Theorem polatN

Description: The polarity of the singleton of an atom (i.e. a point). (Contributed by NM, 14-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	polat.o	|- ._|_ = ( oc ` K )
	polat.a	|- A = ( Atoms ` K )
	polat.m	|- M = ( pmap ` K )
	polat.p	|- P = ( _|_P ` K )
Assertion	polatN	|- ( ( K e. OL /\ Q e. A ) -> ( P ` { Q } ) = ( M ` ( ._|_ ` Q ) ) )

Proof

Step	Hyp	Ref	Expression
1		polat.o	|- ._|_ = ( oc ` K )
2		polat.a	|- A = ( Atoms ` K )
3		polat.m	|- M = ( pmap ` K )
4		polat.p	|- P = ( _|_P ` K )
5		snssi	|- ( Q e. A -> { Q } C_ A )
6	1 2 3 4	polvalN	|- ( ( K e. OL /\ { Q } C_ A ) -> ( P ` { Q } ) = ( A i^i |^|_ p e. { Q } ( M ` ( ._|_ ` p ) ) ) )
7	5 6	sylan2	|- ( ( K e. OL /\ Q e. A ) -> ( P ` { Q } ) = ( A i^i |^|_ p e. { Q } ( M ` ( ._|_ ` p ) ) ) )
8		2fveq3	|- ( p = Q -> ( M ` ( ._|_ ` p ) ) = ( M ` ( ._|_ ` Q ) ) )
9	8	iinxsng	|- ( Q e. A -> |^|_ p e. { Q } ( M ` ( ._|_ ` p ) ) = ( M ` ( ._|_ ` Q ) ) )
10	9	adantl	|- ( ( K e. OL /\ Q e. A ) -> |^|_ p e. { Q } ( M ` ( ._|_ ` p ) ) = ( M ` ( ._|_ ` Q ) ) )
11	10	ineq2d	|- ( ( K e. OL /\ Q e. A ) -> ( A i^i |^|_ p e. { Q } ( M ` ( ._|_ ` p ) ) ) = ( A i^i ( M ` ( ._|_ ` Q ) ) ) )
12		olop	|- ( K e. OL -> K e. OP )
13		eqid	|- ( Base ` K ) = ( Base ` K )
14	13 2	atbase	|- ( Q e. A -> Q e. ( Base ` K ) )
15	13 1	opoccl	|- ( ( K e. OP /\ Q e. ( Base ` K ) ) -> ( ._|_ ` Q ) e. ( Base ` K ) )
16	12 14 15	syl2an	|- ( ( K e. OL /\ Q e. A ) -> ( ._|_ ` Q ) e. ( Base ` K ) )
17	13 2 3	pmapssat	|- ( ( K e. OL /\ ( ._|_ ` Q ) e. ( Base ` K ) ) -> ( M ` ( ._|_ ` Q ) ) C_ A )
18	16 17	syldan	|- ( ( K e. OL /\ Q e. A ) -> ( M ` ( ._|_ ` Q ) ) C_ A )
19		sseqin2	|- ( ( M ` ( ._|_ ` Q ) ) C_ A <-> ( A i^i ( M ` ( ._|_ ` Q ) ) ) = ( M ` ( ._|_ ` Q ) ) )
20	18 19	sylib	|- ( ( K e. OL /\ Q e. A ) -> ( A i^i ( M ` ( ._|_ ` Q ) ) ) = ( M ` ( ._|_ ` Q ) ) )
21	7 11 20	3eqtrd	|- ( ( K e. OL /\ Q e. A ) -> ( P ` { Q } ) = ( M ` ( ._|_ ` Q ) ) )