Metamath Proof Explorer


Theorem dalem21

Description: Lemma for dath . Show that lines c d and P S intersect at an atom. (Contributed by NM, 2-Aug-2012)

Ref Expression
Hypotheses dalem.ph φKHLCBaseKPAQARASATAUAYOZO¬C˙P˙Q¬C˙Q˙R¬C˙R˙P¬C˙S˙T¬C˙T˙U¬C˙U˙SC˙P˙SC˙Q˙TC˙R˙U
dalem.l ˙=K
dalem.j ˙=joinK
dalem.a A=AtomsK
dalem.ps ψcAdA¬c˙Ydc¬d˙YC˙c˙d
dalem21.m ˙=meetK
dalem21.o O=LPlanesK
dalem21.y Y=P˙Q˙R
dalem21.z Z=S˙T˙U
Assertion dalem21 φY=Zψc˙d˙P˙SA

Proof

Step Hyp Ref Expression
1 dalem.ph φKHLCBaseKPAQARASATAUAYOZO¬C˙P˙Q¬C˙Q˙R¬C˙R˙P¬C˙S˙T¬C˙T˙U¬C˙U˙SC˙P˙SC˙Q˙TC˙R˙U
2 dalem.l ˙=K
3 dalem.j ˙=joinK
4 dalem.a A=AtomsK
5 dalem.ps ψcAdA¬c˙Ydc¬d˙YC˙c˙d
6 dalem21.m ˙=meetK
7 dalem21.o O=LPlanesK
8 dalem21.y Y=P˙Q˙R
9 dalem21.z Z=S˙T˙U
10 1 dalemkehl φKHL
11 10 3ad2ant1 φY=ZψKHL
12 1 2 3 4 5 dalemcjden φψc˙dLLinesK
13 12 3adant2 φY=Zψc˙dLLinesK
14 1 2 3 4 7 8 dalempjsen φP˙SLLinesK
15 14 3ad2ant1 φY=ZψP˙SLLinesK
16 1 2 3 4 7 8 dalemply φP˙Y
17 16 adantr φY=ZP˙Y
18 1 2 3 4 9 dalemsly φY=ZS˙Y
19 1 dalemkelat φKLat
20 1 4 dalempeb φPBaseK
21 1 4 dalemseb φSBaseK
22 1 7 dalemyeb φYBaseK
23 eqid BaseK=BaseK
24 23 2 3 latjle12 KLatPBaseKSBaseKYBaseKP˙YS˙YP˙S˙Y
25 19 20 21 22 24 syl13anc φP˙YS˙YP˙S˙Y
26 25 adantr φY=ZP˙YS˙YP˙S˙Y
27 17 18 26 mpbi2and φY=ZP˙S˙Y
28 27 3adant3 φY=ZψP˙S˙Y
29 5 dalem-ccly ψ¬c˙Y
30 29 adantl φψ¬c˙Y
31 19 adantr φψKLat
32 5 4 dalemcceb ψcBaseK
33 32 adantl φψcBaseK
34 5 dalemddea ψdA
35 23 4 atbase dAdBaseK
36 34 35 syl ψdBaseK
37 36 adantl φψdBaseK
38 23 2 3 latlej1 KLatcBaseKdBaseKc˙c˙d
39 31 33 37 38 syl3anc φψc˙c˙d
40 eqid LLinesK=LLinesK
41 23 40 llnbase c˙dLLinesKc˙dBaseK
42 12 41 syl φψc˙dBaseK
43 22 adantr φψYBaseK
44 23 2 lattr KLatcBaseKc˙dBaseKYBaseKc˙c˙dc˙d˙Yc˙Y
45 31 33 42 43 44 syl13anc φψc˙c˙dc˙d˙Yc˙Y
46 39 45 mpand φψc˙d˙Yc˙Y
47 30 46 mtod φψ¬c˙d˙Y
48 47 3adant2 φY=Zψ¬c˙d˙Y
49 nbrne2 P˙S˙Y¬c˙d˙YP˙Sc˙d
50 28 48 49 syl2anc φY=ZψP˙Sc˙d
51 50 necomd φY=Zψc˙dP˙S
52 hlatl KHLKAtLat
53 10 52 syl φKAtLat
54 53 adantr φψKAtLat
55 1 dalempea φPA
56 1 dalemsea φSA
57 23 3 4 hlatjcl KHLPASAP˙SBaseK
58 10 55 56 57 syl3anc φP˙SBaseK
59 58 adantr φψP˙SBaseK
60 23 6 latmcl KLatc˙dBaseKP˙SBaseKc˙d˙P˙SBaseK
61 31 42 59 60 syl3anc φψc˙d˙P˙SBaseK
62 1 2 3 4 7 8 dalemcea φCA
63 62 adantr φψCA
64 5 dalemclccjdd ψC˙c˙d
65 64 adantl φψC˙c˙d
66 1 dalemclpjs φC˙P˙S
67 66 adantr φψC˙P˙S
68 1 4 dalemceb φCBaseK
69 68 adantr φψCBaseK
70 23 2 6 latlem12 KLatCBaseKc˙dBaseKP˙SBaseKC˙c˙dC˙P˙SC˙c˙d˙P˙S
71 31 69 42 59 70 syl13anc φψC˙c˙dC˙P˙SC˙c˙d˙P˙S
72 65 67 71 mpbi2and φψC˙c˙d˙P˙S
73 eqid 0.K=0.K
74 23 2 73 4 atlen0 KAtLatc˙d˙P˙SBaseKCAC˙c˙d˙P˙Sc˙d˙P˙S0.K
75 54 61 63 72 74 syl31anc φψc˙d˙P˙S0.K
76 75 3adant2 φY=Zψc˙d˙P˙S0.K
77 6 73 4 40 2llnmat KHLc˙dLLinesKP˙SLLinesKc˙dP˙Sc˙d˙P˙S0.Kc˙d˙P˙SA
78 11 13 15 51 76 77 syl32anc φY=Zψc˙d˙P˙SA