Theorem pmapeq0

Description: A projective map value is zero iff its argument is lattice zero. (Contributed by NM, 27-Jan-2012)

	Ref	Expression
Hypotheses	pmapeq0.b	|- B = ( Base ` K )
	pmapeq0.z	|- .0. = ( 0. ` K )
	pmapeq0.m	|- M = ( pmap ` K )
Assertion	pmapeq0	|- ( ( K e. HL /\ X e. B ) -> ( ( M ` X ) = (/) <-> X = .0. ) )

Proof

Step	Hyp	Ref	Expression
1		pmapeq0.b	|- B = ( Base ` K )
2		pmapeq0.z	|- .0. = ( 0. ` K )
3		pmapeq0.m	|- M = ( pmap ` K )
4		hlatl	|- ( K e. HL -> K e. AtLat )
5	4	adantr	|- ( ( K e. HL /\ X e. B ) -> K e. AtLat )
6	2 3	pmap0	|- ( K e. AtLat -> ( M ` .0. ) = (/) )
7	5 6	syl	|- ( ( K e. HL /\ X e. B ) -> ( M ` .0. ) = (/) )
8	7	eqeq2d	|- ( ( K e. HL /\ X e. B ) -> ( ( M ` X ) = ( M ` .0. ) <-> ( M ` X ) = (/) ) )
9		hlop	|- ( K e. HL -> K e. OP )
10	9	adantr	|- ( ( K e. HL /\ X e. B ) -> K e. OP )
11	1 2	op0cl	|- ( K e. OP -> .0. e. B )
12	10 11	syl	|- ( ( K e. HL /\ X e. B ) -> .0. e. B )
13	1 3	pmap11	|- ( ( K e. HL /\ X e. B /\ .0. e. B ) -> ( ( M ` X ) = ( M ` .0. ) <-> X = .0. ) )
14	12 13	mpd3an3	|- ( ( K e. HL /\ X e. B ) -> ( ( M ` X ) = ( M ` .0. ) <-> X = .0. ) )
15	8 14	bitr3d	|- ( ( K e. HL /\ X e. B ) -> ( ( M ` X ) = (/) <-> X = .0. ) )