Metamath Proof Explorer

Theorem paddasslem10

Description: Lemma for paddass . Use paddasslem4 to eliminate s from paddasslem9 . (Contributed by NM, 9-Jan-2012)

Ref Expression
Hypotheses paddasslem.l 
|- .<_ = ( le ` K )
paddasslem.j 
|- .\/ = ( join ` K )
paddasslem.a 
|- A = ( Atoms ` K )
paddasslem.p 
|- .+ = ( +P ` K )
Assertion paddasslem10 
|- ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) )

Proof

Step Hyp Ref Expression
1 paddasslem.l 
 |-  .<_ = ( le ` K )
2 paddasslem.j 
 |-  .\/ = ( join ` K )
3 paddasslem.a 
 |-  A = ( Atoms ` K )
4 paddasslem.p 
 |-  .+ = ( +P ` K )
5 simpl11 
 |-  ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> K e. HL )
6 simpl3l 
 |-  ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> p e. A )
7 simpl3r 
 |-  ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> r e. A )
8 5 6 7 3jca 
 |-  ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> ( K e. HL /\ p e. A /\ r e. A ) )
9 an6 
 |-  ( ( ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( x e. X /\ y e. Y /\ z e. Z ) ) <-> ( ( X C_ A /\ x e. X ) /\ ( Y C_ A /\ y e. Y ) /\ ( Z C_ A /\ z e. Z ) ) )
10 ssel2 
 |-  ( ( X C_ A /\ x e. X ) -> x e. A )
11 ssel2 
 |-  ( ( Y C_ A /\ y e. Y ) -> y e. A )
12 ssel2 
 |-  ( ( Z C_ A /\ z e. Z ) -> z e. A )
13 10 11 12 3anim123i 
 |-  ( ( ( X C_ A /\ x e. X ) /\ ( Y C_ A /\ y e. Y ) /\ ( Z C_ A /\ z e. Z ) ) -> ( x e. A /\ y e. A /\ z e. A ) )
14 9 13 sylbi 
 |-  ( ( ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( x e. X /\ y e. Y /\ z e. Z ) ) -> ( x e. A /\ y e. A /\ z e. A ) )
15 14 3ad2antl2 
 |-  ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( x e. X /\ y e. Y /\ z e. Z ) ) -> ( x e. A /\ y e. A /\ z e. A ) )
16 15 adantrr 
 |-  ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> ( x e. A /\ y e. A /\ z e. A ) )
17 simpl12 
 |-  ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> p =/= z )
18 simpl13 
 |-  ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> x =/= y )
19 simprr1 
 |-  ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> -. r .<_ ( x .\/ y ) )
20 17 18 19 3jca 
 |-  ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> ( p =/= z /\ x =/= y /\ -. r .<_ ( x .\/ y ) ) )
21 simprr2 
 |-  ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> p .<_ ( x .\/ r ) )
22 simprr3 
 |-  ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> r .<_ ( y .\/ z ) )
23 1 2 3 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 ) ) )
24 8 16 20 21 22 23 syl32anc 
 |-  ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> E. s e. A ( s .<_ ( x .\/ y ) /\ s .<_ ( p .\/ z ) ) )
25 simpl2 
 |-  ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> ( X C_ A /\ Y C_ A /\ Z C_ A ) )
26 simpl3 
 |-  ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> ( p e. A /\ r e. A ) )
27 5 25 26 3jca 
 |-  ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) )
28 27 adantr 
 |-  ( ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) /\ ( s e. A /\ ( s .<_ ( x .\/ y ) /\ s .<_ ( p .\/ z ) ) ) ) -> ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) )
29 simplrl 
 |-  ( ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) /\ ( s e. A /\ ( s .<_ ( x .\/ y ) /\ s .<_ ( p .\/ z ) ) ) ) -> ( x e. X /\ y e. Y /\ z e. Z ) )
30 19 22 jca 
 |-  ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) ) )
31 30 adantr 
 |-  ( ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) /\ ( s e. A /\ ( s .<_ ( x .\/ y ) /\ s .<_ ( p .\/ z ) ) ) ) -> ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) ) )
32 simprl 
 |-  ( ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) /\ ( s e. A /\ ( s .<_ ( x .\/ y ) /\ s .<_ ( p .\/ z ) ) ) ) -> s e. A )
33 simprrl 
 |-  ( ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) /\ ( s e. A /\ ( s .<_ ( x .\/ y ) /\ s .<_ ( p .\/ z ) ) ) ) -> s .<_ ( x .\/ y ) )
34 simprrr 
 |-  ( ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) /\ ( s e. A /\ ( s .<_ ( x .\/ y ) /\ s .<_ ( p .\/ z ) ) ) ) -> s .<_ ( p .\/ z ) )
35 32 33 34 3jca 
 |-  ( ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) /\ ( s e. A /\ ( s .<_ ( x .\/ y ) /\ s .<_ ( p .\/ z ) ) ) ) -> ( s e. A /\ s .<_ ( x .\/ y ) /\ s .<_ ( p .\/ z ) ) )
36 1 2 3 4 paddasslem9 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) ) /\ ( s e. A /\ s .<_ ( x .\/ y ) /\ s .<_ ( p .\/ z ) ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) )
37 28 29 31 35 36 syl13anc 
 |-  ( ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) /\ ( s e. A /\ ( s .<_ ( x .\/ y ) /\ s .<_ ( p .\/ z ) ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) )
38 24 37 rexlimddv 
 |-  ( ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( -. r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) )