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 ) )