cdleme13

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph on p. 114, " and are centrally perspective." F and G represent f(s) and f(t) respectively. (Contributed by NM, 7-Oct-2012)

	Ref	Expression
Hypotheses	cdleme12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme12.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme12.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme12.a	$⊢ A = Atoms (K)$
	cdleme12.h	$⊢ H = LHyp (K)$
	cdleme12.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme12.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme12.g	$⊢ G = (T \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))$
Assertion	cdleme13	$⊢ ((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) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to ((S \underset{˙}{\lor} F) \underset{˙}{\land} (T \underset{˙}{\lor} G)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$

Proof

Step	Hyp	Ref	Expression
1		cdleme12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme12.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme12.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme12.a	$⊢ A = Atoms (K)$
5		cdleme12.h	$⊢ H = LHyp (K)$
6		cdleme12.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme12.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
8		cdleme12.g	$⊢ G = (T \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))$
9	1 2 3 4 5 6 7 8	cdleme12	$⊢ ((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) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to (S \underset{˙}{\lor} F) \underset{˙}{\land} (T \underset{˙}{\lor} G) = U$
10	9 6	syl6eq	$⊢ ((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) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to (S \underset{˙}{\lor} F) \underset{˙}{\land} (T \underset{˙}{\lor} G) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
11		simp1l	$⊢ ((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) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to K \in HL$
12	11	hllatd	$⊢ ((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) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to K \in Lat$
13		simp21l	$⊢ ((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) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to P \in A$
14		simp22	$⊢ ((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) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to Q \in A$
15		eqid	$⊢ {Base}_{K} = {Base}_{K}$
16	15 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
17	11 13 14 16	syl3anc	$⊢ ((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) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
18		simp1r	$⊢ ((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) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to W \in H$
19	15 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
20	18 19	syl	$⊢ ((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) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to W \in {Base}_{K}$
21	15 1 3	latmle1	$⊢ (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} (P \underset{˙}{\lor} Q)$
22	12 17 20 21	syl3anc	$⊢ ((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) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
23	10 22	eqbrtrd	$⊢ ((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) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to ((S \underset{˙}{\lor} F) \underset{˙}{\land} (T \underset{˙}{\lor} G)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$

Metamath Proof Explorer

Theorem cdleme13

Proof