dihmeetlem15N

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)$
	dihmeetlem15.z	$⊢ \underset{˙}{0} = 0_{U}$
Assertion	dihmeetlem15N	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to I (r) \cap I (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		dihmeetlem15.z	$⊢ \underset{˙}{0} = 0_{U}$
11		simpl1	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
12		simpr1	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to (r \in A \land \neg r \underset{˙}{\leq} W)$
13		simpl3	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to (p \in A \land \neg p \underset{˙}{\leq} W)$
14		simpl3r	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to \neg p \underset{˙}{\leq} W$
15		simp3	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W) \land r = p) \to r = p$
16		simp22	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W) \land r = p) \to r \underset{˙}{\leq} Y$
17	15 16	eqbrtrrd	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W) \land r = p) \to p \underset{˙}{\leq} Y$
18		simp11l	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W) \land r = p) \to K \in HL$
19	18	hllatd	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W) \land r = p) \to K \in Lat$
20		simp13l	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W) \land r = p) \to p \in A$
21	1 6	atbase	$⊢ p \in A \to p \in B$
22	20 21	syl	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W) \land r = p) \to p \in B$
23		simp12	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W) \land r = p) \to Y \in B$
24	1 2 5	latleeqm2	$⊢ (K \in Lat \land p \in B \land Y \in B) \to (p \underset{˙}{\leq} Y \leftrightarrow Y \underset{˙}{\land} p = p)$
25	19 22 23 24	syl3anc	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W) \land r = p) \to (p \underset{˙}{\leq} Y \leftrightarrow Y \underset{˙}{\land} p = p)$
26	17 25	mpbid	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W) \land r = p) \to Y \underset{˙}{\land} p = p$
27		simp23	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W) \land r = p) \to (Y \underset{˙}{\land} p) \underset{˙}{\leq} W$
28	26 27	eqbrtrrd	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W) \land r = p) \to p \underset{˙}{\leq} W$
29	28	3expia	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to (r = p \to p \underset{˙}{\leq} W)$
30	29	necon3bd	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to (\neg p \underset{˙}{\leq} W \to r \neq p)$
31	14 30	mpd	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to r \neq p$
32		eqid	$⊢ oc (K) (W) = oc (K) (W)$
33		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
34		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
35		eqid	$⊢ (h \in LTrn (K) (W) ⟼ {I ↾}_{B}) = (h \in LTrn (K) (W) ⟼ {I ↾}_{B})$
36		eqid	$⊢ (ι h \in LTrn (K) (W) \| h (oc (K) (W)) = r) = (ι h \in LTrn (K) (W) \| h (oc (K) (W)) = r)$
37		eqid	$⊢ (ι h \in LTrn (K) (W) \| h (oc (K) (W)) = p) = (ι h \in LTrn (K) (W) \| h (oc (K) (W)) = p)$
38	1 2 4 6 3 32 33 34 35 9 7 10 36 37	dihmeetlem13N	$⊢ ((K \in HL \land W \in H) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land r \neq p) \to I (r) \cap I (p) = \{\underset{˙}{0}\}$
39	11 12 13 31 38	syl121anc	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to I (r) \cap I (p) = \{\underset{˙}{0}\}$

Metamath Proof Explorer

Theorem dihmeetlem15N

Proof