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