Metamath Proof Explorer

Theorem dalawlem14

Description: Lemma for dalaw . Combine dalawlem10 and dalawlem13 . (Contributed by NM, 6-Oct-2012)

Ref Expression
Hypotheses dalawlem.l 
|- .<_ = ( le ` K )
dalawlem.j 
|- .\/ = ( join ` K )
dalawlem.m 
|- ./\ = ( meet ` K )
dalawlem.a 
|- A = ( Atoms ` K )
dalawlem2.o 
|- O = ( LPlanes ` K )
Assertion dalawlem14 
|- ( ( ( K e. HL /\ -. ( ( ( P .\/ Q ) .\/ R ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( Q .\/ R ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ P ) ) ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) )

Proof

Step Hyp Ref Expression
1 dalawlem.l 
 |-  .<_ = ( le ` K )
2 dalawlem.j 
 |-  .\/ = ( join ` K )
3 dalawlem.m 
 |-  ./\ = ( meet ` K )
4 dalawlem.a 
 |-  A = ( Atoms ` K )
5 dalawlem2.o 
 |-  O = ( LPlanes ` K )
6 ianor 
 |-  ( -. ( ( ( P .\/ Q ) .\/ R ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( Q .\/ R ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ P ) ) ) <-> ( -. ( ( P .\/ Q ) .\/ R ) e. O \/ -. ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( Q .\/ R ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ P ) ) ) )
7 1 2 3 4 5 dalawlem13 
 |-  ( ( ( K e. HL /\ -. ( ( P .\/ Q ) .\/ R ) e. O /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) )
8 7 3expib 
 |-  ( ( K e. HL /\ -. ( ( P .\/ Q ) .\/ R ) e. O /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) -> ( ( ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) ) )
9 8 3exp 
 |-  ( K e. HL -> ( -. ( ( P .\/ Q ) .\/ R ) e. O -> ( ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) -> ( ( ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) ) ) ) )
10 1 2 3 4 dalawlem10 
 |-  ( ( ( K e. HL /\ -. ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( Q .\/ R ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ P ) ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) )
11 10 3expib 
 |-  ( ( K e. HL /\ -. ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( Q .\/ R ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ P ) ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) -> ( ( ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) ) )
12 11 3exp 
 |-  ( K e. HL -> ( -. ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( Q .\/ R ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ P ) ) -> ( ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) -> ( ( ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) ) ) ) )
13 9 12 jaod 
 |-  ( K e. HL -> ( ( -. ( ( P .\/ Q ) .\/ R ) e. O \/ -. ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( Q .\/ R ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ P ) ) ) -> ( ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) -> ( ( ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) ) ) ) )
14 6 13 syl5bi 
 |-  ( K e. HL -> ( -. ( ( ( P .\/ Q ) .\/ R ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( Q .\/ R ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ P ) ) ) -> ( ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) -> ( ( ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) ) ) ) )
15 14 3imp 
 |-  ( ( K e. HL /\ -. ( ( ( P .\/ Q ) .\/ R ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( Q .\/ R ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ P ) ) ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) -> ( ( ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) ) )
16 15 3impib 
 |-  ( ( ( K e. HL /\ -. ( ( ( P .\/ Q ) .\/ R ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( Q .\/ R ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ P ) ) ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) )