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

Metamath Proof Explorer

Theorem dalemcea

Description: Lemma for dath . Frequently-used utility lemma. Here we show that C must be an atom. This is an assumption in most presentations of Desargues's theorem; instead, we assume only the C is a lattice element, in order to make later substitutions for C easier. (Contributed by NM, 23-Sep-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 )
dalem1.o 
|- O = ( LPlanes ` K )
dalem1.y 
|- Y = ( ( P .\/ Q ) .\/ R )
Assertion dalemcea 
|- ( ph -> C e. A )

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 dalem1.o 
 |-  O = ( LPlanes ` K )
6 dalem1.y 
 |-  Y = ( ( P .\/ Q ) .\/ R )
7 1 dalemkeop 
 |-  ( ph -> K e. OP )
8 1 4 dalemceb 
 |-  ( ph -> C e. ( Base ` K ) )
9 1 dalemkehl 
 |-  ( ph -> K e. HL )
10 1 2 3 4 5 6 dalempjsen 
 |-  ( ph -> ( P .\/ S ) e. ( LLines ` K ) )
11 1 dalemqea 
 |-  ( ph -> Q e. A )
12 1 dalemtea 
 |-  ( ph -> T e. A )
13 1 2 3 4 5 6 dalemqnet 
 |-  ( ph -> Q =/= T )
14 eqid 
 |-  ( LLines ` K ) = ( LLines ` K )
15 3 4 14 llni2 
 |-  ( ( ( K e. HL /\ Q e. A /\ T e. A ) /\ Q =/= T ) -> ( Q .\/ T ) e. ( LLines ` K ) )
16 9 11 12 13 15 syl31anc 
 |-  ( ph -> ( Q .\/ T ) e. ( LLines ` K ) )
17 1 2 3 4 5 6 dalem1 
 |-  ( ph -> ( P .\/ S ) =/= ( Q .\/ T ) )
18 1 dalem-clpjq 
 |-  ( ph -> -. C .<_ ( P .\/ Q ) )
19 1 3 4 dalempjqeb 
 |-  ( ph -> ( P .\/ Q ) e. ( Base ` K ) )
20 eqid 
 |-  ( Base ` K ) = ( Base ` K )
21 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
22 20 2 21 op0le 
 |-  ( ( K e. OP /\ ( P .\/ Q ) e. ( Base ` K ) ) -> ( 0. ` K ) .<_ ( P .\/ Q ) )
23 7 19 22 syl2anc 
 |-  ( ph -> ( 0. ` K ) .<_ ( P .\/ Q ) )
24 breq1 
 |-  ( C = ( 0. ` K ) -> ( C .<_ ( P .\/ Q ) <-> ( 0. ` K ) .<_ ( P .\/ Q ) ) )
25 23 24 syl5ibrcom 
 |-  ( ph -> ( C = ( 0. ` K ) -> C .<_ ( P .\/ Q ) ) )
26 25 necon3bd 
 |-  ( ph -> ( -. C .<_ ( P .\/ Q ) -> C =/= ( 0. ` K ) ) )
27 18 26 mpd 
 |-  ( ph -> C =/= ( 0. ` K ) )
28 eqid 
 |-  ( lt ` K ) = ( lt ` K )
29 20 28 21 opltn0 
 |-  ( ( K e. OP /\ C e. ( Base ` K ) ) -> ( ( 0. ` K ) ( lt ` K ) C <-> C =/= ( 0. ` K ) ) )
30 7 8 29 syl2anc 
 |-  ( ph -> ( ( 0. ` K ) ( lt ` K ) C <-> C =/= ( 0. ` K ) ) )
31 27 30 mpbird 
 |-  ( ph -> ( 0. ` K ) ( lt ` K ) C )
32 1 dalemclpjs 
 |-  ( ph -> C .<_ ( P .\/ S ) )
33 1 dalemclqjt 
 |-  ( ph -> C .<_ ( Q .\/ T ) )
34 1 dalemkelat 
 |-  ( ph -> K e. Lat )
35 1 dalempea 
 |-  ( ph -> P e. A )
36 1 dalemsea 
 |-  ( ph -> S e. A )
