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 ∧ 𝑋 ) = 𝑋 )