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	$⊢ \underset{˙}{\land} = meet (K)$
	olm1.u	$⊢ \underset{˙}{1} = 1. (K)$
Assertion	olm12	$⊢ (K \in OL \land X \in B) \to \underset{˙}{1} \underset{˙}{\land} X = X$

Step	Hyp	Ref	Expression
1		olm1.b	$⊢ B = {Base}_{K}$
2		olm1.m	$⊢ \underset{˙}{\land} = meet (K)$
3		olm1.u	$⊢ \underset{˙}{1} = 1. (K)$
4		ollat	$⊢ K \in OL \to K \in Lat$
5	4	adantr	$⊢ (K \in OL \land X \in B) \to K \in Lat$
6		olop	$⊢ K \in OL \to K \in OP$
7	6	adantr	$⊢ (K \in OL \land X \in B) \to K \in OP$
8	1 3	op1cl	$⊢ K \in OP \to \underset{˙}{1} \in B$
9	7 8	syl	$⊢ (K \in OL \land X \in B) \to \underset{˙}{1} \in B$
10		simpr	$⊢ (K \in OL \land X \in B) \to X \in B$
11	1 2	latmcom	$⊢ (K \in Lat \land \underset{˙}{1} \in B \land X \in B) \to \underset{˙}{1} \underset{˙}{\land} X = X \underset{˙}{\land} \underset{˙}{1}$
12	5 9 10 11	syl3anc	$⊢ (K \in OL \land X \in B) \to \underset{˙}{1} \underset{˙}{\land} X = X \underset{˙}{\land} \underset{˙}{1}$
13	1 2 3	olm11	$⊢ (K \in OL \land X \in B) \to X \underset{˙}{\land} \underset{˙}{1} = X$
14	12 13	eqtrd	$⊢ (K \in OL \land X \in B) \to \underset{˙}{1} \underset{˙}{\land} X = X$

Metamath Proof Explorer