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 e. OL /\ X e. 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 e. OL -> K e. Lat )
5	4	adantr	|- ( ( K e. OL /\ X e. B ) -> K e. Lat )
6		olop	|- ( K e. OL -> K e. OP )
7	6	adantr	|- ( ( K e. OL /\ X e. B ) -> K e. OP )
8	1 3	op1cl	|- ( K e. OP -> .1. e. B )
9	7 8	syl	|- ( ( K e. OL /\ X e. B ) -> .1. e. B )
10		simpr	|- ( ( K e. OL /\ X e. B ) -> X e. B )
11	1 2	latmcom	|- ( ( K e. Lat /\ .1. e. B /\ X e. B ) -> ( .1. ./\ X ) = ( X ./\ .1. ) )
12	5 9 10 11	syl3anc	|- ( ( K e. OL /\ X e. B ) -> ( .1. ./\ X ) = ( X ./\ .1. ) )
13	1 2 3	olm11	|- ( ( K e. OL /\ X e. B ) -> ( X ./\ .1. ) = X )
14	12 13	eqtrd	|- ( ( K e. OL /\ X e. B ) -> ( .1. ./\ X ) = X )