Metamath Proof Explorer

Theorem paddunN

Description: The closure of the projective sum of two sets of atoms is the same as the closure of their union. (Closure is actually double polarity, which can be trivially inferred from this theorem using fveq2d .) (Contributed by NM, 6-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses paddun.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
paddun.p ⊢ + = ( +𝑃 ‘ 𝐾 )
paddun.o ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
Assertion paddunN ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( ⊥ ‘ ( 𝑆 + 𝑇 ) ) = ( ⊥ ‘ ( 𝑆 ∪ 𝑇 ) ) )

Proof

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