Metamath Proof Explorer

Theorem paddasslem15

Description: Lemma for paddass . Use elpaddn0 to eliminate y and z from paddasslem14 . (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 paddasslem15 
|- ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) ) -> 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 simpr2r 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) ) -> r e. ( Y .+ Z ) )
6 simpl1 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) ) -> K e. HL )
7 6 hllatd 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) ) -> K e. Lat )
8 simpl22 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) ) -> Y C_ A )
9 simpl23 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) ) -> Z C_ A )
10 simpl3 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) ) -> ( Y =/= (/) /\ Z =/= (/) ) )
11 1 2 3 4 elpaddn0 
 |-  ( ( ( K e. Lat /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) -> ( r e. ( Y .+ Z ) <-> ( r e. A /\ E. y e. Y E. z e. Z r .<_ ( y .\/ z ) ) ) )
12 7 8 9 10 11 syl31anc 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) ) -> ( r e. ( Y .+ Z ) <-> ( r e. A /\ E. y e. Y E. z e. Z r .<_ ( y .\/ z ) ) ) )
13 5 12 mpbid 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) ) -> ( r e. A /\ E. y e. Y E. z e. Z r .<_ ( y .\/ z ) ) )
14 simp11 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) /\ ( r e. A /\ ( y e. Y /\ z e. Z ) /\ r .<_ ( y .\/ z ) ) ) -> K e. HL )
15 simp12 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) /\ ( r e. A /\ ( y e. Y /\ z e. Z ) /\ r .<_ ( y .\/ z ) ) ) -> ( X C_ A /\ Y C_ A /\ Z C_ A ) )
16 simp21 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) /\ ( r e. A /\ ( y e. Y /\ z e. Z ) /\ r .<_ ( y .\/ z ) ) ) -> p e. A )
17 simp31 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) /\ ( r e. A /\ ( y e. Y /\ z e. Z ) /\ r .<_ ( y .\/ z ) ) ) -> r e. A )
18 16 17 jca 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) /\ ( r e. A /\ ( y e. Y /\ z e. Z ) /\ r .<_ ( y .\/ z ) ) ) -> ( p e. A /\ r e. A ) )
19 simp22l 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) /\ ( r e. A /\ ( y e. Y /\ z e. Z ) /\ r .<_ ( y .\/ z ) ) ) -> x e. X )
20 simp32l 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) /\ ( r e. A /\ ( y e. Y /\ z e. Z ) /\ r .<_ ( y .\/ z ) ) ) -> y e. Y )
21 simp32r 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) /\ ( r e. A /\ ( y e. Y /\ z e. Z ) /\ r .<_ ( y .\/ z ) ) ) -> z e. Z )
22 19 20 21 3jca 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) /\ ( r e. A /\ ( y e. Y /\ z e. Z ) /\ r .<_ ( y .\/ z ) ) ) -> ( x e. X /\ y e. Y /\ z e. Z ) )
23 simp23 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) /\ ( r e. A /\ ( y e. Y /\ z e. Z ) /\ r .<_ ( y .\/ z ) ) ) -> p .<_ ( x .\/ r ) )
24 simp33 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) /\ ( r e. A /\ ( y e. Y /\ z e. Z ) /\ r .<_ ( y .\/ z ) ) ) -> r .<_ ( y .\/ z ) )
25 23 24 jca 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) /\ ( r e. A /\ ( y e. Y /\ z e. Z ) /\ r .<_ ( y .\/ z ) ) ) -> ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) )
26 1 2 3 4 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 ) )
27 14 15 18 22 25 26 syl32anc 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) /\ ( r e. A /\ ( y e. Y /\ z e. Z ) /\ r .<_ ( y .\/ z ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) )
28 27 3expia 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) ) -> ( ( r e. A /\ ( y e. Y /\ z e. Z ) /\ r .<_ ( y .\/ z ) ) -> p e. ( ( X .+ Y ) .+ Z ) ) )
29 28 3expd 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) ) -> ( r e. A -> ( ( y e. Y /\ z e. Z ) -> ( r .<_ ( y .\/ z ) -> p e. ( ( X .+ Y ) .+ Z ) ) ) ) )
30 29 imp 
 |-  ( ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) ) /\ r e. A ) -> ( ( y e. Y /\ z e. Z ) -> ( r .<_ ( y .\/ z ) -> p e. ( ( X .+ Y ) .+ Z ) ) ) )
31 30 rexlimdvv 
 |-  ( ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) ) /\ r e. A ) -> ( E. y e. Y E. z e. Z r .<_ ( y .\/ z ) -> p e. ( ( X .+ Y ) .+ Z ) ) )
32 31 expimpd 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) ) -> ( ( r e. A /\ E. y e. Y E. z e. Z r .<_ ( y .\/ z ) ) -> p e. ( ( X .+ Y ) .+ Z ) ) )
33 13 32 mpd 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) )