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 |
|
simpl1l |
|- ( ( ( ( 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 ) ) ) ) -> K e. HL ) |
6 |
|
simpl21 |
|- ( ( ( ( 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 ) ) ) ) -> X C_ A ) |
7 |
|
simpl22 |
|- ( ( ( ( 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 ) ) ) ) -> Y C_ A ) |
8 |
3 4
|
paddssat |
|- ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) C_ A ) |
9 |
5 6 7 8
|
syl3anc |
|- ( ( ( ( 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 ) ) ) ) -> ( X .+ Y ) C_ A ) |
10 |
|
simpl23 |
|- ( ( ( ( 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 ) ) ) ) -> Z C_ A ) |
11 |
3 4
|
sspadd1 |
|- ( ( K e. HL /\ ( X .+ Y ) C_ A /\ Z C_ A ) -> ( X .+ Y ) C_ ( ( X .+ Y ) .+ Z ) ) |
12 |
5 9 10 11
|
syl3anc |
|- ( ( ( ( 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 ) ) ) ) -> ( X .+ Y ) C_ ( ( X .+ Y ) .+ Z ) ) |
13 |
5
|
hllatd |
|- ( ( ( ( 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 ) ) ) ) -> K e. Lat ) |
14 |
|
simprll |
|- ( ( ( ( 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 ) ) ) ) -> x e. X ) |
15 |
|
simprlr |
|- ( ( ( ( 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 ) ) ) ) -> y e. Y ) |
16 |
|
simpl3l |
|- ( ( ( ( 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. A ) |
17 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
18 |
17 3
|
atbase |
|- ( p e. A -> p e. ( Base ` K ) ) |
19 |
16 18
|
syl |
|- ( ( ( ( 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. ( Base ` K ) ) |
20 |
6 14
|
sseldd |
|- ( ( ( ( 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 ) ) ) ) -> x e. A ) |
21 |
17 3
|
atbase |
|- ( x e. A -> x e. ( Base ` K ) ) |
22 |
20 21
|
syl |
|- ( ( ( ( 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 ) ) ) ) -> x e. ( Base ` K ) ) |
23 |
|
simpl3r |
|- ( ( ( ( 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 ) ) ) ) -> r e. A ) |
24 |
17 3
|
atbase |
|- ( r e. A -> r e. ( Base ` K ) ) |
25 |
23 24
|
syl |
|- ( ( ( ( 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 ) ) ) ) -> r e. ( Base ` K ) ) |
26 |
17 2
|
latjcl |
|- ( ( K e. Lat /\ x e. ( Base ` K ) /\ r e. ( Base ` K ) ) -> ( x .\/ r ) e. ( Base ` K ) ) |
27 |
13 22 25 26
|
syl3anc |
|- ( ( ( ( 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 ) ) ) ) -> ( x .\/ r ) e. ( Base ` K ) ) |
28 |
7 15
|
sseldd |
|- ( ( ( ( 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 ) ) ) ) -> y e. A ) |
29 |
17 3
|
atbase |
|- ( y e. A -> y e. ( Base ` K ) ) |
30 |
28 29
|
syl |
|- ( ( ( ( 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 ) ) ) ) -> y e. ( Base ` K ) ) |
31 |
17 2
|
latjcl |
|- ( ( K e. Lat /\ x e. ( Base ` K ) /\ y e. ( Base ` K ) ) -> ( x .\/ y ) e. ( Base ` K ) ) |
32 |
13 22 30 31
|
syl3anc |
|- ( ( ( ( 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 ) ) ) ) -> ( x .\/ y ) e. ( Base ` K ) ) |
33 |
|
simprrr |
|- ( ( ( ( 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 .<_ ( x .\/ r ) ) |
34 |
17 1 2
|
latlej1 |
|- ( ( K e. Lat /\ x e. ( Base ` K ) /\ y e. ( Base ` K ) ) -> x .<_ ( x .\/ y ) ) |
35 |
13 22 30 34
|
syl3anc |
|- ( ( ( ( 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 ) ) ) ) -> x .<_ ( x .\/ y ) ) |
36 |
|
simprrl |
|- ( ( ( ( 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 ) ) ) ) -> r .<_ ( x .\/ y ) ) |
37 |
17 1 2
|
latjle12 |
|- ( ( K e. Lat /\ ( x e. ( Base ` K ) /\ r e. ( Base ` K ) /\ ( x .\/ y ) e. ( Base ` K ) ) ) -> ( ( x .<_ ( x .\/ y ) /\ r .<_ ( x .\/ y ) ) <-> ( x .\/ r ) .<_ ( x .\/ y ) ) ) |
38 |
13 22 25 32 37
|
syl13anc |
|- ( ( ( ( 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 ) ) ) ) -> ( ( x .<_ ( x .\/ y ) /\ r .<_ ( x .\/ y ) ) <-> ( x .\/ r ) .<_ ( x .\/ y ) ) ) |
39 |
35 36 38
|
mpbi2and |
|- ( ( ( ( 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 ) ) ) ) -> ( x .\/ r ) .<_ ( x .\/ y ) ) |
40 |
17 1 13 19 27 32 33 39
|
lattrd |
|- ( ( ( ( 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 .<_ ( x .\/ y ) ) |
41 |
1 2 3 4
|
elpaddri |
|- ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( x e. X /\ y e. Y ) /\ ( p e. A /\ p .<_ ( x .\/ y ) ) ) -> p e. ( X .+ Y ) ) |
42 |
13 6 7 14 15 16 40 41
|
syl322anc |
|- ( ( ( ( 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 ) ) |
43 |
12 42
|
sseldd |
|- ( ( ( ( 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 ) ) |