cdleme16aN

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph on p. 114, showing, in their notation, s \/ u =/= t \/ u. (Contributed by NM, 9-Oct-2012) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cdleme11.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme11.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme11.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme11.a	$⊢ A = Atoms (K)$
5		cdleme11.h	$⊢ H = LHyp (K)$
6		cdleme11.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		simp1ll	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A \land T \in A) \land (P \neq Q \land S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to K \in HL$
8		simp22	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A \land T \in A) \land (P \neq Q \land S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \in A$
9		simp23	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A \land T \in A) \land (P \neq Q \land S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to T \in A$
10		simp1l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A \land T \in A) \land (P \neq Q \land S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (K \in HL \land W \in H)$
11		simp1r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A \land T \in A) \land (P \neq Q \land S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
12		simp21	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A \land T \in A) \land (P \neq Q \land S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to Q \in A$
13		simp31	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A \land T \in A) \land (P \neq Q \land S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to P \neq Q$
14	1 2 3 4 5 6	lhpat2	$⊢ ((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)) \to U \in A$
15	10 11 12 13 14	syl112anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A \land T \in A) \land (P \neq Q \land S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to U \in A$
16		simp32	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A \land T \in A) \land (P \neq Q \land S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \neq T$
17		simp33	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A \land T \in A) \land (P \neq Q \land S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
18		eqid	$⊢ LPlanes (K) = LPlanes (K)$
19	1 2 4 18	lplni2	$⊢ (K \in HL \land (S \in A \land T \in A \land U \in A) \land (S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \underset{˙}{\lor} T) \underset{˙}{\lor} U \in LPlanes (K)$
20	7 8 9 15 16 17 19	syl132anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A \land T \in A) \land (P \neq Q \land S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \underset{˙}{\lor} T) \underset{˙}{\lor} U \in LPlanes (K)$
21		eqid	$⊢ (S \underset{˙}{\lor} T) \underset{˙}{\lor} U = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
22	2 4 18 21	lplnllnneN	$⊢ (K \in HL \land (S \in A \land T \in A \land U \in A) \land (S \underset{˙}{\lor} T) \underset{˙}{\lor} U \in LPlanes (K)) \to S \underset{˙}{\lor} U \neq T \underset{˙}{\lor} U$
23	7 8 9 15 20 22	syl131anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \in A \land S \in A \land T \in A) \land (P \neq Q \land S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \underset{˙}{\lor} U \neq T \underset{˙}{\lor} U$

Metamath Proof Explorer

Theorem cdleme16aN

Proof