omlspjN

Description: Contraction of a Sasaki projection. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		omlspj.b	$⊢ B = {Base}_{K}$
2		omlspj.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		omlspj.j	$⊢ \underset{˙}{\lor} = join (K)$
4		omlspj.m	$⊢ \underset{˙}{\land} = meet (K)$
5		omlspj.o	$⊢ \underset{˙}{⊥} = oc (K)$
6		omllat	$⊢ K \in OML \to K \in Lat$
7	6	3ad2ant1	$⊢ (K \in OML \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to K \in Lat$
8		omlop	$⊢ K \in OML \to K \in OP$
9	8	3ad2ant1	$⊢ (K \in OML \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to K \in OP$
10		simp2r	$⊢ (K \in OML \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to Y \in B$
11	1 5	opoccl	$⊢ (K \in OP \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
12	9 10 11	syl2anc	$⊢ (K \in OML \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to \underset{˙}{⊥} (Y) \in B$
13	1 4	latmcom	$⊢ (K \in Lat \land \underset{˙}{⊥} (Y) \in B \land Y \in B) \to \underset{˙}{⊥} (Y) \underset{˙}{\land} Y = Y \underset{˙}{\land} \underset{˙}{⊥} (Y)$
14	7 12 10 13	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to \underset{˙}{⊥} (Y) \underset{˙}{\land} Y = Y \underset{˙}{\land} \underset{˙}{⊥} (Y)$
15		eqid	$⊢ 0. (K) = 0. (K)$
16	1 5 4 15	opnoncon	$⊢ (K \in OP \land Y \in B) \to Y \underset{˙}{\land} \underset{˙}{⊥} (Y) = 0. (K)$
17	9 10 16	syl2anc	$⊢ (K \in OML \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to Y \underset{˙}{\land} \underset{˙}{⊥} (Y) = 0. (K)$
18	14 17	eqtrd	$⊢ (K \in OML \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to \underset{˙}{⊥} (Y) \underset{˙}{\land} Y = 0. (K)$
19	18	oveq2d	$⊢ (K \in OML \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to X \underset{˙}{\lor} (\underset{˙}{⊥} (Y) \underset{˙}{\land} Y) = X \underset{˙}{\lor} 0. (K)$
20		simp1	$⊢ (K \in OML \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to K \in OML$
21		simp2l	$⊢ (K \in OML \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to X \in B$
22		simp3	$⊢ (K \in OML \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to X \underset{˙}{\leq} Y$
23		eqid	$⊢ cm (K) = cm (K)$
24	1 23	cmtidN	$⊢ (K \in OML \land Y \in B) \to Y cm (K) Y$
25	20 10 24	syl2anc	$⊢ (K \in OML \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to Y cm (K) Y$
26	1 5 23	cmt3N	$⊢ (K \in OML \land Y \in B \land Y \in B) \to (Y cm (K) Y \leftrightarrow \underset{˙}{⊥} (Y) cm (K) Y)$
27	20 10 10 26	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to (Y cm (K) Y \leftrightarrow \underset{˙}{⊥} (Y) cm (K) Y)$
28	25 27	mpbid	$⊢ (K \in OML \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to \underset{˙}{⊥} (Y) cm (K) Y$
29	1 2 3 4 23	omlmod1i2N	$⊢ (K \in OML \land (X \in B \land \underset{˙}{⊥} (Y) \in B \land Y \in B) \land (X \underset{˙}{\leq} Y \land \underset{˙}{⊥} (Y) cm (K) Y)) \to X \underset{˙}{\lor} (\underset{˙}{⊥} (Y) \underset{˙}{\land} Y) = (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \underset{˙}{\land} Y$
30	20 21 12 10 22 28 29	syl132anc	$⊢ (K \in OML \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to X \underset{˙}{\lor} (\underset{˙}{⊥} (Y) \underset{˙}{\land} Y) = (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \underset{˙}{\land} Y$
31		omlol	$⊢ K \in OML \to K \in OL$
32	31	3ad2ant1	$⊢ (K \in OML \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to K \in OL$
33	1 3 15	olj01	$⊢ (K \in OL \land X \in B) \to X \underset{˙}{\lor} 0. (K) = X$
34	32 21 33	syl2anc	$⊢ (K \in OML \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to X \underset{˙}{\lor} 0. (K) = X$
35	19 30 34	3eqtr3d	$⊢ (K \in OML \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \underset{˙}{\land} Y = X$

Metamath Proof Explorer

Theorem omlspjN

Proof