dihmeetlem18N

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)$
	dihmeetlem18.z	$⊢ \underset{˙}{0} = 0_{U}$
Assertion	dihmeetlem18N	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to I (Y) \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		dihmeetlem18.z	$⊢ \underset{˙}{0} = 0_{U}$
11		simpl1	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to (K \in HL \land W \in H)$
12		simpl2	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to (X \in B \land \neg X \underset{˙}{\leq} W)$
13		simpr1	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to (p \in A \land \neg p \underset{˙}{\leq} W)$
14		simpl3	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to Y \in B$
15		simpr33	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} W$
16		simpr31	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to p \underset{˙}{\leq} X$
17		eqid	$⊢ 0. (K) = 0. (K)$
18	1 2 3 4 5 6 7 8 9 17	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 = 0. (K)$
19	11 12 13 14 15 16 18	syl33anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to Y \underset{˙}{\land} p = 0. (K)$
20	19	fveq2d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to I (Y \underset{˙}{\land} p) = I (0. (K))$
21		simpr2	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to (r \in A \land \neg r \underset{˙}{\leq} W)$
22		simpr32	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to r \underset{˙}{\leq} Y$
23		simpl1l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to K \in HL$
24		hlop	$⊢ K \in HL \to K \in OP$
25	23 24	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to K \in OP$
26		simpl1r	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to W \in H$
27	1 3	lhpbase	$⊢ W \in H \to W \in B$
28	26 27	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to W \in B$
29	1 2 17	op0le	$⊢ (K \in OP \land W \in B) \to 0. (K) \underset{˙}{\leq} W$
30	25 28 29	syl2anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to 0. (K) \underset{˙}{\leq} W$
31	19 30	eqbrtrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to (Y \underset{˙}{\land} p) \underset{˙}{\leq} W$
32	1 2 3 4 5 6 7 8 9	dihmeetlem16N	$⊢ (((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 (Y \underset{˙}{\land} p) = I (Y) \cap I (p)$
33	11 14 13 21 22 31 32	syl33anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to I (Y \underset{˙}{\land} p) = I (Y) \cap I (p)$
34	17 3 9 7 10	dih0	$⊢ (K \in HL \land W \in H) \to I (0. (K)) = \{\underset{˙}{0}\}$
35	11 34	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to I (0. (K)) = \{\underset{˙}{0}\}$
36	20 33 35	3eqtr3d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to I (Y) \cap I (p) = \{\underset{˙}{0}\}$

Metamath Proof Explorer

Theorem dihmeetlem18N

Proof