Step |
Hyp |
Ref |
Expression |
1 |
|
paddun.a |
|- A = ( Atoms ` K ) |
2 |
|
paddun.p |
|- .+ = ( +P ` K ) |
3 |
|
paddun.o |
|- ._|_ = ( _|_P ` K ) |
4 |
|
simp1 |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> K e. HL ) |
5 |
1 2
|
paddssat |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S .+ T ) C_ A ) |
6 |
1 2
|
paddunssN |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S u. T ) C_ ( S .+ T ) ) |
7 |
1 3
|
polcon3N |
|- ( ( K e. HL /\ ( S .+ T ) C_ A /\ ( S u. T ) C_ ( S .+ T ) ) -> ( ._|_ ` ( S .+ T ) ) C_ ( ._|_ ` ( S u. T ) ) ) |
8 |
4 5 6 7
|
syl3anc |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( S .+ T ) ) C_ ( ._|_ ` ( S u. T ) ) ) |
9 |
|
hlclat |
|- ( K e. HL -> K e. CLat ) |
10 |
9
|
3ad2ant1 |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> K e. CLat ) |
11 |
|
unss |
|- ( ( S C_ A /\ T C_ A ) <-> ( S u. T ) C_ A ) |
12 |
11
|
biimpi |
|- ( ( S C_ A /\ T C_ A ) -> ( S u. T ) C_ A ) |
13 |
12
|
3adant1 |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S u. T ) C_ A ) |
14 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
15 |
14 1
|
atssbase |
|- A C_ ( Base ` K ) |
16 |
13 15
|
sstrdi |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S u. T ) C_ ( Base ` K ) ) |
17 |
|
eqid |
|- ( lub ` K ) = ( lub ` K ) |
18 |
14 17
|
clatlubcl |
|- ( ( K e. CLat /\ ( S u. T ) C_ ( Base ` K ) ) -> ( ( lub ` K ) ` ( S u. T ) ) e. ( Base ` K ) ) |
19 |
10 16 18
|
syl2anc |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` ( S u. T ) ) e. ( Base ` K ) ) |
20 |
|
eqid |
|- ( pmap ` K ) = ( pmap ` K ) |
21 |
14 20
|
pmapssbaN |
|- ( ( K e. HL /\ ( ( lub ` K ) ` ( S u. T ) ) e. ( Base ` K ) ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) C_ ( Base ` K ) ) |
22 |
4 19 21
|
syl2anc |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) C_ ( Base ` K ) ) |
23 |
1 3
|
polssatN |
|- ( ( K e. HL /\ S C_ A ) -> ( ._|_ ` S ) C_ A ) |
24 |
23
|
3adant3 |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` S ) C_ A ) |
25 |
1 3
|
polssatN |
|- ( ( K e. HL /\ ( ._|_ ` S ) C_ A ) -> ( ._|_ ` ( ._|_ ` S ) ) C_ A ) |
26 |
4 24 25
|
syl2anc |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` S ) ) C_ A ) |
27 |
1 3
|
polssatN |
|- ( ( K e. HL /\ T C_ A ) -> ( ._|_ ` T ) C_ A ) |
28 |
27
|
3adant2 |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` T ) C_ A ) |
29 |
1 3
|
polssatN |
|- ( ( K e. HL /\ ( ._|_ ` T ) C_ A ) -> ( ._|_ ` ( ._|_ ` T ) ) C_ A ) |
30 |
4 28 29
|
syl2anc |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` T ) ) C_ A ) |
31 |
4 26 30
|
3jca |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( K e. HL /\ ( ._|_ ` ( ._|_ ` S ) ) C_ A /\ ( ._|_ ` ( ._|_ ` T ) ) C_ A ) ) |
32 |
1 3
|
2polssN |
|- ( ( K e. HL /\ S C_ A ) -> S C_ ( ._|_ ` ( ._|_ ` S ) ) ) |
33 |
32
|
3adant3 |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> S C_ ( ._|_ ` ( ._|_ ` S ) ) ) |
34 |
1 3
|
2polssN |
|- ( ( K e. HL /\ T C_ A ) -> T C_ ( ._|_ ` ( ._|_ ` T ) ) ) |
35 |
34
|
3adant2 |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> T C_ ( ._|_ ` ( ._|_ ` T ) ) ) |
36 |
33 35
|
jca |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S C_ ( ._|_ ` ( ._|_ ` S ) ) /\ T C_ ( ._|_ ` ( ._|_ ` T ) ) ) ) |
37 |
1 2
|
paddss12 |
|- ( ( K e. HL /\ ( ._|_ ` ( ._|_ ` S ) ) C_ A /\ ( ._|_ ` ( ._|_ ` T ) ) C_ A ) -> ( ( S C_ ( ._|_ ` ( ._|_ ` S ) ) /\ T C_ ( ._|_ ` ( ._|_ ` T ) ) ) -> ( S .+ T ) C_ ( ( ._|_ ` ( ._|_ ` S ) ) .+ ( ._|_ ` ( ._|_ ` T ) ) ) ) ) |
38 |
31 36 37
|
sylc |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S .+ T ) C_ ( ( ._|_ ` ( ._|_ ` S ) ) .+ ( ._|_ ` ( ._|_ ` T ) ) ) ) |
39 |
17 1 20 3
|
2polvalN |
|- ( ( K e. HL /\ S C_ A ) -> ( ._|_ ` ( ._|_ ` S ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) ) |
40 |
39
|
3adant3 |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` S ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) ) |
41 |
17 1 20 3
|
2polvalN |
|- ( ( K e. HL /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` T ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` T ) ) ) |
42 |
41
|
3adant2 |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` T ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` T ) ) ) |
43 |
40 42
|
oveq12d |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( ._|_ ` ( ._|_ ` S ) ) .+ ( ._|_ ` ( ._|_ ` T ) ) ) = ( ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) .+ ( ( pmap ` K ) ` ( ( lub ` K ) ` T ) ) ) ) |
44 |
38 43
|
sseqtrd |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S .+ T ) C_ ( ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) .+ ( ( pmap ` K ) ` ( ( lub ` K ) ` T ) ) ) ) |
45 |
|
hllat |
|- ( K e. HL -> K e. Lat ) |
46 |
45
|
3ad2ant1 |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> K e. Lat ) |
47 |
|
simp2 |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> S C_ A ) |
48 |
47 15
|
sstrdi |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> S C_ ( Base ` K ) ) |
49 |
14 17
|
clatlubcl |
|- ( ( K e. CLat /\ S C_ ( Base ` K ) ) -> ( ( lub ` K ) ` S ) e. ( Base ` K ) ) |
50 |
10 48 49
|
syl2anc |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` S ) e. ( Base ` K ) ) |
51 |
|
simp3 |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> T C_ A ) |
52 |
51 15
|
sstrdi |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> T C_ ( Base ` K ) ) |
53 |
14 17
|
clatlubcl |
|- ( ( K e. CLat /\ T C_ ( Base ` K ) ) -> ( ( lub ` K ) ` T ) e. ( Base ` K ) ) |
54 |
10 52 53
|
syl2anc |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` T ) e. ( Base ` K ) ) |
55 |
|
eqid |
|- ( join ` K ) = ( join ` K ) |
56 |
14 55 20 2
|
pmapjoin |
|- ( ( K e. Lat /\ ( ( lub ` K ) ` S ) e. ( Base ` K ) /\ ( ( lub ` K ) ` T ) e. ( Base ` K ) ) -> ( ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) .+ ( ( pmap ` K ) ` ( ( lub ` K ) ` T ) ) ) C_ ( ( pmap ` K ) ` ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) ) ) |
57 |
46 50 54 56
|
syl3anc |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) .+ ( ( pmap ` K ) ` ( ( lub ` K ) ` T ) ) ) C_ ( ( pmap ` K ) ` ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) ) ) |
58 |
44 57
|
sstrd |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S .+ T ) C_ ( ( pmap ` K ) ` ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) ) ) |
59 |
14 55 17
|
lubun |
|- ( ( K e. CLat /\ S C_ ( Base ` K ) /\ T C_ ( Base ` K ) ) -> ( ( lub ` K ) ` ( S u. T ) ) = ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) ) |
60 |
10 48 52 59
|
syl3anc |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` ( S u. T ) ) = ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) ) |
61 |
60
|
fveq2d |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) = ( ( pmap ` K ) ` ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) ) ) |
62 |
58 61
|
sseqtrrd |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S .+ T ) C_ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) |
63 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
64 |
14 63 17
|
lubss |
|- ( ( K e. CLat /\ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) C_ ( Base ` K ) /\ ( S .+ T ) C_ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) -> ( ( lub ` K ) ` ( S .+ T ) ) ( le ` K ) ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) |
65 |
10 22 62 64
|
syl3anc |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` ( S .+ T ) ) ( le ` K ) ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) |
66 |
5 15
|
sstrdi |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S .+ T ) C_ ( Base ` K ) ) |
67 |
14 17
|
clatlubcl |
|- ( ( K e. CLat /\ ( S .+ T ) C_ ( Base ` K ) ) -> ( ( lub ` K ) ` ( S .+ T ) ) e. ( Base ` K ) ) |
68 |
10 66 67
|
syl2anc |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` ( S .+ T ) ) e. ( Base ` K ) ) |
69 |
14 17
|
clatlubcl |
|- ( ( K e. CLat /\ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) C_ ( Base ` K ) ) -> ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) e. ( Base ` K ) ) |
70 |
10 22 69
|
syl2anc |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) e. ( Base ` K ) ) |
71 |
14 63 20
|
pmaple |
|- ( ( K e. HL /\ ( ( lub ` K ) ` ( S .+ T ) ) e. ( Base ` K ) /\ ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) e. ( Base ` K ) ) -> ( ( ( lub ` K ) ` ( S .+ T ) ) ( le ` K ) ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) <-> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S .+ T ) ) ) C_ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) ) ) |
72 |
4 68 70 71
|
syl3anc |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( ( lub ` K ) ` ( S .+ T ) ) ( le ` K ) ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) <-> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S .+ T ) ) ) C_ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) ) ) |
73 |
65 72
|
mpbid |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S .+ T ) ) ) C_ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) ) |
74 |
17 1 20 3
|
2polvalN |
|- ( ( K e. HL /\ ( S .+ T ) C_ A ) -> ( ._|_ ` ( ._|_ ` ( S .+ T ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S .+ T ) ) ) ) |
75 |
4 5 74
|
syl2anc |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` ( S .+ T ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S .+ T ) ) ) ) |
76 |
17 1 20 3
|
2polvalN |
|- ( ( K e. HL /\ ( S u. T ) C_ A ) -> ( ._|_ ` ( ._|_ ` ( S u. T ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) |
77 |
4 13 76
|
syl2anc |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` ( S u. T ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) |
78 |
17 1 20
|
2pmaplubN |
|- ( ( K e. HL /\ ( S u. T ) C_ A ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) |
79 |
4 13 78
|
syl2anc |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) |
80 |
77 79
|
eqtr4d |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` ( S u. T ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) ) |
81 |
73 75 80
|
3sstr4d |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` ( S .+ T ) ) ) C_ ( ._|_ ` ( ._|_ ` ( S u. T ) ) ) ) |
82 |
1 3
|
2polcon4bN |
|- ( ( K e. HL /\ ( S .+ T ) C_ A /\ ( S u. T ) C_ A ) -> ( ( ._|_ ` ( ._|_ ` ( S .+ T ) ) ) C_ ( ._|_ ` ( ._|_ ` ( S u. T ) ) ) <-> ( ._|_ ` ( S u. T ) ) C_ ( ._|_ ` ( S .+ T ) ) ) ) |
83 |
4 5 13 82
|
syl3anc |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( ._|_ ` ( ._|_ ` ( S .+ T ) ) ) C_ ( ._|_ ` ( ._|_ ` ( S u. T ) ) ) <-> ( ._|_ ` ( S u. T ) ) C_ ( ._|_ ` ( S .+ T ) ) ) ) |
84 |
81 83
|
mpbid |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( S u. T ) ) C_ ( ._|_ ` ( S .+ T ) ) ) |
85 |
8 84
|
eqssd |
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( S .+ T ) ) = ( ._|_ ` ( S u. T ) ) ) |