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

Metamath Proof Explorer

Theorem olm02

Description: Meet with lattice zero is zero. (Contributed by NM, 9-Oct-2012)

Ref Expression
Hypotheses olm0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
olm0.m ⊢ ∧ = ( meet ‘ 𝐾 )
olm0.z ⊢ 0 = ( 0. ‘ 𝐾 )
Assertion olm02 ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( 0 ∧ 𝑋 ) = 0 )

Proof

Step Hyp Ref Expression
1 olm0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 olm0.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 olm0.z ⊢ 0 = ( 0. ‘ 𝐾 )
4 ollat ⊢ ( 𝐾 ∈ OL → 𝐾 ∈ Lat )
5 4 adantr ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ Lat )
6 simpr ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
7 olop ⊢ ( 𝐾 ∈ OL → 𝐾 ∈ OP )
8 7 adantr ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ OP )
9 1 3 op0cl ⊢ ( 𝐾 ∈ OP → 0 ∈ 𝐵 )
10 8 9 syl ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → 0 ∈ 𝐵 )
11 1 2 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → ( 𝑋 ∧ 0 ) = ( 0 ∧ 𝑋 ) )
12 5 6 10 11 syl3anc ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∧ 0 ) = ( 0 ∧ 𝑋 ) )
13 1 2 3 olm01 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∧ 0 ) = 0 )
14 12 13 eqtr3d ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( 0 ∧ 𝑋 ) = 0 )