Metamath Proof Explorer


Theorem cdlemg18c

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

Ref Expression
Hypotheses cdlemg12.l ˙ = K
cdlemg12.j ˙ = join K
cdlemg12.m ˙ = 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 ˙ Q ˙ W
Assertion cdlemg18c K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q P ˙ F Q ˙ Q ˙ F P A

Proof

Step Hyp Ref Expression
1 cdlemg12.l ˙ = K
2 cdlemg12.j ˙ = join K
3 cdlemg12.m ˙ = 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 ˙ Q ˙ W
9 simp1l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q K HL
10 simp21l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q P A
11 simp1r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q W H
12 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q P A ¬ P ˙ W
13 simp22l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q Q A
14 simp31 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q P Q
15 1 2 3 4 5 8 cdleme0a K HL W H P A ¬ P ˙ W Q A P Q U A
16 9 11 12 13 14 15 syl212anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q U A
17 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q K HL W H
18 simp23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q F T
19 1 4 5 6 ltrnat K HL W H F T Q A F Q A
20 17 18 13 19 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q F Q A
21 1 4 5 6 ltrnat K HL W H F T P A F P A
22 17 18 10 21 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q F P A
23 1 2 3 4 5 6 7 8 cdlemg18b K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q ¬ P ˙ U ˙ F Q
24 simp32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q F P Q
25 24 necomd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q Q F P
26 23 25 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q ¬ P ˙ U ˙ F Q Q F P
27 simp33 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q F Q ˙ F P P ˙ Q
28 1 2 3 4 5 6 7 cdlemg18a K HL W H P A Q A F T P Q F Q ˙ F P P ˙ Q P ˙ F Q Q ˙ F P
29 17 10 13 18 14 27 28 syl132anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q P ˙ F Q Q ˙ F P
30 1 2 4 hlatlej2 K HL P A Q A Q ˙ P ˙ Q
31 9 10 13 30 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q Q ˙ P ˙ Q
32 1 2 3 4 5 8 cdleme0cp K HL W H P A ¬ P ˙ W Q A P ˙ U = P ˙ Q
33 9 11 12 13 32 syl22anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q P ˙ U = P ˙ Q
34 31 33 breqtrrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q Q ˙ P ˙ U
35 1 2 4 hlatlej2 K HL F Q A F P A F P ˙ F Q ˙ F P
36 9 20 22 35 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q F P ˙ F Q ˙ F P
37 simp22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q Q A ¬ Q ˙ W
38 5 6 1 2 4 3 8 cdlemg2kq K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T F P ˙ F Q = F Q ˙ U
39 17 12 37 18 38 syl121anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q F P ˙ F Q = F Q ˙ U
40 2 4 hlatjcom K HL F P A F Q A F P ˙ F Q = F Q ˙ F P
41 9 22 20 40 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q F P ˙ F Q = F Q ˙ F P
42 2 4 hlatjcom K HL F Q A U A F Q ˙ U = U ˙ F Q
43 9 20 16 42 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q F Q ˙ U = U ˙ F Q
44 39 41 43 3eqtr3d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q F Q ˙ F P = U ˙ F Q
45 36 44 breqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q F P ˙ U ˙ F Q
46 34 45 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q Q ˙ P ˙ U F P ˙ U ˙ F Q
47 1 2 3 4 ps-2c K HL P A U A F Q A Q A F P A ¬ P ˙ U ˙ F Q Q F P P ˙ F Q Q ˙ F P Q ˙ P ˙ U F P ˙ U ˙ F Q P ˙ F Q ˙ Q ˙ F P A
48 9 10 16 20 13 22 26 29 46 47 syl333anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T P Q F P Q F Q ˙ F P P ˙ Q P ˙ F Q ˙ Q ˙ F P A