cdleme22f

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 6th and 7th lines on p. 115. F , N represent f(t), f_t(s) respectively. If s <_ t \/ v, then f_t(s) <_ f(t) \/ v. (Contributed by NM, 6-Dec-2012)

	Ref	Expression
Hypotheses	cdleme22.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme22.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme22.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme22.a	$⊢ A = Atoms (K)$
	cdleme22.h	$⊢ H = LHyp (K)$
	cdleme22f.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme22f.f	$⊢ F = (T \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))$
	cdleme22f.n	$⊢ N = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((S \underset{˙}{\lor} T) \underset{˙}{\land} W))$
Assertion	cdleme22f	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to N \underset{˙}{\leq} (F \underset{˙}{\lor} V)$

Proof

Step	Hyp	Ref	Expression
1		cdleme22.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme22.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme22.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme22.a	$⊢ A = Atoms (K)$
5		cdleme22.h	$⊢ H = LHyp (K)$
6		cdleme22f.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme22f.f	$⊢ F = (T \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))$
8		cdleme22f.n	$⊢ N = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((S \underset{˙}{\lor} T) \underset{˙}{\land} W))$
9		simp11l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \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 \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to K \in Lat$
11		simp12l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to P \in A$
12		simp13l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to Q \in A$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14	13 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
15	9 11 12 14	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
16		simp11r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to W \in H$
17		simp22	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to T \in A$
18	1 2 3 4 5 6 7 13	cdleme1b	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land T \in A)) \to F \in {Base}_{K}$
19	9 16 11 12 17 18	syl23anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to F \in {Base}_{K}$
20		simp21l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to S \in A$
21	13 2 4	hlatjcl	$⊢ (K \in HL \land S \in A \land T \in A) \to S \underset{˙}{\lor} T \in {Base}_{K}$
22	9 20 17 21	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to S \underset{˙}{\lor} T \in {Base}_{K}$
23	13 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
24	16 23	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to W \in {Base}_{K}$
25	13 3	latmcl	$⊢ (K \in Lat \land S \underset{˙}{\lor} T \in {Base}_{K} \land W \in {Base}_{K}) \to (S \underset{˙}{\lor} T) \underset{˙}{\land} W \in {Base}_{K}$
26	10 22 24 25	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to (S \underset{˙}{\lor} T) \underset{˙}{\land} W \in {Base}_{K}$
27	13 2	latjcl	$⊢ (K \in Lat \land F \in {Base}_{K} \land (S \underset{˙}{\lor} T) \underset{˙}{\land} W \in {Base}_{K}) \to F \underset{˙}{\lor} ((S \underset{˙}{\lor} T) \underset{˙}{\land} W) \in {Base}_{K}$
28	10 19 26 27	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to F \underset{˙}{\lor} ((S \underset{˙}{\lor} T) \underset{˙}{\land} W) \in {Base}_{K}$
29	13 1 3	latmle2	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land F \underset{˙}{\lor} ((S \underset{˙}{\lor} T) \underset{˙}{\land} W) \in {Base}_{K}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((S \underset{˙}{\lor} T) \underset{˙}{\land} W))) \underset{˙}{\leq} (F \underset{˙}{\lor} ((S \underset{˙}{\lor} T) \underset{˙}{\land} W))$
30	10 15 28 29	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((S \underset{˙}{\lor} T) \underset{˙}{\land} W))) \underset{˙}{\leq} (F \underset{˙}{\lor} ((S \underset{˙}{\lor} T) \underset{˙}{\land} W))$
31		simp21	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to (S \in A \land \neg S \underset{˙}{\leq} W)$
32		simp3l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to S \neq T$
33		simp23l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to V \in A$
34		simp23r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to V \underset{˙}{\leq} W$
35		simp3r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to S \underset{˙}{\leq} (T \underset{˙}{\lor} V)$
36	2 4	hlatjcom	$⊢ (K \in HL \land T \in A \land V \in A) \to T \underset{˙}{\lor} V = V \underset{˙}{\lor} T$
37	9 17 33 36	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to T \underset{˙}{\lor} V = V \underset{˙}{\lor} T$
38	35 37	breqtrd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to S \underset{˙}{\leq} (V \underset{˙}{\lor} T)$
39		hlcvl	$⊢ K \in HL \to K \in CvLat$
40	9 39	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to K \in CvLat$
41	1 2 4	cvlatexch2	$⊢ (K \in CvLat \land (S \in A \land V \in A \land T \in A) \land S \neq T) \to (S \underset{˙}{\leq} (V \underset{˙}{\lor} T) \to V \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
42	40 20 33 17 32 41	syl131anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to (S \underset{˙}{\leq} (V \underset{˙}{\lor} T) \to V \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
43	38 42	mpd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to V \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
44		eqid	$⊢ (S \underset{˙}{\lor} T) \underset{˙}{\land} W = (S \underset{˙}{\lor} T) \underset{˙}{\land} W$
45	1 2 3 4 5 44	cdleme22aa	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land S \neq T) \land (V \in A \land V \underset{˙}{\leq} W \land V \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to V = (S \underset{˙}{\lor} T) \underset{˙}{\land} W$
46	9 16 31 17 32 33 34 43 45	syl233anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to V = (S \underset{˙}{\lor} T) \underset{˙}{\land} W$
47	46	oveq2d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to F \underset{˙}{\lor} V = F \underset{˙}{\lor} ((S \underset{˙}{\lor} T) \underset{˙}{\land} W)$
48	30 47	breqtrrd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((S \underset{˙}{\lor} T) \underset{˙}{\land} W))) \underset{˙}{\leq} (F \underset{˙}{\lor} V)$
49	8 48	eqbrtrid	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to N \underset{˙}{\leq} (F \underset{˙}{\lor} V)$

Metamath Proof Explorer

Theorem cdleme22f

Proof