cdlemf2

Description: Part of Lemma F in Crawley p. 116. (Contributed by NM, 12-Apr-2013)

	Ref	Expression
Hypotheses	cdlemf1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemf1.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemf1.a	$⊢ A = Atoms (K)$
	cdlemf1.h	$⊢ H = LHyp (K)$
	cdlemf2.m	$⊢ \underset{˙}{\land} = meet (K)$
Assertion	cdlemf2	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \to \exists p \in A \exists q \in A ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p \underset{˙}{\lor} q) \underset{˙}{\land} W)$

Proof

Step	Hyp	Ref	Expression
1		cdlemf1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemf1.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemf1.a	$⊢ A = Atoms (K)$
4		cdlemf1.h	$⊢ H = LHyp (K)$
5		cdlemf2.m	$⊢ \underset{˙}{\land} = meet (K)$
6	1 3 4	lhpexnle	$⊢ (K \in HL \land W \in H) \to \exists p \in A \neg p \underset{˙}{\leq} W$
7	6	adantr	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \to \exists p \in A \neg p \underset{˙}{\leq} W$
8	1 2 3 4	cdlemf1	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \to \exists q \in A (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q))$
9		simpr1r	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to \neg p \underset{˙}{\leq} W$
10		simpr32	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to \neg q \underset{˙}{\leq} W$
11		simpr33	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to U \underset{˙}{\leq} (p \underset{˙}{\lor} q)$
12		simplrr	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to U \underset{˙}{\leq} W$
13		hllat	$⊢ K \in HL \to K \in Lat$
14	13	ad3antrrr	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to K \in Lat$
15		simplrl	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to U \in A$
16		eqid	$⊢ {Base}_{K} = {Base}_{K}$
17	16 3	atbase	$⊢ U \in A \to U \in {Base}_{K}$
18	15 17	syl	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to U \in {Base}_{K}$
19		simplll	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to K \in HL$
20		simpr1l	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to p \in A$
21		simpr2	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to q \in A$
22	16 2 3	hlatjcl	$⊢ (K \in HL \land p \in A \land q \in A) \to p \underset{˙}{\lor} q \in {Base}_{K}$
23	19 20 21 22	syl3anc	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to p \underset{˙}{\lor} q \in {Base}_{K}$
24	16 4	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
25	24	ad3antlr	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to W \in {Base}_{K}$
26	16 1 5	latlem12	$⊢ (K \in Lat \land (U \in {Base}_{K} \land p \underset{˙}{\lor} q \in {Base}_{K} \land W \in {Base}_{K})) \to ((U \underset{˙}{\leq} (p \underset{˙}{\lor} q) \land U \underset{˙}{\leq} W) \leftrightarrow U \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\land} W))$
27	14 18 23 25 26	syl13anc	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to ((U \underset{˙}{\leq} (p \underset{˙}{\lor} q) \land U \underset{˙}{\leq} W) \leftrightarrow U \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\land} W))$
28	11 12 27	mpbi2and	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to U \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\land} W)$
29		hlatl	$⊢ K \in HL \to K \in AtLat$
30	29	ad3antrrr	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to K \in AtLat$
31		simpll	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to (K \in HL \land W \in H)$
32		simpr31	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to p \neq q$
33	1 2 5 3 4	lhpat	$⊢ ((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 (p \underset{˙}{\lor} q) \underset{˙}{\land} W \in A$
34	31 20 9 21 32 33	syl122anc	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to (p \underset{˙}{\lor} q) \underset{˙}{\land} W \in A$
35	1 3	atcmp	$⊢ (K \in AtLat \land U \in A \land (p \underset{˙}{\lor} q) \underset{˙}{\land} W \in A) \to (U \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\land} W) \leftrightarrow U = (p \underset{˙}{\lor} q) \underset{˙}{\land} W)$
36	30 15 34 35	syl3anc	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to (U \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\land} W) \leftrightarrow U = (p \underset{˙}{\lor} q) \underset{˙}{\land} W)$
37	28 36	mpbid	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to U = (p \underset{˙}{\lor} q) \underset{˙}{\land} W$
38	9 10 37	jca31	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land q \in A \land (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)))) \to ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p \underset{˙}{\lor} q) \underset{˙}{\land} W)$
39	38	3exp2	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \to ((p \in A \land \neg p \underset{˙}{\leq} W) \to (q \in A \to ((p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)) \to ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p \underset{˙}{\lor} q) \underset{˙}{\land} W))))$
40	39	3impia	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \to (q \in A \to ((p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)) \to ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p \underset{˙}{\lor} q) \underset{˙}{\land} W)))$
41	40	reximdvai	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \to (\exists q \in A (p \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (p \underset{˙}{\lor} q)) \to \exists q \in A ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p \underset{˙}{\lor} q) \underset{˙}{\land} W))$
42	8 41	mpd	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \to \exists q \in A ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p \underset{˙}{\lor} q) \underset{˙}{\land} W)$
43	42	3expia	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \to ((p \in A \land \neg p \underset{˙}{\leq} W) \to \exists q \in A ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p \underset{˙}{\lor} q) \underset{˙}{\land} W))$
44	43	expd	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \to (p \in A \to (\neg p \underset{˙}{\leq} W \to \exists q \in A ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p \underset{˙}{\lor} q) \underset{˙}{\land} W)))$
45	44	reximdvai	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \to (\exists p \in A \neg p \underset{˙}{\leq} W \to \exists p \in A \exists q \in A ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p \underset{˙}{\lor} q) \underset{˙}{\land} W))$
46	7 45	mpd	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \to \exists p \in A \exists q \in A ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p \underset{˙}{\lor} q) \underset{˙}{\land} W)$

Metamath Proof Explorer

Theorem cdlemf2

Proof