Metamath Proof Explorer


Theorem dalem-cly

Description: Lemma for dalem9 . Center of perspectivity C is not in plane Y (when Y and Z are different planes). (Contributed by NM, 13-Aug-2012)

Ref Expression
Hypotheses dalema.ph ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( 𝑌𝑂𝑍𝑂 ) ∧ ( ( ¬ 𝐶 ( 𝑃 𝑄 ) ∧ ¬ 𝐶 ( 𝑄 𝑅 ) ∧ ¬ 𝐶 ( 𝑅 𝑃 ) ) ∧ ( ¬ 𝐶 ( 𝑆 𝑇 ) ∧ ¬ 𝐶 ( 𝑇 𝑈 ) ∧ ¬ 𝐶 ( 𝑈 𝑆 ) ) ∧ ( 𝐶 ( 𝑃 𝑆 ) ∧ 𝐶 ( 𝑄 𝑇 ) ∧ 𝐶 ( 𝑅 𝑈 ) ) ) ) )
dalemc.l = ( le ‘ 𝐾 )
dalemc.j = ( join ‘ 𝐾 )
dalemc.a 𝐴 = ( Atoms ‘ 𝐾 )
dalem-cly.o 𝑂 = ( LPlanes ‘ 𝐾 )
dalem-cly.y 𝑌 = ( ( 𝑃 𝑄 ) 𝑅 )
dalem-cly.z 𝑍 = ( ( 𝑆 𝑇 ) 𝑈 )
Assertion dalem-cly ( ( 𝜑𝑌𝑍 ) → ¬ 𝐶 𝑌 )

Proof

Step Hyp Ref Expression
1 dalema.ph ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( 𝑌𝑂𝑍𝑂 ) ∧ ( ( ¬ 𝐶 ( 𝑃 𝑄 ) ∧ ¬ 𝐶 ( 𝑄 𝑅 ) ∧ ¬ 𝐶 ( 𝑅 𝑃 ) ) ∧ ( ¬ 𝐶 ( 𝑆 𝑇 ) ∧ ¬ 𝐶 ( 𝑇 𝑈 ) ∧ ¬ 𝐶 ( 𝑈 𝑆 ) ) ∧ ( 𝐶 ( 𝑃 𝑆 ) ∧ 𝐶 ( 𝑄 𝑇 ) ∧ 𝐶 ( 𝑅 𝑈 ) ) ) ) )
2 dalemc.l = ( le ‘ 𝐾 )
3 dalemc.j = ( join ‘ 𝐾 )
4 dalemc.a 𝐴 = ( Atoms ‘ 𝐾 )
5 dalem-cly.o 𝑂 = ( LPlanes ‘ 𝐾 )
6 dalem-cly.y 𝑌 = ( ( 𝑃 𝑄 ) 𝑅 )
7 dalem-cly.z 𝑍 = ( ( 𝑆 𝑇 ) 𝑈 )
8 1 dalemkelat ( 𝜑𝐾 ∈ Lat )
9 1 4 dalemceb ( 𝜑𝐶 ∈ ( Base ‘ 𝐾 ) )
10 1 5 dalemyeb ( 𝜑𝑌 ∈ ( Base ‘ 𝐾 ) )
11 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12 11 2 3 latleeqj1 ( ( 𝐾 ∈ Lat ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐶 𝑌 ↔ ( 𝐶 𝑌 ) = 𝑌 ) )
13 8 9 10 12 syl3anc ( 𝜑 → ( 𝐶 𝑌 ↔ ( 𝐶 𝑌 ) = 𝑌 ) )
14 1 dalemclpjs ( 𝜑𝐶 ( 𝑃 𝑆 ) )
15 1 dalemkehl ( 𝜑𝐾 ∈ HL )
16 1 2 3 4 5 6 dalemcea ( 𝜑𝐶𝐴 )
17 1 dalemsea ( 𝜑𝑆𝐴 )
18 1 dalempea ( 𝜑𝑃𝐴 )
19 1 dalemqea ( 𝜑𝑄𝐴 )
20 1 dalem-clpjq ( 𝜑 → ¬ 𝐶 ( 𝑃 𝑄 ) )
21 2 3 4 atnlej1 ( ( 𝐾 ∈ HL ∧ ( 𝐶𝐴𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝐶 ( 𝑃 𝑄 ) ) → 𝐶𝑃 )
22 15 16 18 19 20 21 syl131anc ( 𝜑𝐶𝑃 )
23 2 3 4 hlatexch1 ( ( 𝐾 ∈ HL ∧ ( 𝐶𝐴𝑆𝐴𝑃𝐴 ) ∧ 𝐶𝑃 ) → ( 𝐶 ( 𝑃 𝑆 ) → 𝑆 ( 𝑃 𝐶 ) ) )
24 15 16 17 18 22 23 syl131anc ( 𝜑 → ( 𝐶 ( 𝑃 𝑆 ) → 𝑆 ( 𝑃 𝐶 ) ) )
25 14 24 mpd ( 𝜑𝑆 ( 𝑃 𝐶 ) )
26 3 4 hlatjcom ( ( 𝐾 ∈ HL ∧ 𝐶𝐴𝑃𝐴 ) → ( 𝐶 𝑃 ) = ( 𝑃 𝐶 ) )
27 15 16 18 26 syl3anc ( 𝜑 → ( 𝐶 𝑃 ) = ( 𝑃 𝐶 ) )
28 25 27 breqtrrd ( 𝜑𝑆 ( 𝐶 𝑃 ) )
29 1 dalemclqjt ( 𝜑𝐶 ( 𝑄 𝑇 ) )
30 1 dalemtea ( 𝜑𝑇𝐴 )
31 1 dalemrea ( 𝜑𝑅𝐴 )
32 simp312 ( ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( 𝑌𝑂𝑍𝑂 ) ∧ ( ( ¬ 𝐶 ( 𝑃 𝑄 ) ∧ ¬ 𝐶 ( 𝑄 𝑅 ) ∧ ¬ 𝐶 ( 𝑅 𝑃 ) ) ∧ ( ¬ 𝐶 ( 𝑆 𝑇 ) ∧ ¬ 𝐶 ( 𝑇 𝑈 ) ∧ ¬ 𝐶 ( 𝑈 𝑆 ) ) ∧ ( 𝐶 ( 𝑃 𝑆 ) ∧ 𝐶 ( 𝑄 𝑇 ) ∧ 𝐶 ( 𝑅 𝑈 ) ) ) ) → ¬ 𝐶 ( 𝑄 𝑅 ) )
33 1 32 sylbi ( 𝜑 → ¬ 𝐶 ( 𝑄 𝑅 ) )
34 2 3 4 atnlej1 ( ( 𝐾 ∈ HL ∧ ( 𝐶𝐴𝑄𝐴𝑅𝐴 ) ∧ ¬ 𝐶 ( 𝑄 𝑅 ) ) → 𝐶𝑄 )
35 15 16 19 31 33 34 syl131anc ( 𝜑𝐶𝑄 )
36 2 3 4 hlatexch1 ( ( 𝐾 ∈ HL ∧ ( 𝐶𝐴𝑇𝐴𝑄𝐴 ) ∧ 𝐶𝑄 ) → ( 𝐶 ( 𝑄 𝑇 ) → 𝑇 ( 𝑄 𝐶 ) ) )
37 15 16 30 19 35 36 syl131anc ( 𝜑 → ( 𝐶 ( 𝑄 𝑇 ) → 𝑇 ( 𝑄 𝐶 ) ) )
38 29 37 mpd ( 𝜑𝑇 ( 𝑄 𝐶 ) )
39 3 4 hlatjcom ( ( 𝐾 ∈ HL ∧ 𝐶𝐴𝑄𝐴 ) → ( 𝐶 𝑄 ) = ( 𝑄 𝐶 ) )
40 15 16 19 39 syl3anc ( 𝜑 → ( 𝐶 𝑄 ) = ( 𝑄 𝐶 ) )
41 38 40 breqtrrd ( 𝜑𝑇 ( 𝐶 𝑄 ) )
42 1 4 dalemseb ( 𝜑𝑆 ∈ ( Base ‘ 𝐾 ) )
43 11 3 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝐶𝐴𝑃𝐴 ) → ( 𝐶 𝑃 ) ∈ ( Base ‘ 𝐾 ) )
44 15 16 18 43 syl3anc ( 𝜑 → ( 𝐶 𝑃 ) ∈ ( Base ‘ 𝐾 ) )
45 1 4 dalemteb ( 𝜑𝑇 ∈ ( Base ‘ 𝐾 ) )
46 11 3 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝐶𝐴𝑄𝐴 ) → ( 𝐶 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
47 15 16 19 46 syl3anc ( 𝜑 → ( 𝐶 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
48 11 2 3 latjlej12 ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐶 𝑃 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐶 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑆 ( 𝐶 𝑃 ) ∧ 𝑇 ( 𝐶 𝑄 ) ) → ( 𝑆 𝑇 ) ( ( 𝐶 𝑃 ) ( 𝐶 𝑄 ) ) ) )
49 8 42 44 45 47 48 syl122anc ( 𝜑 → ( ( 𝑆 ( 𝐶 𝑃 ) ∧ 𝑇 ( 𝐶 𝑄 ) ) → ( 𝑆 𝑇 ) ( ( 𝐶 𝑃 ) ( 𝐶 𝑄 ) ) ) )
50 28 41 49 mp2and ( 𝜑 → ( 𝑆 𝑇 ) ( ( 𝐶 𝑃 ) ( 𝐶 𝑄 ) ) )
51 1 4 dalempeb ( 𝜑𝑃 ∈ ( Base ‘ 𝐾 ) )
52 1 4 dalemqeb ( 𝜑𝑄 ∈ ( Base ‘ 𝐾 ) )
53 11 3 latjjdi ( ( 𝐾 ∈ Lat ∧ ( 𝐶 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝐶 ( 𝑃 𝑄 ) ) = ( ( 𝐶 𝑃 ) ( 𝐶 𝑄 ) ) )
54 8 9 51 52 53 syl13anc ( 𝜑 → ( 𝐶 ( 𝑃 𝑄 ) ) = ( ( 𝐶 𝑃 ) ( 𝐶 𝑄 ) ) )
55 50 54 breqtrrd ( 𝜑 → ( 𝑆 𝑇 ) ( 𝐶 ( 𝑃 𝑄 ) ) )
56 1 dalemclrju ( 𝜑𝐶 ( 𝑅 𝑈 ) )
57 1 dalemuea ( 𝜑𝑈𝐴 )
58 simp313 ( ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( 𝑌𝑂𝑍𝑂 ) ∧ ( ( ¬ 𝐶 ( 𝑃 𝑄 ) ∧ ¬ 𝐶 ( 𝑄 𝑅 ) ∧ ¬ 𝐶 ( 𝑅 𝑃 ) ) ∧ ( ¬ 𝐶 ( 𝑆 𝑇 ) ∧ ¬ 𝐶 ( 𝑇 𝑈 ) ∧ ¬ 𝐶 ( 𝑈 𝑆 ) ) ∧ ( 𝐶 ( 𝑃 𝑆 ) ∧ 𝐶 ( 𝑄 𝑇 ) ∧ 𝐶 ( 𝑅 𝑈 ) ) ) ) → ¬ 𝐶 ( 𝑅 𝑃 ) )
59 1 58 sylbi ( 𝜑 → ¬ 𝐶 ( 𝑅 𝑃 ) )
60 2 3 4 atnlej1 ( ( 𝐾 ∈ HL ∧ ( 𝐶𝐴𝑅𝐴𝑃𝐴 ) ∧ ¬ 𝐶 ( 𝑅 𝑃 ) ) → 𝐶𝑅 )
61 15 16 31 18 59 60 syl131anc ( 𝜑𝐶𝑅 )
62 2 3 4 hlatexch1 ( ( 𝐾 ∈ HL ∧ ( 𝐶𝐴𝑈𝐴𝑅𝐴 ) ∧ 𝐶𝑅 ) → ( 𝐶 ( 𝑅 𝑈 ) → 𝑈 ( 𝑅 𝐶 ) ) )
63 15 16 57 31 61 62 syl131anc ( 𝜑 → ( 𝐶 ( 𝑅 𝑈 ) → 𝑈 ( 𝑅 𝐶 ) ) )
64 56 63 mpd ( 𝜑𝑈 ( 𝑅 𝐶 ) )
65 3 4 hlatjcom ( ( 𝐾 ∈ HL ∧ 𝐶𝐴𝑅𝐴 ) → ( 𝐶 𝑅 ) = ( 𝑅 𝐶 ) )
66 15 16 31 65 syl3anc ( 𝜑 → ( 𝐶 𝑅 ) = ( 𝑅 𝐶 ) )
67 64 66 breqtrrd ( 𝜑𝑈 ( 𝐶 𝑅 ) )
68 1 3 4 dalemsjteb ( 𝜑 → ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
69 1 3 4 dalempjqeb ( 𝜑 → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
70 11 3 latjcl ( ( 𝐾 ∈ Lat ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐶 ( 𝑃 𝑄 ) ) ∈ ( Base ‘ 𝐾 ) )
71 8 9 69 70 syl3anc ( 𝜑 → ( 𝐶 ( 𝑃 𝑄 ) ) ∈ ( Base ‘ 𝐾 ) )
72 1 4 dalemueb ( 𝜑𝑈 ∈ ( Base ‘ 𝐾 ) )
73 11 3 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝐶𝐴𝑅𝐴 ) → ( 𝐶 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
74 15 16 31 73 syl3anc ( 𝜑 → ( 𝐶 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
75 11 2 3 latjlej12 ( ( 𝐾 ∈ Lat ∧ ( ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐶 ( 𝑃 𝑄 ) ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐶 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑆 𝑇 ) ( 𝐶 ( 𝑃 𝑄 ) ) ∧ 𝑈 ( 𝐶 𝑅 ) ) → ( ( 𝑆 𝑇 ) 𝑈 ) ( ( 𝐶 ( 𝑃 𝑄 ) ) ( 𝐶 𝑅 ) ) ) )
76 8 68 71 72 74 75 syl122anc ( 𝜑 → ( ( ( 𝑆 𝑇 ) ( 𝐶 ( 𝑃 𝑄 ) ) ∧ 𝑈 ( 𝐶 𝑅 ) ) → ( ( 𝑆 𝑇 ) 𝑈 ) ( ( 𝐶 ( 𝑃 𝑄 ) ) ( 𝐶 𝑅 ) ) ) )
77 55 67 76 mp2and ( 𝜑 → ( ( 𝑆 𝑇 ) 𝑈 ) ( ( 𝐶 ( 𝑃 𝑄 ) ) ( 𝐶 𝑅 ) ) )
78 1 4 dalemreb ( 𝜑𝑅 ∈ ( Base ‘ 𝐾 ) )
79 11 3 latjjdi ( ( 𝐾 ∈ Lat ∧ ( 𝐶 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝐶 ( ( 𝑃 𝑄 ) 𝑅 ) ) = ( ( 𝐶 ( 𝑃 𝑄 ) ) ( 𝐶 𝑅 ) ) )
80 8 9 69 78 79 syl13anc ( 𝜑 → ( 𝐶 ( ( 𝑃 𝑄 ) 𝑅 ) ) = ( ( 𝐶 ( 𝑃 𝑄 ) ) ( 𝐶 𝑅 ) ) )
81 77 80 breqtrrd ( 𝜑 → ( ( 𝑆 𝑇 ) 𝑈 ) ( 𝐶 ( ( 𝑃 𝑄 ) 𝑅 ) ) )
82 6 oveq2i ( 𝐶 𝑌 ) = ( 𝐶 ( ( 𝑃 𝑄 ) 𝑅 ) )
83 81 7 82 3brtr4g ( 𝜑𝑍 ( 𝐶 𝑌 ) )
84 breq2 ( ( 𝐶 𝑌 ) = 𝑌 → ( 𝑍 ( 𝐶 𝑌 ) ↔ 𝑍 𝑌 ) )
85 83 84 syl5ibcom ( 𝜑 → ( ( 𝐶 𝑌 ) = 𝑌𝑍 𝑌 ) )
86 13 85 sylbid ( 𝜑 → ( 𝐶 𝑌𝑍 𝑌 ) )
87 1 dalemzeo ( 𝜑𝑍𝑂 )
88 1 dalemyeo ( 𝜑𝑌𝑂 )
89 2 5 lplncmp ( ( 𝐾 ∈ HL ∧ 𝑍𝑂𝑌𝑂 ) → ( 𝑍 𝑌𝑍 = 𝑌 ) )
90 15 87 88 89 syl3anc ( 𝜑 → ( 𝑍 𝑌𝑍 = 𝑌 ) )
91 eqcom ( 𝑍 = 𝑌𝑌 = 𝑍 )
92 90 91 bitrdi ( 𝜑 → ( 𝑍 𝑌𝑌 = 𝑍 ) )
93 86 92 sylibd ( 𝜑 → ( 𝐶 𝑌𝑌 = 𝑍 ) )
94 93 necon3ad ( 𝜑 → ( 𝑌𝑍 → ¬ 𝐶 𝑌 ) )
95 94 imp ( ( 𝜑𝑌𝑍 ) → ¬ 𝐶 𝑌 )