dihmeetlem20N

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)$
Assertion	dihmeetlem20N	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$

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		simp1	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
11		simp2	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to (X \in B \land \neg X \underset{˙}{\leq} W)$
12		simp3ll	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to Y \in B$
13		simp3r	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} W$
14	1 2 4 5 6 3	lhpmcvr6N	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to \exists q \in A (\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X)$
15	10 11 12 13 14	syl112anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to \exists q \in A (\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X)$
16		simp3l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to (Y \in B \land \neg Y \underset{˙}{\leq} W)$
17		simp2l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to X \in B$
18		simp1l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to K \in HL$
19	18	hllatd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to K \in Lat$
20	1 5	latmcom	$⊢ (K \in Lat \land Y \in B \land X \in B) \to Y \underset{˙}{\land} X = X \underset{˙}{\land} Y$
21	19 12 17 20	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to Y \underset{˙}{\land} X = X \underset{˙}{\land} Y$
22	21 13	eqbrtrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to (Y \underset{˙}{\land} X) \underset{˙}{\leq} W$
23	1 2 4 5 6 3	lhpmcvr6N	$⊢ ((K \in HL \land W \in H) \land (Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \in B \land (Y \underset{˙}{\land} X) \underset{˙}{\leq} W)) \to \exists r \in A (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y)$
24	10 16 17 22 23	syl112anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to \exists r \in A (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y)$
25		reeanv	$⊢ \exists q \in A \exists r \in A ((\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X) \land (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y)) \leftrightarrow (\exists q \in A (\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y))$
26		simp11	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X) \land (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y))) \to (K \in HL \land W \in H)$
27		simp12	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X) \land (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y))) \to (X \in B \land \neg X \underset{˙}{\leq} W)$
28	12	3ad2ant1	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X) \land (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y))) \to Y \in B$
29		simp2l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X) \land (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y))) \to q \in A$
30		simp3l1	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X) \land (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y))) \to \neg q \underset{˙}{\leq} W$
31	29 30	jca	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X) \land (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y))) \to (q \in A \land \neg q \underset{˙}{\leq} W)$
32		simp2r	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X) \land (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y))) \to r \in A$
33		simp3r1	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X) \land (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y))) \to \neg r \underset{˙}{\leq} W$
34	32 33	jca	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X) \land (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y))) \to (r \in A \land \neg r \underset{˙}{\leq} W)$
35		simp3l3	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X) \land (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y))) \to q \underset{˙}{\leq} X$
36		simp3r3	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X) \land (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y))) \to r \underset{˙}{\leq} Y$
37		simp13r	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X) \land (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y))) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} W$
38	35 36 37	3jca	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X) \land (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y))) \to (q \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)$
39	1 2 3 4 5 6 7 8 9	dihmeetlem19N	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land (r \in A \land \neg r \underset{˙}{\leq} W) \land (q \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$
40	26 27 28 31 34 38 39	syl33anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X) \land (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y))) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$
41	40	3exp	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to ((q \in A \land r \in A) \to (((\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X) \land (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y)) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)))$
42	41	rexlimdvv	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to (\exists q \in A \exists r \in A ((\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X) \land (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y)) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y))$
43	25 42	syl5bir	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to ((\exists q \in A (\neg q \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} Y \land q \underset{˙}{\leq} X) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y)) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y))$
44	15 24 43	mp2and	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Y \in B \land \neg Y \underset{˙}{\leq} W) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$

Metamath Proof Explorer

Theorem dihmeetlem20N

Proof