dihmeetbclemN

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihmeetc.b	$⊢ B = {Base}_{K}$
	dihmeetc.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihmeetc.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihmeetc.h	$⊢ H = LHyp (K)$
	dihmeetc.i	$⊢ I = DIsoH (K) (W)$
Assertion	dihmeetbclemN	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to I (X \underset{˙}{\land} Y) = (I (X) \cap I (Y)) \cap I (W)$

Proof

Step	Hyp	Ref	Expression
1		dihmeetc.b	$⊢ B = {Base}_{K}$
2		dihmeetc.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihmeetc.m	$⊢ \underset{˙}{\land} = meet (K)$
4		dihmeetc.h	$⊢ H = LHyp (K)$
5		dihmeetc.i	$⊢ I = DIsoH (K) (W)$
6		simp3	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} W$
7		simp1l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to K \in HL$
8	7	hllatd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to K \in Lat$
9		simp2l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to X \in B$
10		simp2r	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to Y \in B$
11	1 3	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
12	8 9 10 11	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to X \underset{˙}{\land} Y \in B$
13		simp1r	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to W \in H$
14	1 4	lhpbase	$⊢ W \in H \to W \in B$
15	13 14	syl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to W \in B$
16	1 2 3	latleeqm1	$⊢ (K \in Lat \land X \underset{˙}{\land} Y \in B \land W \in B) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} W \leftrightarrow (X \underset{˙}{\land} Y) \underset{˙}{\land} W = X \underset{˙}{\land} Y)$
17	8 12 15 16	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} W \leftrightarrow (X \underset{˙}{\land} Y) \underset{˙}{\land} W = X \underset{˙}{\land} Y)$
18	6 17	mpbid	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to (X \underset{˙}{\land} Y) \underset{˙}{\land} W = X \underset{˙}{\land} Y$
19		hlol	$⊢ K \in HL \to K \in OL$
20	7 19	syl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to K \in OL$
21	1 3	latmassOLD	$⊢ (K \in OL \land (X \in B \land Y \in B \land W \in B)) \to (X \underset{˙}{\land} Y) \underset{˙}{\land} W = X \underset{˙}{\land} (Y \underset{˙}{\land} W)$
22	20 9 10 15 21	syl13anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to (X \underset{˙}{\land} Y) \underset{˙}{\land} W = X \underset{˙}{\land} (Y \underset{˙}{\land} W)$
23	18 22	eqtr3d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to X \underset{˙}{\land} Y = X \underset{˙}{\land} (Y \underset{˙}{\land} W)$
24	23	fveq2d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to I (X \underset{˙}{\land} Y) = I (X \underset{˙}{\land} (Y \underset{˙}{\land} W))$
25		simp1	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to (K \in HL \land W \in H)$
26	1 3	latmcl	$⊢ (K \in Lat \land Y \in B \land W \in B) \to Y \underset{˙}{\land} W \in B$
27	8 10 15 26	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to Y \underset{˙}{\land} W \in B$
28	1 2 3	latmle2	$⊢ (K \in Lat \land Y \in B \land W \in B) \to (Y \underset{˙}{\land} W) \underset{˙}{\leq} W$
29	8 10 15 28	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to (Y \underset{˙}{\land} W) \underset{˙}{\leq} W$
30	1 2 3 4 5	dihmeetbN	$⊢ ((K \in HL \land W \in H) \land X \in B \land (Y \underset{˙}{\land} W \in B \land (Y \underset{˙}{\land} W) \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} (Y \underset{˙}{\land} W)) = I (X) \cap I (Y \underset{˙}{\land} W)$
31	25 9 27 29 30	syl112anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to I (X \underset{˙}{\land} (Y \underset{˙}{\land} W)) = I (X) \cap I (Y \underset{˙}{\land} W)$
32	1 2	latref	$⊢ (K \in Lat \land W \in B) \to W \underset{˙}{\leq} W$
33	8 15 32	syl2anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to W \underset{˙}{\leq} W$
34	1 2 3 4 5	dihmeetbN	$⊢ ((K \in HL \land W \in H) \land Y \in B \land (W \in B \land W \underset{˙}{\leq} W)) \to I (Y \underset{˙}{\land} W) = I (Y) \cap I (W)$
35	25 10 15 33 34	syl112anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to I (Y \underset{˙}{\land} W) = I (Y) \cap I (W)$
36	35	ineq2d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to I (X) \cap I (Y \underset{˙}{\land} W) = I (X) \cap (I (Y) \cap I (W))$
37	24 31 36	3eqtrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to I (X \underset{˙}{\land} Y) = I (X) \cap (I (Y) \cap I (W))$
38		inass	$⊢ (I (X) \cap I (Y)) \cap I (W) = I (X) \cap (I (Y) \cap I (W))$
39	37 38	syl6eqr	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to I (X \underset{˙}{\land} Y) = (I (X) \cap I (Y)) \cap I (W)$

Metamath Proof Explorer

Theorem dihmeetbclemN

Proof