Metamath Proof Explorer

Theorem dalem8

Description: Lemma for dath . Plane Z belongs to the 3-dimensional space. (Contributed by NM, 21-Jul-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 )
dalem6.o 
|- O = ( LPlanes ` K )
dalem6.y 
|- Y = ( ( P .\/ Q ) .\/ R )
dalem6.z 
|- Z = ( ( S .\/ T ) .\/ U )
dalem6.w 
|- W = ( Y .\/ C )
Assertion dalem8 
|- ( ph -> Z .<_ W )

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 dalem6.o 
 |-  O = ( LPlanes ` K )
6 dalem6.y 
 |-  Y = ( ( P .\/ Q ) .\/ R )
7 dalem6.z 
 |-  Z = ( ( S .\/ T ) .\/ U )
8 dalem6.w 
 |-  W = ( Y .\/ C )
9 1 2 3 4 5 6 7 8 dalem6 
 |-  ( ph -> S .<_ W )
10 1 2 3 4 5 6 7 8 dalem7 
 |-  ( ph -> T .<_ W )
11 1 dalemkelat 
 |-  ( ph -> K e. Lat )
12 1 4 dalemseb 
 |-  ( ph -> S e. ( Base ` K ) )
13 1 4 dalemteb 
 |-  ( ph -> T e. ( Base ` K ) )
14 1 5 dalemyeb 
 |-  ( ph -> Y e. ( Base ` K ) )
15 1 4 dalemceb 
 |-  ( ph -> C e. ( Base ` K ) )
16 eqid 
 |-  ( Base ` K ) = ( Base ` K )
17 16 3 latjcl 
 |-  ( ( K e. Lat /\ Y e. ( Base ` K ) /\ C e. ( Base ` K ) ) -> ( Y .\/ C ) e. ( Base ` K ) )
18 11 14 15 17 syl3anc 
 |-  ( ph -> ( Y .\/ C ) e. ( Base ` K ) )
19 8 18 eqeltrid 
 |-  ( ph -> W e. ( Base ` K ) )
20 16 2 3 latjle12 
 |-  ( ( K e. Lat /\ ( S e. ( Base ` K ) /\ T e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( S .<_ W /\ T .<_ W ) <-> ( S .\/ T ) .<_ W ) )
21 11 12 13 19 20 syl13anc 
 |-  ( ph -> ( ( S .<_ W /\ T .<_ W ) <-> ( S .\/ T ) .<_ W ) )
22 9 10 21 mpbi2and 
 |-  ( ph -> ( S .\/ T ) .<_ W )
23 1 2 3 4 5 6 8 dalem5 
 |-  ( ph -> U .<_ W )
24 1 3 4 dalemsjteb 
 |-  ( ph -> ( S .\/ T ) e. ( Base ` K ) )
25 1 4 dalemueb 
 |-  ( ph -> U e. ( Base ` K ) )
26 16 2 3 latjle12 
 |-  ( ( K e. Lat /\ ( ( S .\/ T ) e. ( Base ` K ) /\ U e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( ( S .\/ T ) .<_ W /\ U .<_ W ) <-> ( ( S .\/ T ) .\/ U ) .<_ W ) )
27 11 24 25 19 26 syl13anc 
 |-  ( ph -> ( ( ( S .\/ T ) .<_ W /\ U .<_ W ) <-> ( ( S .\/ T ) .\/ U ) .<_ W ) )
28 22 23 27 mpbi2and 
 |-  ( ph -> ( ( S .\/ T ) .\/ U ) .<_ W )
29 7 28 eqbrtrid 
 |-  ( ph -> Z .<_ W )