olj01

Description: An ortholattice element joined with zero equals itself. ( chj0 analog.) (Contributed by NM, 19-Oct-2011)

	Ref	Expression
Hypotheses	olj0.b	$⊢ B = {Base}_{K}$
	olj0.j	$⊢ \underset{˙}{\lor} = join (K)$
	olj0.z	$⊢ \underset{˙}{0} = 0. (K)$
Assertion	olj01	$⊢ (K \in OL \land X \in B) \to X \underset{˙}{\lor} \underset{˙}{0} = X$

Proof

Step	Hyp	Ref	Expression
1		olj0.b	$⊢ B = {Base}_{K}$
2		olj0.j	$⊢ \underset{˙}{\lor} = join (K)$
3		olj0.z	$⊢ \underset{˙}{0} = 0. (K)$
4		olop	$⊢ K \in OL \to K \in OP$
5	1 3	op0cl	$⊢ K \in OP \to \underset{˙}{0} \in B$
6	4 5	syl	$⊢ K \in OL \to \underset{˙}{0} \in B$
7	6	adantr	$⊢ (K \in OL \land X \in B) \to \underset{˙}{0} \in B$
8		eqid	$⊢ \leq_{K} = \leq_{K}$
9		ollat	$⊢ K \in OL \to K \in Lat$
10	9	3ad2ant1	$⊢ (K \in OL \land X \in B \land \underset{˙}{0} \in B) \to K \in Lat$
11	1 2	latjcl	$⊢ (K \in Lat \land X \in B \land \underset{˙}{0} \in B) \to X \underset{˙}{\lor} \underset{˙}{0} \in B$
12	9 11	syl3an1	$⊢ (K \in OL \land X \in B \land \underset{˙}{0} \in B) \to X \underset{˙}{\lor} \underset{˙}{0} \in B$
13		simp2	$⊢ (K \in OL \land X \in B \land \underset{˙}{0} \in B) \to X \in B$
14	1 8	latref	$⊢ (K \in Lat \land X \in B) \to X \leq_{K} X$
15	9 14	sylan	$⊢ (K \in OL \land X \in B) \to X \leq_{K} X$
16	15	3adant3	$⊢ (K \in OL \land X \in B \land \underset{˙}{0} \in B) \to X \leq_{K} X$
17	1 8 3	op0le	$⊢ (K \in OP \land X \in B) \to \underset{˙}{0} \leq_{K} X$
18	4 17	sylan	$⊢ (K \in OL \land X \in B) \to \underset{˙}{0} \leq_{K} X$
19	18	3adant3	$⊢ (K \in OL \land X \in B \land \underset{˙}{0} \in B) \to \underset{˙}{0} \leq_{K} X$
20		simp3	$⊢ (K \in OL \land X \in B \land \underset{˙}{0} \in B) \to \underset{˙}{0} \in B$
21	1 8 2	latjle12	$⊢ (K \in Lat \land (X \in B \land \underset{˙}{0} \in B \land X \in B)) \to ((X \leq_{K} X \land \underset{˙}{0} \leq_{K} X) \leftrightarrow (X \underset{˙}{\lor} \underset{˙}{0}) \leq_{K} X)$
22	10 13 20 13 21	syl13anc	$⊢ (K \in OL \land X \in B \land \underset{˙}{0} \in B) \to ((X \leq_{K} X \land \underset{˙}{0} \leq_{K} X) \leftrightarrow (X \underset{˙}{\lor} \underset{˙}{0}) \leq_{K} X)$
23	16 19 22	mpbi2and	$⊢ (K \in OL \land X \in B \land \underset{˙}{0} \in B) \to (X \underset{˙}{\lor} \underset{˙}{0}) \leq_{K} X$
24	1 8 2	latlej1	$⊢ (K \in Lat \land X \in B \land \underset{˙}{0} \in B) \to X \leq_{K} (X \underset{˙}{\lor} \underset{˙}{0})$
25	9 24	syl3an1	$⊢ (K \in OL \land X \in B \land \underset{˙}{0} \in B) \to X \leq_{K} (X \underset{˙}{\lor} \underset{˙}{0})$
26	1 8 10 12 13 23 25	latasymd	$⊢ (K \in OL \land X \in B \land \underset{˙}{0} \in B) \to X \underset{˙}{\lor} \underset{˙}{0} = X$
27	7 26	mpd3an3	$⊢ (K \in OL \land X \in B) \to X \underset{˙}{\lor} \underset{˙}{0} = X$

Metamath Proof Explorer

Theorem olj01

Proof