cdlemf1

Description: Part of Lemma F in Crawley p. 116. TODO: should this or part of it become a stand-alone theorem? (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)$
Assertion	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))$

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		simp1l	$⊢ ((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 K \in HL$
6		simp3l	$⊢ ((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 P \in A$
7		simp2l	$⊢ ((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 U \in A$
8		simp2r	$⊢ ((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 U \underset{˙}{\leq} W$
9		simp3r	$⊢ ((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 \neg P \underset{˙}{\leq} W$
10		nbrne2	$⊢ (U \underset{˙}{\leq} W \land \neg P \underset{˙}{\leq} W) \to U \neq P$
11	10	necomd	$⊢ (U \underset{˙}{\leq} W \land \neg P \underset{˙}{\leq} W) \to P \neq U$
12	8 9 11	syl2anc	$⊢ ((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 P \neq U$
13	1 2 3	hlsupr	$⊢ ((K \in HL \land P \in A \land U \in A) \land P \neq U) \to \exists q \in A (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))$
14	5 6 7 12 13	syl31anc	$⊢ ((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))$
15		simp31	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to q \neq P$
16	15	necomd	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to P \neq q$
17		simp13r	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to \neg P \underset{˙}{\leq} W$
18		simp12r	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to U \underset{˙}{\leq} W$
19		simp11l	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to K \in HL$
20	19	hllatd	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to K \in Lat$
21		eqid	$⊢ {Base}_{K} = {Base}_{K}$
22	21 3	atbase	$⊢ q \in A \to q \in {Base}_{K}$
23	22	3ad2ant2	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to q \in {Base}_{K}$
24		simp12l	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to U \in A$
25	21 3	atbase	$⊢ U \in A \to U \in {Base}_{K}$
26	24 25	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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to U \in {Base}_{K}$
27		simp11r	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to W \in H$
28	21 4	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
29	27 28	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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to W \in {Base}_{K}$
30	21 1 2	latjle12	$⊢ (K \in Lat \land (q \in {Base}_{K} \land U \in {Base}_{K} \land W \in {Base}_{K})) \to ((q \underset{˙}{\leq} W \land U \underset{˙}{\leq} W) \leftrightarrow (q \underset{˙}{\lor} U) \underset{˙}{\leq} W)$
31	20 23 26 29 30	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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to ((q \underset{˙}{\leq} W \land U \underset{˙}{\leq} W) \leftrightarrow (q \underset{˙}{\lor} U) \underset{˙}{\leq} W)$
32	31	biimpd	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to ((q \underset{˙}{\leq} W \land U \underset{˙}{\leq} W) \to (q \underset{˙}{\lor} U) \underset{˙}{\leq} W)$
33	18 32	mpan2d	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to (q \underset{˙}{\leq} W \to (q \underset{˙}{\lor} U) \underset{˙}{\leq} W)$
34		simp33	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to q \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
35		hlcvl	$⊢ K \in HL \to K \in CvLat$
36	19 35	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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to K \in CvLat$
37		simp2	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to q \in A$
38		simp13l	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to P \in A$
39		simp32	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to q \neq U$
40	1 2 3	cvlatexch2	$⊢ (K \in CvLat \land (q \in A \land P \in A \land U \in A) \land q \neq U) \to (q \underset{˙}{\leq} (P \underset{˙}{\lor} U) \to P \underset{˙}{\leq} (q \underset{˙}{\lor} U))$
41	36 37 38 24 39 40	syl131anc	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to (q \underset{˙}{\leq} (P \underset{˙}{\lor} U) \to P \underset{˙}{\leq} (q \underset{˙}{\lor} U))$
42	34 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)) \land q \in A \land (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to P \underset{˙}{\leq} (q \underset{˙}{\lor} U)$
43	21 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
44	38 43	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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to P \in {Base}_{K}$
45	21 2 3	hlatjcl	$⊢ (K \in HL \land q \in A \land U \in A) \to q \underset{˙}{\lor} U \in {Base}_{K}$
46	19 37 24 45	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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to q \underset{˙}{\lor} U \in {Base}_{K}$
47	21 1	lattr	$⊢ (K \in Lat \land (P \in {Base}_{K} \land q \underset{˙}{\lor} U \in {Base}_{K} \land W \in {Base}_{K})) \to ((P \underset{˙}{\leq} (q \underset{˙}{\lor} U) \land (q \underset{˙}{\lor} U) \underset{˙}{\leq} W) \to P \underset{˙}{\leq} W)$
48	20 44 46 29 47	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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to ((P \underset{˙}{\leq} (q \underset{˙}{\lor} U) \land (q \underset{˙}{\lor} U) \underset{˙}{\leq} W) \to P \underset{˙}{\leq} W)$
49	42 48	mpand	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to ((q \underset{˙}{\lor} U) \underset{˙}{\leq} W \to P \underset{˙}{\leq} W)$
50	33 49	syld	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to (q \underset{˙}{\leq} W \to P \underset{˙}{\leq} W)$
51	17 50	mtod	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to \neg q \underset{˙}{\leq} W$
52	1 2 3	cvlatexch1	$⊢ (K \in CvLat \land (q \in A \land U \in A \land P \in A) \land q \neq P) \to (q \underset{˙}{\leq} (P \underset{˙}{\lor} U) \to U \underset{˙}{\leq} (P \underset{˙}{\lor} q))$
53	36 37 24 38 15 52	syl131anc	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to (q \underset{˙}{\leq} (P \underset{˙}{\lor} U) \to U \underset{˙}{\leq} (P \underset{˙}{\lor} q))$
54	34 53	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)) \land q \in A \land (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to U \underset{˙}{\leq} (P \underset{˙}{\lor} q)$
55	16 51 54	3jca	$⊢ (((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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to (P \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (P \underset{˙}{\lor} q))$
56	55	3exp	$⊢ ((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 ((q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \to (P \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (P \underset{˙}{\lor} q))))$
57	56	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 (q \neq P \land q \neq U \land q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \to \exists q \in A (P \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (P \underset{˙}{\lor} q)))$
58	14 57	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 (P \neq q \land \neg q \underset{˙}{\leq} W \land U \underset{˙}{\leq} (P \underset{˙}{\lor} q))$

Metamath Proof Explorer

Theorem cdlemf1

Proof