cdlemg18c

Description: Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemg12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg12.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemg12.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemg12.a	$⊢ A = Atoms (K)$
5		cdlemg12.h	$⊢ H = LHyp (K)$
6		cdlemg12.t	$⊢ T = LTrn (K) (W)$
7		cdlemg12b.r	$⊢ R = trL (K) (W)$
8		cdlemg18b.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
9		simp1l	$⊢ ((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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to K \in HL$
10		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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to P \in A$
11		simp1r	$⊢ ((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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to W \in H$
12		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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
13		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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to Q \in A$
14		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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to P \neq Q$
15	1 2 3 4 5 8	cdleme0a	$⊢ ((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$
16	9 11 12 13 14 15	syl212anc	$⊢ ((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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to U \in A$
17		simp1	$⊢ ((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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to (K \in HL \land W \in H)$
18		simp23	$⊢ ((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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to F \in T$
19	1 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land Q \in A) \to F (Q) \in A$
20	17 18 13 19	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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to F (Q) \in A$
21	1 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in A) \to F (P) \in A$
22	17 18 10 21	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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to F (P) \in A$
23	1 2 3 4 5 6 7 8	cdlemg18b	$⊢ ((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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to \neg P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q))$
24		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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to F (P) \neq Q$
25	24	necomd	$⊢ ((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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to Q \neq F (P)$
26	23 25	jca	$⊢ ((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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to (\neg P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)) \land Q \neq F (P))$
27		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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q$
28	1 2 3 4 5 6 7	cdlemg18a	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land F \in T) \land (P \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} F (Q) \neq Q \underset{˙}{\lor} F (P)$
29	17 10 13 18 14 27 28	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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} F (Q) \neq Q \underset{˙}{\lor} F (P)$
30	1 2 4	hlatlej2	$⊢ (K \in HL \land P \in A \land Q \in A) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
31	9 10 13 30	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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
32	1 2 3 4 5 8	cdleme0cp	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)) \to P \underset{˙}{\lor} U = P \underset{˙}{\lor} Q$
33	9 11 12 13 32	syl22anc	$⊢ ((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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} U = P \underset{˙}{\lor} Q$
34	31 33	breqtrrd	$⊢ ((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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
35	1 2 4	hlatlej2	$⊢ (K \in HL \land F (Q) \in A \land F (P) \in A) \to F (P) \underset{˙}{\leq} (F (Q) \underset{˙}{\lor} F (P))$
36	9 20 22 35	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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to F (P) \underset{˙}{\leq} (F (Q) \underset{˙}{\lor} F (P))$
37		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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
38	5 6 1 2 4 3 8	cdlemg2kq	$⊢ ((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 F \in T) \to F (P) \underset{˙}{\lor} F (Q) = F (Q) \underset{˙}{\lor} U$
39	17 12 37 18 38	syl121anc	$⊢ ((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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to F (P) \underset{˙}{\lor} F (Q) = F (Q) \underset{˙}{\lor} U$
40	2 4	hlatjcom	$⊢ (K \in HL \land F (P) \in A \land F (Q) \in A) \to F (P) \underset{˙}{\lor} F (Q) = F (Q) \underset{˙}{\lor} F (P)$
41	9 22 20 40	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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to F (P) \underset{˙}{\lor} F (Q) = F (Q) \underset{˙}{\lor} F (P)$
42	2 4	hlatjcom	$⊢ (K \in HL \land F (Q) \in A \land U \in A) \to F (Q) \underset{˙}{\lor} U = U \underset{˙}{\lor} F (Q)$
43	9 20 16 42	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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to F (Q) \underset{˙}{\lor} U = U \underset{˙}{\lor} F (Q)$
44	39 41 43	3eqtr3d	$⊢ ((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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to F (Q) \underset{˙}{\lor} F (P) = U \underset{˙}{\lor} F (Q)$
45	36 44	breqtrd	$⊢ ((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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to F (P) \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q))$
46	34 45	jca	$⊢ ((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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} U) \land F (P) \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))$
47	1 2 3 4	ps-2c	$⊢ ((K \in HL \land P \in A \land U \in A) \land (F (Q) \in A \land Q \in A \land F (P) \in A) \land ((\neg P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)) \land Q \neq F (P)) \land P \underset{˙}{\lor} F (Q) \neq Q \underset{˙}{\lor} F (P) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} U) \land F (P) \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q))))) \to (P \underset{˙}{\lor} F (Q)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (P)) \in A$
48	9 10 16 20 13 22 26 29 46 47	syl333anc	$⊢ ((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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to (P \underset{˙}{\lor} F (Q)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (P)) \in A$

Metamath Proof Explorer

Theorem cdlemg18c

Proof