omlmod1i2N

Description: Analogue of modular law atmod1i2 that holds in any OML. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	omlmod.b	$⊢ B = {Base}_{K}$
	omlmod.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	omlmod.j	$⊢ \underset{˙}{\lor} = join (K)$
	omlmod.m	$⊢ \underset{˙}{\land} = meet (K)$
	omlmod.c	$⊢ C = cm (K)$
Assertion	omlmod1i2N	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to X \underset{˙}{\lor} (Y \underset{˙}{\land} Z) = (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z$

Proof

Step	Hyp	Ref	Expression
1		omlmod.b	$⊢ B = {Base}_{K}$
2		omlmod.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		omlmod.j	$⊢ \underset{˙}{\lor} = join (K)$
4		omlmod.m	$⊢ \underset{˙}{\land} = meet (K)$
5		omlmod.c	$⊢ C = cm (K)$
6		simp1	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to K \in OML$
7		simp23	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to Z \in B$
8		simp21	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to X \in B$
9		simp22	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to Y \in B$
10		simp3l	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to X \underset{˙}{\leq} Z$
11	1 2 5	lecmtN	$⊢ (K \in OML \land X \in B \land Z \in B) \to (X \underset{˙}{\leq} Z \to X C Z)$
12	6 8 7 11	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to (X \underset{˙}{\leq} Z \to X C Z)$
13	10 12	mpd	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to X C Z$
14	1 5	cmtcomN	$⊢ (K \in OML \land X \in B \land Z \in B) \to (X C Z \leftrightarrow Z C X)$
15	6 8 7 14	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to (X C Z \leftrightarrow Z C X)$
16	13 15	mpbid	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to Z C X$
17		simp3r	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to Y C Z$
18	1 5	cmtcomN	$⊢ (K \in OML \land Y \in B \land Z \in B) \to (Y C Z \leftrightarrow Z C Y)$
19	6 9 7 18	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to (Y C Z \leftrightarrow Z C Y)$
20	17 19	mpbid	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to Z C Y$
21	1 3 4 5	omlfh1N	$⊢ (K \in OML \land (Z \in B \land X \in B \land Y \in B) \land (Z C X \land Z C Y)) \to Z \underset{˙}{\land} (X \underset{˙}{\lor} Y) = (Z \underset{˙}{\land} X) \underset{˙}{\lor} (Z \underset{˙}{\land} Y)$
22	6 7 8 9 16 20 21	syl132anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to Z \underset{˙}{\land} (X \underset{˙}{\lor} Y) = (Z \underset{˙}{\land} X) \underset{˙}{\lor} (Z \underset{˙}{\land} Y)$
23		omllat	$⊢ K \in OML \to K \in Lat$
24	23	3ad2ant1	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to K \in Lat$
25	1 3	latjcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y \in B$
26	24 8 9 25	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to X \underset{˙}{\lor} Y \in B$
27	1 4	latmcom	$⊢ (K \in Lat \land Z \in B \land X \underset{˙}{\lor} Y \in B) \to Z \underset{˙}{\land} (X \underset{˙}{\lor} Y) = (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z$
28	24 7 26 27	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to Z \underset{˙}{\land} (X \underset{˙}{\lor} Y) = (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z$
29	1 2 4	latleeqm2	$⊢ (K \in Lat \land X \in B \land Z \in B) \to (X \underset{˙}{\leq} Z \leftrightarrow Z \underset{˙}{\land} X = X)$
30	24 8 7 29	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to (X \underset{˙}{\leq} Z \leftrightarrow Z \underset{˙}{\land} X = X)$
31	10 30	mpbid	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to Z \underset{˙}{\land} X = X$
32	1 4	latmcom	$⊢ (K \in Lat \land Z \in B \land Y \in B) \to Z \underset{˙}{\land} Y = Y \underset{˙}{\land} Z$
33	24 7 9 32	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to Z \underset{˙}{\land} Y = Y \underset{˙}{\land} Z$
34	31 33	oveq12d	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to (Z \underset{˙}{\land} X) \underset{˙}{\lor} (Z \underset{˙}{\land} Y) = X \underset{˙}{\lor} (Y \underset{˙}{\land} Z)$
35	22 28 34	3eqtr3rd	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land Y C Z)) \to X \underset{˙}{\lor} (Y \underset{˙}{\land} Z) = (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z$

Metamath Proof Explorer

Theorem omlmod1i2N

Proof