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 B = Base K
olm1.m ˙ = meet K
olm1.u 1 ˙ = 1. K
Assertion olm12 K OL X B 1 ˙ ˙ X = X

Proof

Step Hyp Ref Expression
1 olm1.b B = Base K
2 olm1.m ˙ = meet K
3 olm1.u 1 ˙ = 1. K
4 ollat K OL K Lat
5 4 adantr K OL X B K Lat
6 olop K OL K OP
7 6 adantr K OL X B K OP
8 1 3 op1cl K OP 1 ˙ B
9 7 8 syl K OL X B 1 ˙ B
10 simpr K OL X B X B
11 1 2 latmcom K Lat 1 ˙ B X B 1 ˙ ˙ X = X ˙ 1 ˙
12 5 9 10 11 syl3anc K OL X B 1 ˙ ˙ X = X ˙ 1 ˙
13 1 2 3 olm11 K OL X B X ˙ 1 ˙ = X
14 12 13 eqtrd K OL X B 1 ˙ ˙ X = X