Step |
Hyp |
Ref |
Expression |
1 |
|
paddun.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
2 |
|
paddun.p |
⊢ + = ( +𝑃 ‘ 𝐾 ) |
3 |
|
paddun.o |
⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 ) |
4 |
1 2 3
|
paddunN |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( ⊥ ‘ ( 𝑆 + 𝑇 ) ) = ( ⊥ ‘ ( 𝑆 ∪ 𝑇 ) ) ) |
5 |
|
simp1 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → 𝐾 ∈ HL ) |
6 |
|
unss |
⊢ ( ( 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) ↔ ( 𝑆 ∪ 𝑇 ) ⊆ 𝐴 ) |
7 |
6
|
biimpi |
⊢ ( ( 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( 𝑆 ∪ 𝑇 ) ⊆ 𝐴 ) |
8 |
7
|
3adant1 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( 𝑆 ∪ 𝑇 ) ⊆ 𝐴 ) |
9 |
|
eqid |
⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 ) |
10 |
|
eqid |
⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 ) |
11 |
|
eqid |
⊢ ( pmap ‘ 𝐾 ) = ( pmap ‘ 𝐾 ) |
12 |
9 10 1 11 3
|
polval2N |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∪ 𝑇 ) ⊆ 𝐴 ) → ( ⊥ ‘ ( 𝑆 ∪ 𝑇 ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( 𝑆 ∪ 𝑇 ) ) ) ) ) |
13 |
5 8 12
|
syl2anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( ⊥ ‘ ( 𝑆 ∪ 𝑇 ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( 𝑆 ∪ 𝑇 ) ) ) ) ) |
14 |
|
hlop |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP ) |
15 |
14
|
3ad2ant1 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → 𝐾 ∈ OP ) |
16 |
|
hlclat |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CLat ) |
17 |
16
|
3ad2ant1 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → 𝐾 ∈ CLat ) |
18 |
|
simp2 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → 𝑆 ⊆ 𝐴 ) |
19 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
20 |
19 1
|
atssbase |
⊢ 𝐴 ⊆ ( Base ‘ 𝐾 ) |
21 |
18 20
|
sstrdi |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → 𝑆 ⊆ ( Base ‘ 𝐾 ) ) |
22 |
19 9
|
clatlubcl |
⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ ( Base ‘ 𝐾 ) ) → ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) |
23 |
17 21 22
|
syl2anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) |
24 |
19 10
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ) |
25 |
15 23 24
|
syl2anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ) |
26 |
|
simp3 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → 𝑇 ⊆ 𝐴 ) |
27 |
26 20
|
sstrdi |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → 𝑇 ⊆ ( Base ‘ 𝐾 ) ) |
28 |
19 9
|
clatlubcl |
⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ ( Base ‘ 𝐾 ) ) → ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) |
29 |
17 27 28
|
syl2anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) |
30 |
19 10
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) ) |
31 |
15 29 30
|
syl2anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) ) |
32 |
|
eqid |
⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 ) |
33 |
19 32 1 11
|
pmapmeet |
⊢ ( ( 𝐾 ∈ HL ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) ) = ( ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ) ∩ ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) ) ) |
34 |
5 25 31 33
|
syl3anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) ) = ( ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ) ∩ ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) ) ) |
35 |
|
eqid |
⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 ) |
36 |
19 35 9
|
lubun |
⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ ( Base ‘ 𝐾 ) ∧ 𝑇 ⊆ ( Base ‘ 𝐾 ) ) → ( ( lub ‘ 𝐾 ) ‘ ( 𝑆 ∪ 𝑇 ) ) = ( ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ( join ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) |
37 |
17 21 27 36
|
syl3anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( ( lub ‘ 𝐾 ) ‘ ( 𝑆 ∪ 𝑇 ) ) = ( ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ( join ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) |
38 |
37
|
fveq2d |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( 𝑆 ∪ 𝑇 ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ( join ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) ) |
39 |
|
hlol |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL ) |
40 |
39
|
3ad2ant1 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → 𝐾 ∈ OL ) |
41 |
19 35 32 10
|
oldmj1 |
⊢ ( ( 𝐾 ∈ OL ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ( join ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) ) |
42 |
40 23 29 41
|
syl3anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ( join ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) ) |
43 |
38 42
|
eqtrd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( 𝑆 ∪ 𝑇 ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) ) |
44 |
43
|
fveq2d |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( 𝑆 ∪ 𝑇 ) ) ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) ) ) |
45 |
9 10 1 11 3
|
polval2N |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ) → ( ⊥ ‘ 𝑆 ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ) ) |
46 |
45
|
3adant3 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( ⊥ ‘ 𝑆 ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ) ) |
47 |
9 10 1 11 3
|
polval2N |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴 ) → ( ⊥ ‘ 𝑇 ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) ) |
48 |
47
|
3adant2 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( ⊥ ‘ 𝑇 ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) ) |
49 |
46 48
|
ineq12d |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( ( ⊥ ‘ 𝑆 ) ∩ ( ⊥ ‘ 𝑇 ) ) = ( ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ) ∩ ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) ) ) |
50 |
34 44 49
|
3eqtr4d |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( 𝑆 ∪ 𝑇 ) ) ) ) = ( ( ⊥ ‘ 𝑆 ) ∩ ( ⊥ ‘ 𝑇 ) ) ) |
51 |
4 13 50
|
3eqtrd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( ⊥ ‘ ( 𝑆 + 𝑇 ) ) = ( ( ⊥ ‘ 𝑆 ) ∩ ( ⊥ ‘ 𝑇 ) ) ) |