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 ) )