dihmeetlem11N

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

	Ref	Expression
Hypotheses	dihmeetlem9.b	$⊢ B = {Base}_{K}$
	dihmeetlem9.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihmeetlem9.h	$⊢ H = LHyp (K)$
	dihmeetlem9.j	$⊢ \underset{˙}{\lor} = join (K)$
	dihmeetlem9.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihmeetlem9.a	$⊢ A = Atoms (K)$
	dihmeetlem9.u	$⊢ U = DVecH (K) (W)$
	dihmeetlem9.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	dihmeetlem9.i	$⊢ I = DIsoH (K) (W)$
Assertion	dihmeetlem11N	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land p \underset{˙}{\leq} X)) \to I ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) \cap I (Y) = I (X) \cap I (Y)$

Proof

Step	Hyp	Ref	Expression
1		dihmeetlem9.b	$⊢ B = {Base}_{K}$
2		dihmeetlem9.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihmeetlem9.h	$⊢ H = LHyp (K)$
4		dihmeetlem9.j	$⊢ \underset{˙}{\lor} = join (K)$
5		dihmeetlem9.m	$⊢ \underset{˙}{\land} = meet (K)$
6		dihmeetlem9.a	$⊢ A = Atoms (K)$
7		dihmeetlem9.u	$⊢ U = DVecH (K) (W)$
8		dihmeetlem9.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
9		dihmeetlem9.i	$⊢ I = DIsoH (K) (W)$
10	1 2 3 4 5 6 7 8 9	dihmeetlem10N	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land p \underset{˙}{\leq} X)) \to I ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) = I (X) \cap I (Y \underset{˙}{\lor} p)$
11	10	ineq1d	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land p \underset{˙}{\leq} X)) \to I ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) \cap I (Y) = (I (X) \cap I (Y \underset{˙}{\lor} p)) \cap I (Y)$
12		inass	$⊢ (I (X) \cap I (Y \underset{˙}{\lor} p)) \cap I (Y) = I (X) \cap (I (Y \underset{˙}{\lor} p) \cap I (Y))$
13		simpl1l	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land p \underset{˙}{\leq} X)) \to K \in HL$
14	13	hllatd	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land p \underset{˙}{\leq} X)) \to K \in Lat$
15		simpl3	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land p \underset{˙}{\leq} X)) \to Y \in B$
16		simprll	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land p \underset{˙}{\leq} X)) \to p \in A$
17	1 6	atbase	$⊢ p \in A \to p \in B$
18	16 17	syl	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land p \underset{˙}{\leq} X)) \to p \in B$
19	1 2 4	latlej1	$⊢ (K \in Lat \land Y \in B \land p \in B) \to Y \underset{˙}{\leq} (Y \underset{˙}{\lor} p)$
20	14 15 18 19	syl3anc	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land p \underset{˙}{\leq} X)) \to Y \underset{˙}{\leq} (Y \underset{˙}{\lor} p)$
21		simpl1	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land p \underset{˙}{\leq} X)) \to (K \in HL \land W \in H)$
22	1 4	latjcl	$⊢ (K \in Lat \land Y \in B \land p \in B) \to Y \underset{˙}{\lor} p \in B$
23	14 15 18 22	syl3anc	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land p \underset{˙}{\leq} X)) \to Y \underset{˙}{\lor} p \in B$
24	1 2 3 9	dihord	$⊢ ((K \in HL \land W \in H) \land Y \in B \land Y \underset{˙}{\lor} p \in B) \to (I (Y) \subseteq I (Y \underset{˙}{\lor} p) \leftrightarrow Y \underset{˙}{\leq} (Y \underset{˙}{\lor} p))$
25	21 15 23 24	syl3anc	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land p \underset{˙}{\leq} X)) \to (I (Y) \subseteq I (Y \underset{˙}{\lor} p) \leftrightarrow Y \underset{˙}{\leq} (Y \underset{˙}{\lor} p))$
26	20 25	mpbird	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land p \underset{˙}{\leq} X)) \to I (Y) \subseteq I (Y \underset{˙}{\lor} p)$
27		sseqin2	$⊢ I (Y) \subseteq I (Y \underset{˙}{\lor} p) \leftrightarrow I (Y \underset{˙}{\lor} p) \cap I (Y) = I (Y)$
28	26 27	sylib	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land p \underset{˙}{\leq} X)) \to I (Y \underset{˙}{\lor} p) \cap I (Y) = I (Y)$
29	28	ineq2d	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land p \underset{˙}{\leq} X)) \to I (X) \cap (I (Y \underset{˙}{\lor} p) \cap I (Y)) = I (X) \cap I (Y)$
30	12 29	syl5eq	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land p \underset{˙}{\leq} X)) \to (I (X) \cap I (Y \underset{˙}{\lor} p)) \cap I (Y) = I (X) \cap I (Y)$
31	11 30	eqtrd	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land p \underset{˙}{\leq} X)) \to I ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) \cap I (Y) = I (X) \cap I (Y)$

Metamath Proof Explorer

Theorem dihmeetlem11N

Proof