cdleme22a

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 3rd line on p. 115. Show that t \/ v = p \/ q implies v = u. (Contributed by NM, 30-Nov-2012)

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

Proof

Step	Hyp	Ref	Expression
1		cdleme22.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme22.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme22.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme22.a	$⊢ A = Atoms (K)$
5		cdleme22.h	$⊢ H = LHyp (K)$
6		cdleme22.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		simp1	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land T \in A) \land ((V \in A \land V \underset{˙}{\leq} W) \land P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q)) \to (K \in HL \land W \in H)$
8		simp21	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land T \in A) \land ((V \in A \land V \underset{˙}{\leq} W) \land P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
9		simp22	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land T \in A) \land ((V \in A \land V \underset{˙}{\leq} W) \land P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q)) \to Q \in A$
10		simp32	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land T \in A) \land ((V \in A \land V \underset{˙}{\leq} W) \land P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q)) \to P \neq Q$
11		simp31l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land T \in A) \land ((V \in A \land V \underset{˙}{\leq} W) \land P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q)) \to V \in A$
12		simp31r	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land T \in A) \land ((V \in A \land V \underset{˙}{\leq} W) \land P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q)) \to V \underset{˙}{\leq} W$
13		simp1l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land T \in A) \land ((V \in A \land V \underset{˙}{\leq} W) \land P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q)) \to K \in HL$
14		simp23	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land T \in A) \land ((V \in A \land V \underset{˙}{\leq} W) \land P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q)) \to T \in A$
15	1 2 4	hlatlej2	$⊢ (K \in HL \land T \in A \land V \in A) \to V \underset{˙}{\leq} (T \underset{˙}{\lor} V)$
16	13 14 11 15	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land T \in A) \land ((V \in A \land V \underset{˙}{\leq} W) \land P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q)) \to V \underset{˙}{\leq} (T \underset{˙}{\lor} V)$
17		simp33	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land T \in A) \land ((V \in A \land V \underset{˙}{\leq} W) \land P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q)) \to T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q$
18	16 17	breqtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land T \in A) \land ((V \in A \land V \underset{˙}{\leq} W) \land P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q)) \to V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
19	1 2 3 4 5 6	cdleme22aa	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (V \in A \land V \underset{˙}{\leq} W \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to V = U$
20	7 8 9 10 11 12 18 19	syl133anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land T \in A) \land ((V \in A \land V \underset{˙}{\leq} W) \land P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q)) \to V = U$

Metamath Proof Explorer

Theorem cdleme22a

Proof