Metamath Proof Explorer

Theorem dalem22

Description: Lemma for dath . Show that lines c d and P S determine a plane. (Contributed by NM, 2-Aug-2012)

Ref Expression
Hypotheses dalem.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 ) ) ) ) )
dalem.l 
|- .<_ = ( le ` K )
dalem.j 
|- .\/ = ( join ` K )
dalem.a 
|- A = ( Atoms ` K )
dalem.ps 
|- ( ps <-> ( ( c e. A /\ d e. A ) /\ -. c .<_ Y /\ ( d =/= c /\ -. d .<_ Y /\ C .<_ ( c .\/ d ) ) ) )
dalem22.o 
|- O = ( LPlanes ` K )
dalem22.y 
|- Y = ( ( P .\/ Q ) .\/ R )
dalem22.z 
|- Z = ( ( S .\/ T ) .\/ U )
Assertion dalem22 
|- ( ( ph /\ Y = Z /\ ps ) -> ( ( c .\/ d ) .\/ ( P .\/ S ) ) e. O )

Proof

Step Hyp Ref Expression
1 dalem.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 dalem.l 
 |-  .<_ = ( le ` K )
3 dalem.j 
 |-  .\/ = ( join ` K )
4 dalem.a 
 |-  A = ( Atoms ` K )
5 dalem.ps 
 |-  ( ps <-> ( ( c e. A /\ d e. A ) /\ -. c .<_ Y /\ ( d =/= c /\ -. d .<_ Y /\ C .<_ ( c .\/ d ) ) ) )
6 dalem22.o 
 |-  O = ( LPlanes ` K )
7 dalem22.y 
 |-  Y = ( ( P .\/ Q ) .\/ R )
8 dalem22.z 
 |-  Z = ( ( S .\/ T ) .\/ U )
9 eqid 
 |-  ( meet ` K ) = ( meet ` K )
10 1 2 3 4 5 9 6 7 8 dalem21 
 |-  ( ( ph /\ Y = Z /\ ps ) -> ( ( c .\/ d ) ( meet ` K ) ( P .\/ S ) ) e. A )
11 1 dalemkehl 
 |-  ( ph -> K e. HL )
12 11 adantr 
 |-  ( ( ph /\ ps ) -> K e. HL )
13 1 2 3 4 5 dalemcjden 
 |-  ( ( ph /\ ps ) -> ( c .\/ d ) e. ( LLines ` K ) )
14 1 2 3 4 6 7 dalempjsen 
 |-  ( ph -> ( P .\/ S ) e. ( LLines ` K ) )
15 14 adantr 
 |-  ( ( ph /\ ps ) -> ( P .\/ S ) e. ( LLines ` K ) )
16 eqid 
 |-  ( LLines ` K ) = ( LLines ` K )
17 3 9 4 16 6 2llnmj 
 |-  ( ( K e. HL /\ ( c .\/ d ) e. ( LLines ` K ) /\ ( P .\/ S ) e. ( LLines ` K ) ) -> ( ( ( c .\/ d ) ( meet ` K ) ( P .\/ S ) ) e. A <-> ( ( c .\/ d ) .\/ ( P .\/ S ) ) e. O ) )
18 12 13 15 17 syl3anc 
 |-  ( ( ph /\ ps ) -> ( ( ( c .\/ d ) ( meet ` K ) ( P .\/ S ) ) e. A <-> ( ( c .\/ d ) .\/ ( P .\/ S ) ) e. O ) )
19 18 3adant2 
 |-  ( ( ph /\ Y = Z /\ ps ) -> ( ( ( c .\/ d ) ( meet ` K ) ( P .\/ S ) ) e. A <-> ( ( c .\/ d ) .\/ ( P .\/ S ) ) e. O ) )
20 10 19 mpbid 
 |-  ( ( ph /\ Y = Z /\ ps ) -> ( ( c .\/ d ) .\/ ( P .\/ S ) ) e. O )