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	⊢ 𝐵 = ( Base ‘ 𝐾 )
	pmapeq0.z	⊢ 0 = ( 0. ‘ 𝐾 )
	pmapeq0.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion	pmapeq0	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑋 ) = ∅ ↔ 𝑋 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		pmapeq0.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		pmapeq0.z	⊢ 0 = ( 0. ‘ 𝐾 )
3		pmapeq0.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
4		hlatl	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
5	4	adantr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ AtLat )
6	2 3	pmap0	⊢ ( 𝐾 ∈ AtLat → ( 𝑀 ‘ 0 ) = ∅ )
7	5 6	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 0 ) = ∅ )
8	7	eqeq2d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 0 ) ↔ ( 𝑀 ‘ 𝑋 ) = ∅ ) )
9		hlop	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
10	9	adantr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ OP )
11	1 2	op0cl	⊢ ( 𝐾 ∈ OP → 0 ∈ 𝐵 )
12	10 11	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → 0 ∈ 𝐵 )
13	1 3	pmap11	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 0 ) ↔ 𝑋 = 0 ) )
14	12 13	mpd3an3	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 0 ) ↔ 𝑋 = 0 ) )
15	8 14	bitr3d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑋 ) = ∅ ↔ 𝑋 = 0 ) )