Metamath Proof Explorer

Theorem cdlemc

Description: 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	cdlemc	$⊢ ((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 F (Q) = (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (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		simpl1	$⊢ (((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))) \land F (P) = P) \to (K \in HL \land W \in H)$
9		simpl2	$⊢ (((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))) \land F (P) = P) \to (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))$
10		simpr	$⊢ (((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))) \land F (P) = P) \to F (P) = P$
11	1 2 3 4 5 6 7	cdlemc6	$⊢ ((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 F (P) = P) \to F (Q) = (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
12	8 9 10 11	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)) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = P) \to F (Q) = (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
13		simpl1	$⊢ (((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))) \land F (P) \neq P) \to (K \in HL \land W \in H)$
14		simpl2	$⊢ (((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))) \land F (P) \neq P) \to (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))$
15		simpl3	$⊢ (((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))) \land F (P) \neq P) \to \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))$
16		simpr	$⊢ (((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))) \land F (P) \neq P) \to F (P) \neq P$
17	1 2 3 4 5 6 7	cdlemc5	$⊢ ((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)) \land F (P) \neq P)) \to F (Q) = (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
18	13 14 15 16 17	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)) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) \neq P) \to F (Q) = (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
19	12 18	pm2.61dane	$⊢ ((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 F (Q) = (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$