cdlemc2

Description: Part of proof of Lemma C in Crawley p. 112. (Contributed by NM, 25-May-2012)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemc2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemc2.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemc2.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemc2.a	$⊢ A = Atoms (K)$
5		cdlemc2.h	$⊢ H = LHyp (K)$
6		cdlemc2.t	$⊢ T = LTrn (K) (W)$
7		simp1l	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to K \in HL$
8		simp3ll	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to P \in A$
9		simp3rl	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to Q \in A$
10	1 2 4	hlatlej2	$⊢ (K \in HL \land P \in A \land Q \in A) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
11	7 8 9 10	syl3anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
12		simp1	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to (K \in HL \land W \in H)$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14	13 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
15	9 14	syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to Q \in {Base}_{K}$
16		simp3l	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
17	13 1 2 3 4 5	cdlemc1	$⊢ ((K \in HL \land W \in H) \land Q \in {Base}_{K} \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = P \underset{˙}{\lor} Q$
18	12 15 16 17	syl3anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = P \underset{˙}{\lor} Q$
19	11 18	breqtrrd	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
20		simp2	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to F \in T$
21	7	hllatd	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to K \in Lat$
22	13 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
23	8 22	syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to P \in {Base}_{K}$
24	13 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land Q \in {Base}_{K}) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
25	21 23 15 24	syl3anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
26		simp1r	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to W \in H$
27	13 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
28	26 27	syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to W \in {Base}_{K}$
29	13 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}$
30	21 25 28 29	syl3anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K}$
31	13 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K}) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \in {Base}_{K}$
32	21 23 30 31	syl3anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \in {Base}_{K}$
33	13 1 5 6	ltrnle	$⊢ ((K \in HL \land W \in H) \land F \in T \land (Q \in {Base}_{K} \land P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \in {Base}_{K})) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \leftrightarrow F (Q) \underset{˙}{\leq} F (P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)))$
34	12 20 15 32 33	syl112anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \leftrightarrow F (Q) \underset{˙}{\leq} F (P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)))$
35	19 34	mpbid	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to F (Q) \underset{˙}{\leq} F (P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
36	13 2 5 6	ltrnj	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in {Base}_{K} \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K})) \to F (P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) = F (P) \underset{˙}{\lor} F ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
37	12 20 23 30 36	syl112anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to F (P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) = F (P) \underset{˙}{\lor} F ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
38	13 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$
39	21 25 28 38	syl3anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
40	13 1 5 6	ltrnval1	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K} \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W)) \to F ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
41	12 20 30 39 40	syl112anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to F ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
42	41	oveq2d	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to F (P) \underset{˙}{\lor} F ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
43	37 42	eqtrd	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to F (P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) = F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
44	35 43	breqtrd	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to F (Q) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$

Metamath Proof Explorer

Theorem cdlemc2

Proof