Metamath Proof Explorer

Theorem paddasslem14

Description: Lemma for paddass . Remove p =/= z , x =/= y , and -. r .<_ ( x .\/ y ) from antecedent of paddasslem10 , using paddasslem11 , paddasslem12 , and paddasslem13 . (Contributed by NM, 11-Jan-2012)

Ref Expression
Hypotheses paddasslem.l 
|- .<_ = ( le ` K )
paddasslem.j 
|- .\/ = ( join ` K )
paddasslem.a 
|- A = ( Atoms ` K )
paddasslem.p 
|- .+ = ( +P ` K )
Assertion paddasslem14 
|- ( ( ( 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 ) /\ ( 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 1 2 3 4 paddasslem11 
 |-  ( ( ( ( K e. HL /\ p = z ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) /\ z e. Z ) -> p e. ( ( X .+ Y ) .+ Z ) )
6 5 3ad2antr3 
 |-  ( ( ( ( K e. HL /\ p = z ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) /\ ( x e. X /\ y e. Y /\ z e. Z ) ) -> p e. ( ( X .+ Y ) .+ Z ) )
7 6 ex 
 |-  ( ( ( K e. HL /\ p = z ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( x e. X /\ y e. Y /\ z e. Z ) -> p e. ( ( X .+ Y ) .+ Z ) ) )
8 7 adantrd 
 |-  ( ( ( K e. HL /\ p = z ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) ) )
9 8 a1d 
 |-  ( ( ( K e. HL /\ p = z ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( p e. A /\ r e. A ) -> ( ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) ) ) )
10 9 exp31 
 |-  ( K e. HL -> ( p = z -> ( ( X C_ A /\ Y C_ A /\ Z C_ A ) -> ( ( p e. A /\ r e. A ) -> ( ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) ) ) ) ) )
11 3simpb 
 |-  ( ( K e. HL /\ p =/= z /\ x = y ) -> ( K e. HL /\ x = y ) )
12 11 3anim1i 
 |-  ( ( ( K e. HL /\ p =/= z /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) -> ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) )
13 3simpc 
 |-  ( ( x e. X /\ y e. Y /\ z e. Z ) -> ( y e. Y /\ z e. Z ) )
14 13 anim1i 
 |-  ( ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) )
15 1 2 3 4 paddasslem12 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) )
16 12 14 15 syl2an 
 |-  ( ( ( ( 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 ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) )
17 16 3exp1 
 |-  ( ( 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 ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) ) ) ) )
18 17 3expia 
 |-  ( ( 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 ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) ) ) ) ) )
19 3simpa 
 |-  ( ( K e. HL /\ p =/= z /\ x =/= y ) -> ( K e. HL /\ p =/= z ) )
20 19 3anim1i 
 |-  ( ( ( K e. HL /\ p =/= z /\ x =/= y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) -> ( ( K e. HL /\ p =/= z ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) )
21 3simpa 
 |-  ( ( x e. X /\ y e. Y /\ z e. Z ) -> ( x e. X /\ y e. Y ) )
22 3simpa 
 |-  ( ( r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) -> ( r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) ) )
23 21 22 anim12i 
 |-  ( ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> ( ( x e. X /\ y e. Y ) /\ ( r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) ) ) )
24 1 2 3 4 paddasslem13 
 |-  ( ( ( ( K e. HL /\ p =/= z ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( x e. X /\ y e. Y ) /\ ( r .<_ ( x .\/ y ) /\ p .<_ ( x .\/ r ) ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) )
25 20 23 24 syl2an 
 |-  ( ( ( ( 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 ) )
26 25 expr 
 |-  ( ( ( ( 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 ) ) )
27 26 3expd 
 |-  ( ( ( ( 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 ) ) ) ) )
28 1 2 3 4 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 ) )
29 28 expr 
 |-  ( ( ( ( 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 ) ) )
30 29 3expd 
 |-  ( ( ( ( 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 ) ) ) ) )
31 27 30 pm2.61d 
 |-  ( ( ( ( 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 ) ) -> ( p .<_ ( x .\/ r ) -> ( r .<_ ( y .\/ z ) -> p e. ( ( X .+ Y ) .+ Z ) ) ) )
32 31 impd 
 |-  ( ( ( ( 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 ) ) -> ( ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) -> p e. ( ( X .+ Y ) .+ Z ) ) )
33 32 expimpd 
 |-  ( ( ( 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 ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) ) )
34 33 3exp 
 |-  ( ( 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 ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) ) ) ) )
35 34 3expia 
 |-  ( ( 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 ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) ) ) ) ) )
36 18 35 pm2.61dne 
 |-  ( ( K e. HL /\ p =/= z ) -> ( ( X C_ A /\ Y C_ A /\ Z C_ A ) -> ( ( p e. A /\ r e. A ) -> ( ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) ) ) ) )
37 36 ex 
 |-  ( K e. HL -> ( p =/= z -> ( ( X C_ A /\ Y C_ A /\ Z C_ A ) -> ( ( p e. A /\ r e. A ) -> ( ( ( x e. X /\ y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) ) ) ) ) )
38 10 37 pm2.61dne 
 |-  ( 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 ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) ) ) ) )
39 38 3imp1 
 |-  ( ( ( 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 ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) )