37 20 3 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ S e. A ) -> ( P .\/ S ) e. ( Base ` K ) )
38 9 35 36 37 syl3anc 
 |-  ( ph -> ( P .\/ S ) e. ( Base ` K ) )
39 20 3 4 hlatjcl 
 |-  ( ( K e. HL /\ Q e. A /\ T e. A ) -> ( Q .\/ T ) e. ( Base ` K ) )
40 9 11 12 39 syl3anc 
 |-  ( ph -> ( Q .\/ T ) e. ( Base ` K ) )
41 eqid 
 |-  ( meet ` K ) = ( meet ` K )
42 20 2 41 latlem12 
 |-  ( ( K e. Lat /\ ( C e. ( Base ` K ) /\ ( P .\/ S ) e. ( Base ` K ) /\ ( Q .\/ T ) e. ( Base ` K ) ) ) -> ( ( C .<_ ( P .\/ S ) /\ C .<_ ( Q .\/ T ) ) <-> C .<_ ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) ) )
43 34 8 38 40 42 syl13anc 
 |-  ( ph -> ( ( C .<_ ( P .\/ S ) /\ C .<_ ( Q .\/ T ) ) <-> C .<_ ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) ) )
44 32 33 43 mpbi2and 
 |-  ( ph -> C .<_ ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) )
45 opposet 
 |-  ( K e. OP -> K e. Poset )
46 7 45 syl 
 |-  ( ph -> K e. Poset )
47 20 21 op0cl 
 |-  ( K e. OP -> ( 0. ` K ) e. ( Base ` K ) )
48 7 47 syl 
 |-  ( ph -> ( 0. ` K ) e. ( Base ` K ) )
49 20 41 latmcl 
 |-  ( ( K e. Lat /\ ( P .\/ S ) e. ( Base ` K ) /\ ( Q .\/ T ) e. ( Base ` K ) ) -> ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) e. ( Base ` K ) )
50 34 38 40 49 syl3anc 
 |-  ( ph -> ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) e. ( Base ` K ) )
51 20 2 28 pltletr 
 |-  ( ( K e. Poset /\ ( ( 0. ` K ) e. ( Base ` K ) /\ C e. ( Base ` K ) /\ ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) e. ( Base ` K ) ) ) -> ( ( ( 0. ` K ) ( lt ` K ) C /\ C .<_ ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) ) -> ( 0. ` K ) ( lt ` K ) ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) ) )
52 46 48 8 50 51 syl13anc 
 |-  ( ph -> ( ( ( 0. ` K ) ( lt ` K ) C /\ C .<_ ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) ) -> ( 0. ` K ) ( lt ` K ) ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) ) )
53 31 44 52 mp2and 
 |-  ( ph -> ( 0. ` K ) ( lt ` K ) ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) )
54 20 28 21 opltn0 
 |-  ( ( K e. OP /\ ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) e. ( Base ` K ) ) -> ( ( 0. ` K ) ( lt ` K ) ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) <-> ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) =/= ( 0. ` K ) ) )
55 7 50 54 syl2anc 
 |-  ( ph -> ( ( 0. ` K ) ( lt ` K ) ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) <-> ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) =/= ( 0. ` K ) ) )
56 53 55 mpbid 
 |-  ( ph -> ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) =/= ( 0. ` K ) )
57 41 21 4 14 2llnmat 
 |-  ( ( ( K e. HL /\ ( P .\/ S ) e. ( LLines ` K ) /\ ( Q .\/ T ) e. ( LLines ` K ) ) /\ ( ( P .\/ S ) =/= ( Q .\/ T ) /\ ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) =/= ( 0. ` K ) ) ) -> ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) e. A )
58 9 10 16 17 56 57 syl32anc 
 |-  ( ph -> ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) e. A )
59 20 2 21 4 leat2 
 |-  ( ( ( K e. OP /\ C e. ( Base ` K ) /\ ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) e. A ) /\ ( C =/= ( 0. ` K ) /\ C .<_ ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) ) ) -> C = ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) )
60 7 8 58 27 44 59 syl32anc 
 |-  ( ph -> C = ( ( P .\/ S ) ( meet ` K ) ( Q .\/ T ) ) )
61 60 58 eqeltrd 
 |-  ( ph -> C e. A )