dihmeetlem17N

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

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

Proof

Step	Hyp	Ref	Expression
1		dihmeetlem14.b	$⊢ B = {Base}_{K}$
2		dihmeetlem14.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihmeetlem14.h	$⊢ H = LHyp (K)$
4		dihmeetlem14.j	$⊢ \underset{˙}{\lor} = join (K)$
5		dihmeetlem14.m	$⊢ \underset{˙}{\land} = meet (K)$
6		dihmeetlem14.a	$⊢ A = Atoms (K)$
7		dihmeetlem14.u	$⊢ U = DVecH (K) (W)$
8		dihmeetlem14.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
9		dihmeetlem14.i	$⊢ I = DIsoH (K) (W)$
10		dihmeetlem17.o	$⊢ \underset{˙}{0} = 0. (K)$
11		simpl1l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land p \underset{˙}{\leq} X)) \to K \in HL$
12	11	hllatd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land p \underset{˙}{\leq} X)) \to K \in Lat$
13		simpl3l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land p \underset{˙}{\leq} X)) \to p \in A$
14	1 6	atbase	$⊢ p \in A \to p \in B$
15	13 14	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land p \underset{˙}{\leq} X)) \to p \in B$
16		simpr1	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land p \underset{˙}{\leq} X)) \to Y \in B$
17	1 5	latmcom	$⊢ (K \in Lat \land p \in B \land Y \in B) \to p \underset{˙}{\land} Y = Y \underset{˙}{\land} p$
18	12 15 16 17	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land p \underset{˙}{\leq} X)) \to p \underset{˙}{\land} Y = Y \underset{˙}{\land} p$
19		simpl1	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land p \underset{˙}{\leq} X)) \to (K \in HL \land W \in H)$
20		simpl2	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land p \underset{˙}{\leq} X)) \to (X \in B \land \neg X \underset{˙}{\leq} W)$
21		simpl3	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land p \underset{˙}{\leq} X)) \to (p \in A \land \neg p \underset{˙}{\leq} W)$
22		simpr2	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land p \underset{˙}{\leq} X)) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} W$
23		simpr3	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land p \underset{˙}{\leq} X)) \to p \underset{˙}{\leq} X$
24	1 2 4 5 6 3	lhpmcvr4N	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land p \underset{˙}{\leq} X)) \to \neg p \underset{˙}{\leq} Y$
25	19 20 21 16 22 23 24	syl123anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land p \underset{˙}{\leq} X)) \to \neg p \underset{˙}{\leq} Y$
26		hlatl	$⊢ K \in HL \to K \in AtLat$
27	11 26	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land p \underset{˙}{\leq} X)) \to K \in AtLat$
28	1 2 5 10 6	atnle	$⊢ (K \in AtLat \land p \in A \land Y \in B) \to (\neg p \underset{˙}{\leq} Y \leftrightarrow p \underset{˙}{\land} Y = \underset{˙}{0})$
29	27 13 16 28	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land p \underset{˙}{\leq} X)) \to (\neg p \underset{˙}{\leq} Y \leftrightarrow p \underset{˙}{\land} Y = \underset{˙}{0})$
30	25 29	mpbid	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land p \underset{˙}{\leq} X)) \to p \underset{˙}{\land} Y = \underset{˙}{0}$
31	18 30	eqtr3d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land p \underset{˙}{\leq} X)) \to Y \underset{˙}{\land} p = \underset{˙}{0}$

Metamath Proof Explorer

Theorem dihmeetlem17N

Proof