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

Metamath Proof Explorer

Theorem olm12

Description: The meet of an ortholattice element with one equals itself. (Contributed by NM, 22-May-2012)

Ref Expression
Hypotheses olm1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
olm1.m ⊢ ∧ = ( meet ‘ 𝐾 )
olm1.u ⊢ 1 = ( 1. ‘ 𝐾 )
Assertion olm12 ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( 1 ∧ 𝑋 ) = 𝑋 )

Proof

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