This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dalem16

Description: Lemma for dath . The atoms D , E , and F form a line of perspectivity. This is Desargues's theorem for the special case where planes Y and Z are different. (Contributed by NM, 7-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 )
dalem16.m 
|- ./\ = ( meet ` K )
dalem16.o 
|- O = ( LPlanes ` K )
dalem16.y 
|- Y = ( ( P .\/ Q ) .\/ R )
dalem16.z 
|- Z = ( ( S .\/ T ) .\/ U )
dalem16.d 
|- D = ( ( P .\/ Q ) ./\ ( S .\/ T ) )
dalem16.e 
|- E = ( ( Q .\/ R ) ./\ ( T .\/ U ) )
dalem16.f 
|- F = ( ( R .\/ P ) ./\ ( U .\/ S ) )
Assertion dalem16 
|- ( ( ph /\ Y =/= Z ) -> F .<_ ( D .\/ E ) )

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 dalem16.m 
 |-  ./\ = ( meet ` K )
6 dalem16.o 
 |-  O = ( LPlanes ` K )
7 dalem16.y 
 |-  Y = ( ( P .\/ Q ) .\/ R )
8 dalem16.z 
 |-  Z = ( ( S .\/ T ) .\/ U )
9 dalem16.d 
 |-  D = ( ( P .\/ Q ) ./\ ( S .\/ T ) )
10 dalem16.e 
 |-  E = ( ( Q .\/ R ) ./\ ( T .\/ U ) )
11 dalem16.f 
 |-  F = ( ( R .\/ P ) ./\ ( U .\/ S ) )
12 eqid 
 |-  ( Y ./\ Z ) = ( Y ./\ Z )
13 1 2 3 4 5 6 7 8 12 11 dalem12 
 |-  ( ph -> F .<_ ( Y ./\ Z ) )
14 13 adantr 
 |-  ( ( ph /\ Y =/= Z ) -> F .<_ ( Y ./\ Z ) )
15 1 2 3 4 5 6 7 8 12 9 dalem10 
 |-  ( ph -> D .<_ ( Y ./\ Z ) )
16 1 2 3 4 5 6 7 8 12 10 dalem11 
 |-  ( ph -> E .<_ ( Y ./\ Z ) )
17 1 dalemkelat 
 |-  ( ph -> K e. Lat )
18 1 2 3 4 5 6 7 8 9 dalemdea 
 |-  ( ph -> D e. A )
19 eqid 
 |-  ( Base ` K ) = ( Base ` K )
20 19 4 atbase 
 |-  ( D e. A -> D e. ( Base ` K ) )
21 18 20 syl 
 |-  ( ph -> D e. ( Base ` K ) )
22 1 2 3 4 5 6 7 8 10 dalemeea 
 |-  ( ph -> E e. A )
23 19 4 atbase 
 |-  ( E e. A -> E e. ( Base ` K ) )
24 22 23 syl 
 |-  ( ph -> E e. ( Base ` K ) )
25 1 6 dalemyeb 
 |-  ( ph -> Y e. ( Base ` K ) )
26 1 dalemzeo 
 |-  ( ph -> Z e. O )
27 19 6 lplnbase 
 |-  ( Z e. O -> Z e. ( Base ` K ) )
28 26 27 syl 
 |-  ( ph -> Z e. ( Base ` K ) )
29 19 5 latmcl 
 |-  ( ( K e. Lat /\ Y e. ( Base ` K ) /\ Z e. ( Base ` K ) ) -> ( Y ./\ Z ) e. ( Base ` K ) )
30 17 25 28 29 syl3anc 
 |-  ( ph -> ( Y ./\ Z ) e. ( Base ` K ) )
31 19 2 3 latjle12 
 |-  ( ( K e. Lat /\ ( D e. ( Base ` K ) /\ E e. ( Base ` K ) /\ ( Y ./\ Z ) e. ( Base ` K ) ) ) -> ( ( D .<_ ( Y ./\ Z ) /\ E .<_ ( Y ./\ Z ) ) <-> ( D .\/ E ) .<_ ( Y ./\ Z ) ) )
32 17 21 24 30 31 syl13anc 
 |-  ( ph -> ( ( D .<_ ( Y ./\ Z ) /\ E .<_ ( Y ./\ Z ) ) <-> ( D .\/ E ) .<_ ( Y ./\ Z ) ) )
33 15 16 32 mpbi2and 
 |-  ( ph -> ( D .\/ E ) .<_ ( Y ./\ Z ) )
34 33 adantr 
 |-  ( ( ph /\ Y =/= Z ) -> ( D .\/ E ) .<_ ( Y ./\ Z ) )
35 1 dalemkehl 
 |-  ( ph -> K e. HL )
36 35 adantr 
 |-  ( ( ph /\ Y =/= Z ) -> K e. HL )
37 1 2 3 4 5 6 7 8 9 10 dalemdnee 
 |-  ( ph -> D =/= E )
38 eqid 
 |-  ( LLines ` K ) = ( LLines ` K )
39 3 4 38 llni2 
 |-  ( ( ( K e. HL /\ D e. A /\ E e. A ) /\ D =/= E ) -> ( D .\/ E ) e. ( LLines ` K ) )
40 35 18 22 37 39 syl31anc 
 |-  ( ph -> ( D .\/ E ) e. ( LLines ` K ) )
41 40 adantr 
 |-  ( ( ph /\ Y =/= Z ) -> ( D .\/ E ) e. ( LLines ` K ) )
42 1 2 3 4 5 38 6 7 8 12 dalem15 
 |-  ( ( ph /\ Y =/= Z ) -> ( Y ./\ Z ) e. ( LLines ` K ) )
43 2 38 llncmp 
 |-  ( ( K e. HL /\ ( D .\/ E ) e. ( LLines ` K ) /\ ( Y ./\ Z ) e. ( LLines ` K ) ) -> ( ( D .\/ E ) .<_ ( Y ./\ Z ) <-> ( D .\/ E ) = ( Y ./\ Z ) ) )
44 36 41 42 43 syl3anc 
 |-  ( ( ph /\ Y =/= Z ) -> ( ( D .\/ E ) .<_ ( Y ./\ Z ) <-> ( D .\/ E ) = ( Y ./\ Z ) ) )
45 34 44 mpbid 
 |-  ( ( ph /\ Y =/= Z ) -> ( D .\/ E ) = ( Y ./\ Z ) )
46 14 45 breqtrrd 
 |-  ( ( ph /\ Y =/= Z ) -> F .<_ ( D .\/ E ) )