lhpat3

Description: There is only one atom under both P .\/ Q and co-atom W . (Contributed by NM, 21-Nov-2012)

	Ref	Expression
Hypotheses	lhpat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lhpat.j	$⊢ \underset{˙}{\lor} = join (K)$
	lhpat.m	$⊢ \underset{˙}{\land} = meet (K)$
	lhpat.a	$⊢ A = Atoms (K)$
	lhpat.h	$⊢ H = LHyp (K)$
	lhpat2.r	$⊢ R = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
Assertion	lhpat3	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (\neg S \underset{˙}{\leq} W \leftrightarrow S \neq R)$

Proof

Step	Hyp	Ref	Expression
1		lhpat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lhpat.j	$⊢ \underset{˙}{\lor} = join (K)$
3		lhpat.m	$⊢ \underset{˙}{\land} = meet (K)$
4		lhpat.a	$⊢ A = Atoms (K)$
5		lhpat.h	$⊢ H = LHyp (K)$
6		lhpat2.r	$⊢ R = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		simpl3r	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land S \underset{˙}{\leq} W) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
8		simpr	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land S \underset{˙}{\leq} W) \to S \underset{˙}{\leq} W$
9		simp1ll	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in HL$
10	9	hllatd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in Lat$
11		simp2r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \in A$
12		eqid	$⊢ {Base}_{K} = {Base}_{K}$
13	12 4	atbase	$⊢ S \in A \to S \in {Base}_{K}$
14	11 13	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \in {Base}_{K}$
15		simp1rl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \in A$
16		simp2l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \in A$
17	12 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
18	9 15 16 17	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
19		simp1lr	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to W \in H$
20	12 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
21	19 20	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to W \in {Base}_{K}$
22	12 1 3	latlem12	$⊢ (K \in Lat \land (S \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K})) \to ((S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} W) \leftrightarrow S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
23	10 14 18 21 22	syl13anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to ((S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} W) \leftrightarrow S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
24	23	adantr	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land S \underset{˙}{\leq} W) \to ((S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} W) \leftrightarrow S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
25	7 8 24	mpbi2and	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land S \underset{˙}{\leq} W) \to S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
26	25 6	breqtrrdi	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land S \underset{˙}{\leq} W) \to S \underset{˙}{\leq} R$
27	9	adantr	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land S \underset{˙}{\leq} W) \to K \in HL$
28		hlatl	$⊢ K \in HL \to K \in AtLat$
29	27 28	syl	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land S \underset{˙}{\leq} W) \to K \in AtLat$
30		simpl2r	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land S \underset{˙}{\leq} W) \to S \in A$
31		simpl1l	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land S \underset{˙}{\leq} W) \to (K \in HL \land W \in H)$
32		simpl1r	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land S \underset{˙}{\leq} W) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
33		simpl2l	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land S \underset{˙}{\leq} W) \to Q \in A$
34		simpl3l	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land S \underset{˙}{\leq} W) \to P \neq Q$
35	1 2 3 4 5 6	lhpat2	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land P \neq Q)) \to R \in A$
36	31 32 33 34 35	syl112anc	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land S \underset{˙}{\leq} W) \to R \in A$
37	1 4	atcmp	$⊢ (K \in AtLat \land S \in A \land R \in A) \to (S \underset{˙}{\leq} R \leftrightarrow S = R)$
38	29 30 36 37	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land S \underset{˙}{\leq} W) \to (S \underset{˙}{\leq} R \leftrightarrow S = R)$
39	26 38	mpbid	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land S \underset{˙}{\leq} W) \to S = R$
40	39	ex	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (S \underset{˙}{\leq} W \to S = R)$
41	12 1 3	latmle2	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
42	10 18 21 41	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
43	6 42	eqbrtrid	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\leq} W$
44		breq1	$⊢ S = R \to (S \underset{˙}{\leq} W \leftrightarrow R \underset{˙}{\leq} W)$
45	43 44	syl5ibrcom	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (S = R \to S \underset{˙}{\leq} W)$
46	40 45	impbid	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (S \underset{˙}{\leq} W \leftrightarrow S = R)$
47	46	necon3bbid	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (\neg S \underset{˙}{\leq} W \leftrightarrow S \neq R)$

Metamath Proof Explorer

Theorem lhpat3

Proof