cdlemg27a

Description: For use with case when ( P .\/ v ) ./\ ( Q .\/ ( RF ) ) or ( P .\/ v ) ./\ ( Q .\/ ( RF ) ) is zero, letting us establish -. z .<_ W /\ z .<_ ( P .\/ v ) via 4atex . TODO: Fix comment. (Contributed by NM, 28-May-2013)

	Ref	Expression
Hypotheses	cdlemg12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg12.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemg12.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemg12.a	$⊢ A = Atoms (K)$
	cdlemg12.h	$⊢ H = LHyp (K)$
	cdlemg12.t	$⊢ T = LTrn (K) (W)$
	cdlemg12b.r	$⊢ R = trL (K) (W)$
Assertion	cdlemg27a	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} z)$

Proof

Step	Hyp	Ref	Expression
1		cdlemg12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg12.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemg12.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemg12.a	$⊢ A = Atoms (K)$
5		cdlemg12.h	$⊢ H = LHyp (K)$
6		cdlemg12.t	$⊢ T = LTrn (K) (W)$
7		cdlemg12b.r	$⊢ R = trL (K) (W)$
8		simp11	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to (K \in HL \land W \in H)$
9		simp12	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
10		simp31	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to v \neq R (F)$
11		simp13	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to (v \in A \land v \underset{˙}{\leq} W)$
12		simp2r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to F \in T$
13		simp33	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to F (P) \neq P$
14	1 4 5 6 7	trlat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) \neq P)) \to R (F) \in A$
15	8 9 12 13 14	syl112anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to R (F) \in A$
16	1 5 6 7	trlle	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \underset{˙}{\leq} W$
17	8 12 16	syl2anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to R (F) \underset{˙}{\leq} W$
18	1 2 4 5	lhp2atnle	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land v \neq R (F)) \land (v \in A \land v \underset{˙}{\leq} W) \land (R (F) \in A \land R (F) \underset{˙}{\leq} W)) \to \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} v)$
19	8 9 10 11 15 17 18	syl312anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} v)$
20		simp11l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to K \in HL$
21		simp12l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to P \in A$
22		simp13l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to v \in A$
23	1 2 4	hlatlej1	$⊢ (K \in HL \land P \in A \land v \in A) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} v)$
24	20 21 22 23	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} v)$
25		simp32	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to z \underset{˙}{\leq} (P \underset{˙}{\lor} v)$
26	20	hllatd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to K \in Lat$
27		eqid	$⊢ {Base}_{K} = {Base}_{K}$
28	27 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
29	21 28	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to P \in {Base}_{K}$
30		simp2l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to z \in A$
31	27 4	atbase	$⊢ z \in A \to z \in {Base}_{K}$
32	30 31	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to z \in {Base}_{K}$
33	27 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land v \in A) \to P \underset{˙}{\lor} v \in {Base}_{K}$
34	20 21 22 33	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to P \underset{˙}{\lor} v \in {Base}_{K}$
35	27 1 2	latjle12	$⊢ (K \in Lat \land (P \in {Base}_{K} \land z \in {Base}_{K} \land P \underset{˙}{\lor} v \in {Base}_{K})) \to ((P \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v)) \leftrightarrow (P \underset{˙}{\lor} z) \underset{˙}{\leq} (P \underset{˙}{\lor} v))$
36	26 29 32 34 35	syl13anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to ((P \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v)) \leftrightarrow (P \underset{˙}{\lor} z) \underset{˙}{\leq} (P \underset{˙}{\lor} v))$
37	24 25 36	mpbi2and	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to (P \underset{˙}{\lor} z) \underset{˙}{\leq} (P \underset{˙}{\lor} v)$
38	27 4	atbase	$⊢ R (F) \in A \to R (F) \in {Base}_{K}$
39	15 38	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to R (F) \in {Base}_{K}$
40	27 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land z \in A) \to P \underset{˙}{\lor} z \in {Base}_{K}$
41	20 21 30 40	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to P \underset{˙}{\lor} z \in {Base}_{K}$
42	27 1	lattr	$⊢ (K \in Lat \land (R (F) \in {Base}_{K} \land P \underset{˙}{\lor} z \in {Base}_{K} \land P \underset{˙}{\lor} v \in {Base}_{K})) \to ((R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} z) \land (P \underset{˙}{\lor} z) \underset{˙}{\leq} (P \underset{˙}{\lor} v)) \to R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} v))$
43	26 39 41 34 42	syl13anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to ((R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} z) \land (P \underset{˙}{\lor} z) \underset{˙}{\leq} (P \underset{˙}{\lor} v)) \to R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} v))$
44	37 43	mpan2d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} z) \to R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} v))$
45	19 44	mtod	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (v \in A \land v \underset{˙}{\leq} W)) \land (z \in A \land F \in T) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} z)$

Metamath Proof Explorer

Theorem cdlemg27a

Proof