Metamath Proof Explorer

Theorem paddasslem4

Description: Lemma for paddass . Combine paddasslem1 , paddasslem2 , and paddasslem3 . (Contributed by NM, 8-Jan-2012)

Ref Expression
Hypotheses paddasslem.l 
|- .<_ = ( le ` K )
paddasslem.j 
|- .\/ = ( join ` K )
paddasslem.a 
|- A = ( Atoms ` K )
Assertion paddasslem4 
|- ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> E. s e. A ( s .<_ ( x .\/ y ) /\ s .<_ ( p .\/ z ) ) )

Proof

Step Hyp Ref Expression
1 paddasslem.l 
 |-  .<_ = ( le ` K )
2 paddasslem.j 
 |-  .\/ = ( join ` K )
3 paddasslem.a 
 |-  A = ( Atoms ` K )
4 simpl11 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> K e. HL )
5 simpl21 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> x e. A )
6 simpl13 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> r e. A )
7 simpl22 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> y e. A )
8 5 6 7 3jca 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> ( x e. A /\ r e. A /\ y e. A ) )
9 simpl12 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> p e. A )
10 simpl23 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> z e. A )
11 9 10 jca 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> ( p e. A /\ z e. A ) )
12 4 8 11 3jca 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> ( K e. HL /\ ( x e. A /\ r e. A /\ y e. A ) /\ ( p e. A /\ z e. A ) ) )
13 simpl32 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> x =/= y )
14 simpl33 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> -. r .<_ ( x .\/ y ) )
15 1 2 3 paddasslem1 
 |-  ( ( ( K e. HL /\ ( x e. A /\ r e. A /\ y e. A ) /\ x =/= y ) /\ -. r .<_ ( x .\/ y ) ) -> -. x .<_ ( r .\/ y ) )
16 4 8 13 14 15 syl31anc 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> -. x .<_ ( r .\/ y ) )
17 simpl31 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> p =/= z )
18 simprl 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> p .<_ ( x .\/ r ) )
19 simpl2 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> ( x e. A /\ y e. A /\ z e. A ) )
20 simprr 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> r .<_ ( y .\/ z ) )
21 1 2 3 paddasslem2 
 |-  ( ( ( K e. HL /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) ) ) -> z .<_ ( r .\/ y ) )
22 4 6 19 14 20 21 syl212anc 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> z .<_ ( r .\/ y ) )
23 18 22 jca 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> ( p .<_ ( x .\/ r ) /\ z .<_ ( r .\/ y ) ) )
24 16 17 23 jca31 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> ( ( -. x .<_ ( r .\/ y ) /\ p =/= z ) /\ ( p .<_ ( x .\/ r ) /\ z .<_ ( r .\/ y ) ) ) )
25 1 2 3 paddasslem3 
 |-  ( ( K e. HL /\ ( x e. A /\ r e. A /\ y e. A ) /\ ( p e. A /\ z e. A ) ) -> ( ( ( -. x .<_ ( r .\/ y ) /\ p =/= z ) /\ ( p .<_ ( x .\/ r ) /\ z .<_ ( r .\/ y ) ) ) -> E. s e. A ( s .<_ ( x .\/ y ) /\ s .<_ ( p .\/ z ) ) ) )
26 12 24 25 sylc 
 |-  ( ( ( ( K e. HL /\ p e. A /\ r e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) /\ ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> E. s e. A ( s .<_ ( x .\/ y ) /\ s .<_ ( p .\/ z ) ) )