dihmeetlem3N

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

	Ref	Expression
Hypotheses	dihmeetlem3.b	$⊢ B = {Base}_{K}$
	dihmeetlem3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihmeetlem3.j	$⊢ \underset{˙}{\lor} = join (K)$
	dihmeetlem3.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihmeetlem3.a	$⊢ A = Atoms (K)$
	dihmeetlem3.h	$⊢ H = LHyp (K)$
Assertion	dihmeetlem3N	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land ((R \in A \land \neg R \underset{˙}{\leq} W) \land R \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to Q \neq R$

Proof

Step	Hyp	Ref	Expression
1		dihmeetlem3.b	$⊢ B = {Base}_{K}$
2		dihmeetlem3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihmeetlem3.j	$⊢ \underset{˙}{\lor} = join (K)$
4		dihmeetlem3.m	$⊢ \underset{˙}{\land} = meet (K)$
5		dihmeetlem3.a	$⊢ A = Atoms (K)$
6		dihmeetlem3.h	$⊢ H = LHyp (K)$
7		simp2lr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land ((R \in A \land \neg R \underset{˙}{\leq} W) \land R \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to \neg Q \underset{˙}{\leq} W$
8		oveq1	$⊢ Q = R \to Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = R \underset{˙}{\lor} (Y \underset{˙}{\land} W)$
9		simpr	$⊢ ((R \in A \land \neg R \underset{˙}{\leq} W) \land R \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to R \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y$
10	8 9	sylan9eqr	$⊢ (((R \in A \land \neg R \underset{˙}{\leq} W) \land R \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \land Q = R) \to Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y$
11		simp11l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to K \in HL$
12	11	hllatd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to K \in Lat$
13		simp2ll	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to Q \in A$
14	1 5	atbase	$⊢ Q \in A \to Q \in B$
15	13 14	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to Q \in B$
16		simp12l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to X \in B$
17		simp12r	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to Y \in B$
18	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
19	12 16 17 18	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to X \underset{˙}{\land} Y \in B$
20		simp11r	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to W \in H$
21	1 6	lhpbase	$⊢ W \in H \to W \in B$
22	20 21	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to W \in B$
23	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land W \in B) \to X \underset{˙}{\land} W \in B$
24	12 16 22 23	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to X \underset{˙}{\land} W \in B$
25	1 2 3	latlej1	$⊢ (K \in Lat \land Q \in B \land X \underset{˙}{\land} W \in B) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} (X \underset{˙}{\land} W))$
26	12 15 24 25	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} (X \underset{˙}{\land} W))$
27		simp2r	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X$
28	26 27	breqtrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to Q \underset{˙}{\leq} X$
29	1 4	latmcl	$⊢ (K \in Lat \land Y \in B \land W \in B) \to Y \underset{˙}{\land} W \in B$
30	12 17 22 29	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to Y \underset{˙}{\land} W \in B$
31	1 2 3	latlej1	$⊢ (K \in Lat \land Q \in B \land Y \underset{˙}{\land} W \in B) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} (Y \underset{˙}{\land} W))$
32	12 15 30 31	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} (Y \underset{˙}{\land} W))$
33		simp3	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y$
34	32 33	breqtrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to Q \underset{˙}{\leq} Y$
35	1 2 4	latlem12	$⊢ (K \in Lat \land (Q \in B \land X \in B \land Y \in B)) \to ((Q \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \leftrightarrow Q \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
36	12 15 16 17 35	syl13anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to ((Q \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \leftrightarrow Q \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
37	28 34 36	mpbi2and	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to Q \underset{˙}{\leq} (X \underset{˙}{\land} Y)$
38		simp13	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} W$
39	1 2 12 15 19 22 37 38	lattrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to Q \underset{˙}{\leq} W$
40	39	3exp	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to (((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to (Q \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y \to Q \underset{˙}{\leq} W))$
41	10 40	syl7	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to (((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to ((((R \in A \land \neg R \underset{˙}{\leq} W) \land R \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \land Q = R) \to Q \underset{˙}{\leq} W))$
42	41	exp4a	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to (((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to (((R \in A \land \neg R \underset{˙}{\leq} W) \land R \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to (Q = R \to Q \underset{˙}{\leq} W)))$
43	42	3imp	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land ((R \in A \land \neg R \underset{˙}{\leq} W) \land R \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to (Q = R \to Q \underset{˙}{\leq} W)$
44	43	necon3bd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land ((R \in A \land \neg R \underset{˙}{\leq} W) \land R \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to (\neg Q \underset{˙}{\leq} W \to Q \neq R)$
45	7 44	mpd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land ((R \in A \land \neg R \underset{˙}{\leq} W) \land R \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to Q \neq R$

Metamath Proof Explorer

Theorem dihmeetlem3N

Proof