Metamath Proof Explorer

Theorem dalawlem13

Description: Lemma for dalaw . Special case to eliminate the requirement ( ( P .\/ Q ) .\/ R ) e. O in dalawlem1 . (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 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 ) ) ) )

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 simp11 
 |-  ( ( ( 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 ) ) -> K e. HL )
7 simp12 
 |-  ( ( ( 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 ) .\/ R ) e. O )
8 simp22 
 |-  ( ( ( 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 ) ) -> Q e. A )
9 simp23 
 |-  ( ( ( 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 ) ) -> R e. A )
10 simp21 
 |-  ( ( ( 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 e. A )
11 1 2 4 5 islpln2a 
 |-  ( ( K e. HL /\ ( Q e. A /\ R e. A /\ P e. A ) ) -> ( ( ( Q .\/ R ) .\/ P ) e. O <-> ( Q =/= R /\ -. P .<_ ( Q .\/ R ) ) ) )
12 6 8 9 10 11 syl13anc 
 |-  ( ( ( 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 ) ) -> ( ( ( Q .\/ R ) .\/ P ) e. O <-> ( Q =/= R /\ -. P .<_ ( Q .\/ R ) ) ) )
13 df-ne 
 |-  ( Q =/= R <-> -. Q = R )
14 13 anbi1i 
 |-  ( ( Q =/= R /\ -. P .<_ ( Q .\/ R ) ) <-> ( -. Q = R /\ -. P .<_ ( Q .\/ R ) ) )
15 pm4.56 
 |-  ( ( -. Q = R /\ -. P .<_ ( Q .\/ R ) ) <-> -. ( Q = R \/ P .<_ ( Q .\/ R ) ) )
16 14 15 bitri 
 |-  ( ( Q =/= R /\ -. P .<_ ( Q .\/ R ) ) <-> -. ( Q = R \/ P .<_ ( Q .\/ R ) ) )
17 12 16 bitr2di 
 |-  ( ( ( 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 ) ) -> ( -. ( Q = R \/ P .<_ ( Q .\/ R ) ) <-> ( ( Q .\/ R ) .\/ P ) e. O ) )
18 2 4 hlatjrot 
 |-  ( ( K e. HL /\ ( Q e. A /\ R e. A /\ P e. A ) ) -> ( ( Q .\/ R ) .\/ P ) = ( ( P .\/ Q ) .\/ R ) )
19 6 8 9 10 18 syl13anc 
 |-  ( ( ( 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 ) ) -> ( ( Q .\/ R ) .\/ P ) = ( ( P .\/ Q ) .\/ R ) )
20 19 eleq1d 
 |-  ( ( ( 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 ) ) -> ( ( ( Q .\/ R ) .\/ P ) e. O <-> ( ( P .\/ Q ) .\/ R ) e. O ) )
21 17 20 bitrd 
 |-  ( ( ( 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 ) ) -> ( -. ( Q = R \/ P .<_ ( Q .\/ R ) ) <-> ( ( P .\/ Q ) .\/ R ) e. O ) )
22 21 con1bid 
 |-  ( ( ( 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 ) .\/ R ) e. O <-> ( Q = R \/ P .<_ ( Q .\/ R ) ) ) )
23 7 22 mpbid 
 |-  ( ( ( 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 ) ) -> ( Q = R \/ P .<_ ( Q .\/ R ) ) )
24 simp13 
 |-  ( ( ( 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 .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) )
25 simp2 
 |-  ( ( ( 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 e. A /\ Q e. A /\ R e. A ) )
26 simp3 
 |-  ( ( ( 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 ) ) -> ( S e. A /\ T e. A /\ U e. A ) )
27 1 2 3 4 dalawlem12 
 |-  ( ( ( K e. HL /\ Q = R /\ ( ( 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 ) ) ) )
28 27 3expib 
 |-  ( ( K e. HL /\ Q = R /\ ( ( 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 ) ) ) ) )
29 28 3exp 
 |-  ( K e. HL -> ( Q = R -> ( ( ( 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 ) ) ) ) ) ) )
30 1 2 3 4 dalawlem11 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( 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 ) ) ) )
31 30 3expib 
 |-  ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( 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 ) ) ) ) )
32 31 3exp 
 |-  ( K e. HL -> ( P .<_ ( Q .\/ R ) -> ( ( ( 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 ) ) ) ) ) ) )
33 29 32 jaod 
 |-  ( K e. HL -> ( ( Q = R \/ P .<_ ( Q .\/ R ) ) -> ( ( ( 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 ) ) ) ) ) ) )
34 33 3imp 
 |-  ( ( K e. HL /\ ( Q = R \/ P .<_ ( Q .\/ R ) ) /\ ( ( 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 ) ) ) ) )
35 34 3impib 
 |-  ( ( ( K e. HL /\ ( Q = R \/ P .<_ ( Q .\/ R ) ) /\ ( ( 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 ) ) ) )
36 6 23 24 25 26 35 syl311anc 
 |-  ( ( ( 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 ) ) ) )