cdleme4

Description: Part of proof of Lemma E in Crawley p. 113. F and G represent f(s) and f_s(r). Here show p \/ q = r \/ u at the top of p. 114. (Contributed by NM, 7-Jun-2012)

	Ref	Expression
Hypotheses	cdleme4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme4.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme4.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme4.a	$⊢ A = Atoms (K)$
	cdleme4.h	$⊢ H = LHyp (K)$
	cdleme4.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
Assertion	cdleme4	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} Q = R \underset{˙}{\lor} U$

Proof

Step	Hyp	Ref	Expression
1		cdleme4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme4.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme4.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme4.a	$⊢ A = Atoms (K)$
5		cdleme4.h	$⊢ H = LHyp (K)$
6		cdleme4.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7	6	oveq2i	$⊢ R \underset{˙}{\lor} U = R \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
8		simp1l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to K \in HL$
9		simp23l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \in A$
10		simp21	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \in A$
11		simp22	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Q \in A$
12		eqid	$⊢ {Base}_{K} = {Base}_{K}$
13	12 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
14	8 10 11 13	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
15		simp1r	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to W \in H$
16	12 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
17	15 16	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to W \in {Base}_{K}$
18		simp3	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
19	12 1 2 3 4	atmod3i1	$⊢ (K \in HL \land (R \in A \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K}) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} W)$
20	8 9 14 17 18 19	syl131anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} W)$
21		simp1	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (K \in HL \land W \in H)$
22		simp23	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
23		eqid	$⊢ 1. (K) = 1. (K)$
24	1 2 23 4 5	lhpjat2	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to R \underset{˙}{\lor} W = 1. (K)$
25	21 22 24	syl2anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \underset{˙}{\lor} W = 1. (K)$
26	25	oveq2d	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} W) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} 1. (K)$
27		hlol	$⊢ K \in HL \to K \in OL$
28	8 27	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to K \in OL$
29	12 3 23	olm11	$⊢ (K \in OL \land P \underset{˙}{\lor} Q \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} 1. (K) = P \underset{˙}{\lor} Q$
30	28 14 29	syl2anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} 1. (K) = P \underset{˙}{\lor} Q$
31	20 26 30	3eqtrd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = P \underset{˙}{\lor} Q$
32	7 31	syl5req	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} Q = R \underset{˙}{\lor} U$

Metamath Proof Explorer

Theorem cdleme4

Proof