omllaw2N

Description: Variation of orthomodular law. Definition of OML law in Kalmbach p. 22. ( pjoml2i analog.) (Contributed by NM, 6-Nov-2011) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		omllaw.b	$⊢ B = {Base}_{K}$
2		omllaw.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		omllaw.j	$⊢ \underset{˙}{\lor} = join (K)$
4		omllaw.m	$⊢ \underset{˙}{\land} = meet (K)$
5		omllaw.o	$⊢ \underset{˙}{⊥} = oc (K)$
6	1 2 3 4 5	omllaw	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \to Y = X \underset{˙}{\lor} (Y \underset{˙}{\land} \underset{˙}{⊥} (X)))$
7		eqcom	$⊢ X \underset{˙}{\lor} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) = Y \leftrightarrow Y = X \underset{˙}{\lor} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y)$
8		omllat	$⊢ K \in OML \to K \in Lat$
9	8	3ad2ant1	$⊢ (K \in OML \land X \in B \land Y \in B) \to K \in Lat$
10		omlop	$⊢ K \in OML \to K \in OP$
11	1 5	opoccl	$⊢ (K \in OP \land X \in B) \to \underset{˙}{⊥} (X) \in B$
12	10 11	sylan	$⊢ (K \in OML \land X \in B) \to \underset{˙}{⊥} (X) \in B$
13	12	3adant3	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \in B$
14		simp3	$⊢ (K \in OML \land X \in B \land Y \in B) \to Y \in B$
15	1 4	latmcom	$⊢ (K \in Lat \land \underset{˙}{⊥} (X) \in B \land Y \in B) \to \underset{˙}{⊥} (X) \underset{˙}{\land} Y = Y \underset{˙}{\land} \underset{˙}{⊥} (X)$
16	9 13 14 15	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \underset{˙}{\land} Y = Y \underset{˙}{\land} \underset{˙}{⊥} (X)$
17	16	oveq2d	$⊢ (K \in OML \land X \in B \land Y \in B) \to X \underset{˙}{\lor} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) = X \underset{˙}{\lor} (Y \underset{˙}{\land} \underset{˙}{⊥} (X))$
18	17	eqeq2d	$⊢ (K \in OML \land X \in B \land Y \in B) \to (Y = X \underset{˙}{\lor} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) \leftrightarrow Y = X \underset{˙}{\lor} (Y \underset{˙}{\land} \underset{˙}{⊥} (X)))$
19	7 18	bitrid	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X \underset{˙}{\lor} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) = Y \leftrightarrow Y = X \underset{˙}{\lor} (Y \underset{˙}{\land} \underset{˙}{⊥} (X)))$
20	6 19	sylibrd	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \to X \underset{˙}{\lor} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) = Y)$

Metamath Proof Explorer

Theorem omllaw2N

Proof