cdleme2

Description: Part of proof of Lemma E in Crawley p. 113. F represents f(r). W is the fiducial co-atom (hyperplane) w. Here we show that (r \/ f(r)) /\ w = u in their notation (4th line from bottom on p. 113). (Contributed by NM, 5-Jun-2012)

	Ref	Expression
Hypotheses	cdleme1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme1.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme1.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme1.a	$⊢ A = Atoms (K)$
	cdleme1.h	$⊢ H = LHyp (K)$
	cdleme1.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme1.f	$⊢ F = (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))$
Assertion	cdleme2	$⊢ ((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))) \to (R \underset{˙}{\lor} F) \underset{˙}{\land} W = U$

Proof

Step	Hyp	Ref	Expression
1		cdleme1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme1.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme1.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme1.a	$⊢ A = Atoms (K)$
5		cdleme1.h	$⊢ H = LHyp (K)$
6		cdleme1.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme1.f	$⊢ F = (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))$
8	1 2 3 4 5 6 7	cdleme1	$⊢ ((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))) \to R \underset{˙}{\lor} F = R \underset{˙}{\lor} U$
9	8	oveq1d	$⊢ ((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))) \to (R \underset{˙}{\lor} F) \underset{˙}{\land} W = (R \underset{˙}{\lor} U) \underset{˙}{\land} W$
10		simpll	$⊢ ((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))) \to K \in HL$
11		simpr3l	$⊢ ((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))) \to R \in A$
12		hllat	$⊢ K \in HL \to K \in Lat$
13	12	ad2antrr	$⊢ ((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))) \to K \in Lat$
14		simpr1	$⊢ ((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))) \to P \in A$
15		eqid	$⊢ {Base}_{K} = {Base}_{K}$
16	15 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
17	14 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))) \to P \in {Base}_{K}$
18		simpr2	$⊢ ((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))) \to Q \in A$
19	15 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
20	18 19	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))) \to Q \in {Base}_{K}$
21	15 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land Q \in {Base}_{K}) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
22	13 17 20 21	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))) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
23	15 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
24	23	ad2antlr	$⊢ ((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))) \to W \in {Base}_{K}$
25	15 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K}$
26	13 22 24 25	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))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K}$
27	6 26	eqeltrid	$⊢ ((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))) \to U \in {Base}_{K}$
28	15 1 3	latmle2	$⊢ (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} W$
29	13 22 24 28	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))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
30	6 29	eqbrtrid	$⊢ ((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))) \to U \underset{˙}{\leq} W$
31	15 1 2 3 4	atmod4i2	$⊢ (K \in HL \land (R \in A \land U \in {Base}_{K} \land W \in {Base}_{K}) \land U \underset{˙}{\leq} W) \to (R \underset{˙}{\land} W) \underset{˙}{\lor} U = (R \underset{˙}{\lor} U) \underset{˙}{\land} W$
32	10 11 27 24 30 31	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))) \to (R \underset{˙}{\land} W) \underset{˙}{\lor} U = (R \underset{˙}{\lor} U) \underset{˙}{\land} W$
33		eqid	$⊢ 0. (K) = 0. (K)$
34	1 3 33 4 5	lhpmat	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to R \underset{˙}{\land} W = 0. (K)$
35	34	3ad2antr3	$⊢ ((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))) \to R \underset{˙}{\land} W = 0. (K)$
36	35	oveq1d	$⊢ ((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))) \to (R \underset{˙}{\land} W) \underset{˙}{\lor} U = 0. (K) \underset{˙}{\lor} U$
37		hlol	$⊢ K \in HL \to K \in OL$
38	37	ad2antrr	$⊢ ((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))) \to K \in OL$
39	15 2 33	olj02	$⊢ (K \in OL \land U \in {Base}_{K}) \to 0. (K) \underset{˙}{\lor} U = U$
40	38 27 39	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))) \to 0. (K) \underset{˙}{\lor} U = U$
41	36 40	eqtrd	$⊢ ((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))) \to (R \underset{˙}{\land} W) \underset{˙}{\lor} U = U$
42	9 32 41	3eqtr2d	$⊢ ((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))) \to (R \underset{˙}{\lor} F) \underset{˙}{\land} W = U$

Metamath Proof Explorer

Theorem cdleme2

Proof