cdleme16d

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph on p. 114, 3rd part of 3rd sentence. F and G represent f(s) and f(t) respectively. We show, in their notation, (s \/ t) /\ (f(s) \/ f(t)) is an atom. (Contributed by NM, 11-Oct-2012)

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

Proof

Step	Hyp	Ref	Expression
1		cdleme12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme12.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme12.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme12.a	$⊢ A = Atoms (K)$
5		cdleme12.h	$⊢ H = LHyp (K)$
6		cdleme12.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme12.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
8		cdleme12.g	$⊢ G = (T \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))$
9	1 2 3 4 5 6 7 8	cdleme16c	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \underset{˙}{\lor} T) \underset{˙}{\lor} (F \underset{˙}{\lor} G) = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
10		simp23r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \neq T$
11		simp33	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
12		simp11l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to K \in HL$
13		simp21l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \in A$
14		simp22l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to T \in A$
15		simp11r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to W \in H$
16		simp12l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to P \in A$
17		simp12r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg P \underset{˙}{\leq} W$
18		simp13l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to Q \in A$
19		simp23l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to P \neq Q$
20	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$
21	12 15 16 17 18 19 20	syl222anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to U \in A$
22		eqid	$⊢ LPlanes (K) = LPlanes (K)$
23	1 2 4 22	islpln2a	$⊢ (K \in HL \land (S \in A \land T \in A \land U \in A)) \to ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U \in LPlanes (K) \leftrightarrow (S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T)))$
24	12 13 14 21 23	syl13anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U \in LPlanes (K) \leftrightarrow (S \neq T \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T)))$
25	10 11 24	mpbir2and	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \underset{˙}{\lor} T) \underset{˙}{\lor} U \in LPlanes (K)$
26	9 25	eqeltrd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \underset{˙}{\lor} T) \underset{˙}{\lor} (F \underset{˙}{\lor} G) \in LPlanes (K)$
27		eqid	$⊢ LLines (K) = LLines (K)$
28	2 4 27	islln2a	$⊢ (K \in HL \land S \in A \land T \in A) \to (S \underset{˙}{\lor} T \in LLines (K) \leftrightarrow S \neq T)$
29	12 13 14 28	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \underset{˙}{\lor} T \in LLines (K) \leftrightarrow S \neq T)$
30	10 29	mpbird	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \underset{˙}{\lor} T \in LLines (K)$
31	1 2 3 4 5 6 7 8	cdleme16b	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to F \neq G$
32		simp11	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (K \in HL \land W \in H)$
33		simp12	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
34		simp13	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
35		simp21	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \in A \land \neg S \underset{˙}{\leq} W)$
36		simp31	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
37	1 2 3 4 5 6 7	cdleme3fa	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \in A$
38	32 33 34 35 19 36 37	syl132anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to F \in A$
39		simp22	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (T \in A \land \neg T \underset{˙}{\leq} W)$
40		simp32	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
41	1 2 3 4 5 6 8	cdleme3fa	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (P \neq Q \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to G \in A$
42	32 33 34 39 19 40 41	syl132anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to G \in A$
43	2 4 27	islln2a	$⊢ (K \in HL \land F \in A \land G \in A) \to (F \underset{˙}{\lor} G \in LLines (K) \leftrightarrow F \neq G)$
44	12 38 42 43	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (F \underset{˙}{\lor} G \in LLines (K) \leftrightarrow F \neq G)$
45	31 44	mpbird	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to F \underset{˙}{\lor} G \in LLines (K)$
46	2 3 4 27 22	2llnmj	$⊢ (K \in HL \land S \underset{˙}{\lor} T \in LLines (K) \land F \underset{˙}{\lor} G \in LLines (K)) \to ((S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G) \in A \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\lor} (F \underset{˙}{\lor} G) \in LPlanes (K))$
47	12 30 45 46	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to ((S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G) \in A \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\lor} (F \underset{˙}{\lor} G) \in LPlanes (K))$
48	26 47	mpbird	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G) \in A$

Metamath Proof Explorer

Theorem cdleme16d

Proof