omllaw3

Description: Orthomodular law equivalent. Theorem 2(ii) of Kalmbach p. 22. ( pjoml analog.) (Contributed by NM, 19-Oct-2011)

	Ref	Expression
Hypotheses	omllaw3.b	$⊢ B = {Base}_{K}$
	omllaw3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	omllaw3.m	$⊢ \underset{˙}{\land} = meet (K)$
	omllaw3.o	$⊢ \underset{˙}{⊥} = oc (K)$
	omllaw3.z	$⊢ \underset{˙}{0} = 0. (K)$
Assertion	omllaw3	$⊢ (K \in OML \land X \in B \land Y \in B) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\land} \underset{˙}{⊥} (X) = \underset{˙}{0}) \to X = Y)$

Proof

Step	Hyp	Ref	Expression
1		omllaw3.b	$⊢ B = {Base}_{K}$
2		omllaw3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		omllaw3.m	$⊢ \underset{˙}{\land} = meet (K)$
4		omllaw3.o	$⊢ \underset{˙}{⊥} = oc (K)$
5		omllaw3.z	$⊢ \underset{˙}{0} = 0. (K)$
6		oveq2	$⊢ Y \underset{˙}{\land} \underset{˙}{⊥} (X) = \underset{˙}{0} \to X join (K) (Y \underset{˙}{\land} \underset{˙}{⊥} (X)) = X join (K) \underset{˙}{0}$
7	6	adantl	$⊢ ((K \in OML \land X \in B \land Y \in B) \land Y \underset{˙}{\land} \underset{˙}{⊥} (X) = \underset{˙}{0}) \to X join (K) (Y \underset{˙}{\land} \underset{˙}{⊥} (X)) = X join (K) \underset{˙}{0}$
8		omlol	$⊢ K \in OML \to K \in OL$
9		eqid	$⊢ join (K) = join (K)$
10	1 9 5	olj01	$⊢ (K \in OL \land X \in B) \to X join (K) \underset{˙}{0} = X$
11	8 10	sylan	$⊢ (K \in OML \land X \in B) \to X join (K) \underset{˙}{0} = X$
12	11	3adant3	$⊢ (K \in OML \land X \in B \land Y \in B) \to X join (K) \underset{˙}{0} = X$
13	12	adantr	$⊢ ((K \in OML \land X \in B \land Y \in B) \land Y \underset{˙}{\land} \underset{˙}{⊥} (X) = \underset{˙}{0}) \to X join (K) \underset{˙}{0} = X$
14	7 13	eqtr2d	$⊢ ((K \in OML \land X \in B \land Y \in B) \land Y \underset{˙}{\land} \underset{˙}{⊥} (X) = \underset{˙}{0}) \to X = X join (K) (Y \underset{˙}{\land} \underset{˙}{⊥} (X))$
15	14	adantrl	$⊢ ((K \in OML \land X \in B \land Y \in B) \land (X \underset{˙}{\leq} Y \land Y \underset{˙}{\land} \underset{˙}{⊥} (X) = \underset{˙}{0})) \to X = X join (K) (Y \underset{˙}{\land} \underset{˙}{⊥} (X))$
16	1 2 9 3 4	omllaw	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \to Y = X join (K) (Y \underset{˙}{\land} \underset{˙}{⊥} (X)))$
17	16	imp	$⊢ ((K \in OML \land X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to Y = X join (K) (Y \underset{˙}{\land} \underset{˙}{⊥} (X))$
18	17	adantrr	$⊢ ((K \in OML \land X \in B \land Y \in B) \land (X \underset{˙}{\leq} Y \land Y \underset{˙}{\land} \underset{˙}{⊥} (X) = \underset{˙}{0})) \to Y = X join (K) (Y \underset{˙}{\land} \underset{˙}{⊥} (X))$
19	15 18	eqtr4d	$⊢ ((K \in OML \land X \in B \land Y \in B) \land (X \underset{˙}{\leq} Y \land Y \underset{˙}{\land} \underset{˙}{⊥} (X) = \underset{˙}{0})) \to X = Y$
20	19	ex	$⊢ (K \in OML \land X \in B \land Y \in B) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\land} \underset{˙}{⊥} (X) = \underset{˙}{0}) \to X = Y)$

Metamath Proof Explorer

Theorem omllaw3

Proof