Metamath Proof Explorer

Theorem paddasslem9

Description: Lemma for paddass . Combine paddasslem7 and paddasslem8 . (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 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 ) )

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 simpl1 
 |-  ( ( ( 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 ) ) ) ) -> K e. HL )
6 simpl2 
 |-  ( ( ( 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 ) ) ) ) -> ( X C_ A /\ Y C_ A /\ Z C_ A ) )
7 simpl3l 
 |-  ( ( ( 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. A )
8 simpr31 
 |-  ( ( ( 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 ) ) ) ) -> s e. A )
9 7 8 jca 
 |-  ( ( ( 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. A /\ s e. A ) )
10 simpr1 
 |-  ( ( ( 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 ) ) ) ) -> ( x e. X /\ y e. Y /\ z e. Z ) )
11 simpr32 
 |-  ( ( ( 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 ) ) ) ) -> s .<_ ( x .\/ y ) )
12 simpl3r 
 |-  ( ( ( 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 ) ) ) ) -> r e. A )
13 7 12 8 3jca 
 |-  ( ( ( 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. A /\ r e. A /\ s e. A ) )
14 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 ) ) )
15 ssel2 
 |-  ( ( X C_ A /\ x e. X ) -> x e. A )
16 ssel2 
 |-  ( ( Y C_ A /\ y e. Y ) -> y e. A )
17 ssel2 
 |-  ( ( Z C_ A /\ z e. Z ) -> z e. A )
18 15 16 17 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 ) )
19 14 18 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 ) )
20 19 3ad2antl2 
 |-  ( ( ( 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 ) ) -> ( x e. A /\ y e. A /\ z e. A ) )
21 20 3ad2antr1 
 |-  ( ( ( 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 ) ) ) ) -> ( x e. A /\ y e. A /\ z e. A ) )
22 simpr2l 
 |-  ( ( ( 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 ) ) ) ) -> -. r .<_ ( x .\/ y ) )
23 simpr2r 
 |-  ( ( ( 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 ) ) ) ) -> r .<_ ( y .\/ z ) )
24 22 23 11 3jca 
 |-  ( ( ( 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 ) ) ) ) -> ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) /\ s .<_ ( x .\/ y ) ) )
25 simpr33 
 |-  ( ( ( 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 ) ) ) ) -> s .<_ ( p .\/ z ) )
26 1 2 3 paddasslem7 
 |-  ( ( ( K e. HL /\ ( p e. A /\ r e. A /\ s e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ ( ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) /\ s .<_ ( x .\/ y ) ) /\ s .<_ ( p .\/ z ) ) ) -> p .<_ ( s .\/ z ) )
27 5 13 21 24 25 26 syl32anc 
 |-  ( ( ( 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 .<_ ( s .\/ z ) )
28 1 2 3 4 paddasslem8 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ s e. A ) ) /\ ( ( x e. X /\ y e. Y /\ z e. Z ) /\ s .<_ ( x .\/ y ) /\ p .<_ ( s .\/ z ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) )
29 5 6 9 10 11 27 28 syl33anc 
 |-  ( ( ( 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 ) )