cdlemc4

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

	Ref	Expression
Hypotheses	cdlemc3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemc3.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemc3.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemc3.a	$⊢ A = Atoms (K)$
	cdlemc3.h	$⊢ H = LHyp (K)$
	cdlemc3.t	$⊢ T = LTrn (K) (W)$
	cdlemc3.r	$⊢ R = trL (K) (W)$
Assertion	cdlemc4	$⊢ ((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)) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \to Q \underset{˙}{\lor} R (F) \neq F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$

Proof

Step	Hyp	Ref	Expression
1		cdlemc3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemc3.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemc3.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemc3.a	$⊢ A = Atoms (K)$
5		cdlemc3.h	$⊢ H = LHyp (K)$
6		cdlemc3.t	$⊢ T = LTrn (K) (W)$
7		cdlemc3.r	$⊢ R = trL (K) (W)$
8		simpll	$⊢ ((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$
9	8	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$
10		simpl	$⊢ ((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)$
11		simpr1	$⊢ ((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$
12		simpr2l	$⊢ ((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$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14	13 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
15	12 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 P \in {Base}_{K}$
16	13 5 6	ltrncl	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in {Base}_{K}) \to F (P) \in {Base}_{K}$
17	10 11 15 16	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 F (P) \in {Base}_{K}$
18		simpr3l	$⊢ ((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$
19	13 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
20	8 12 18 19	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}$
21	13 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
22	21	ad2antlr	$⊢ ((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}$
23	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}$
24	9 20 22 23	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}$
25	13 1 2	latlej1	$⊢ (K \in Lat \land F (P) \in {Base}_{K} \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K}) \to F (P) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
26	9 17 24 25	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 F (P) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
27		breq2	$⊢ Q \underset{˙}{\lor} R (F) = F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \to (F (P) \underset{˙}{\leq} (Q \underset{˙}{\lor} R (F)) \leftrightarrow F (P) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)))$
28	26 27	syl5ibrcom	$⊢ ((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{˙}{\lor} R (F) = F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \to F (P) \underset{˙}{\leq} (Q \underset{˙}{\lor} R (F)))$
29	1 2 3 4 5 6 7	cdlemc3	$⊢ ((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{˙}{\leq} (Q \underset{˙}{\lor} R (F)) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))$
30	28 29	syld	$⊢ ((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{˙}{\lor} R (F) = F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))$
31	30	necon3bd	$⊢ ((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 (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \to Q \underset{˙}{\lor} R (F) \neq F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
32	31	3impia	$⊢ ((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)) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \to Q \underset{˙}{\lor} R (F) \neq F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$

Metamath Proof Explorer

Theorem cdlemc4

Proof