This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )