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 
|- ( ph <-> ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) /\ ( Y e. O /\ Z e. O ) /\ ( ( -. C .<_ ( P .\/ Q ) /\ -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) ) /\ ( -. C .<_ ( S .\/ T ) /\ -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) ) /\ ( C .<_ ( P .\/ S ) /\ C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) ) ) ) )
dalemc.l 
|- .<_ = ( le ` K )
dalemc.j 
|- .\/ = ( join ` K )
dalemc.a 
|- A = ( Atoms ` K )
dalem-cly.o 
|- O = ( LPlanes ` K )
dalem-cly.y 
|- Y = ( ( P .\/ Q ) .\/ R )
dalem-cly.z 
|- Z = ( ( S .\/ T ) .\/ U )
Assertion dalem-cly 
|- ( ( ph /\ Y =/= Z ) -> -. C .<_ Y )

Proof

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