Proof of Theorem paddunN
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp1 1136 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝐾 ∈ HL) | 
| 2 |  | paddun.a | . . . 4
⊢ 𝐴 = (Atoms‘𝐾) | 
| 3 |  | paddun.p | . . . 4
⊢  + =
(+𝑃‘𝐾) | 
| 4 | 2, 3 | paddssat 39817 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ 𝐴) | 
| 5 | 2, 3 | paddunssN 39811 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ (𝑆 + 𝑇)) | 
| 6 |  | paddun.o | . . . 4
⊢  ⊥ =
(⊥𝑃‘𝐾) | 
| 7 | 2, 6 | polcon3N 39920 | . . 3
⊢ ((𝐾 ∈ HL ∧ (𝑆 + 𝑇) ⊆ 𝐴 ∧ (𝑆 ∪ 𝑇) ⊆ (𝑆 + 𝑇)) → ( ⊥ ‘(𝑆 + 𝑇)) ⊆ ( ⊥ ‘(𝑆 ∪ 𝑇))) | 
| 8 | 1, 4, 5, 7 | syl3anc 1372 | . 2
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) ⊆ ( ⊥ ‘(𝑆 ∪ 𝑇))) | 
| 9 |  | hlclat 39360 | . . . . . . 7
⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat) | 
| 10 | 9 | 3ad2ant1 1133 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝐾 ∈ CLat) | 
| 11 |  | unss 4189 | . . . . . . . . . . 11
⊢ ((𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) ↔ (𝑆 ∪ 𝑇) ⊆ 𝐴) | 
| 12 | 11 | biimpi 216 | . . . . . . . . . 10
⊢ ((𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ 𝐴) | 
| 13 | 12 | 3adant1 1130 | . . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ 𝐴) | 
| 14 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 15 | 14, 2 | atssbase 39292 | . . . . . . . . 9
⊢ 𝐴 ⊆ (Base‘𝐾) | 
| 16 | 13, 15 | sstrdi 3995 | . . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ (Base‘𝐾)) | 
| 17 |  | eqid 2736 | . . . . . . . . 9
⊢
(lub‘𝐾) =
(lub‘𝐾) | 
| 18 | 14, 17 | clatlubcl 18549 | . . . . . . . 8
⊢ ((𝐾 ∈ CLat ∧ (𝑆 ∪ 𝑇) ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) ∈ (Base‘𝐾)) | 
| 19 | 10, 16, 18 | syl2anc 584 | . . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) ∈ (Base‘𝐾)) | 
| 20 |  | eqid 2736 | . . . . . . . 8
⊢
(pmap‘𝐾) =
(pmap‘𝐾) | 
| 21 | 14, 20 | pmapssbaN 39763 | . . . . . . 7
⊢ ((𝐾 ∈ HL ∧
((lub‘𝐾)‘(𝑆 ∪ 𝑇)) ∈ (Base‘𝐾)) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) ⊆ (Base‘𝐾)) | 
| 22 | 1, 19, 21 | syl2anc 584 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) ⊆ (Base‘𝐾)) | 
| 23 | 2, 6 | polssatN 39911 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘𝑆) ⊆ 𝐴) | 
| 24 | 23 | 3adant3 1132 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑆) ⊆ 𝐴) | 
| 25 | 2, 6 | polssatN 39911 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ ( ⊥
‘𝑆) ⊆ 𝐴) → ( ⊥ ‘( ⊥
‘𝑆)) ⊆ 𝐴) | 
| 26 | 1, 24, 25 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥
‘𝑆)) ⊆ 𝐴) | 
| 27 | 2, 6 | polssatN 39911 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑇) ⊆ 𝐴) | 
| 28 | 27 | 3adant2 1131 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑇) ⊆ 𝐴) | 
| 29 | 2, 6 | polssatN 39911 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ ( ⊥
‘𝑇) ⊆ 𝐴) → ( ⊥ ‘( ⊥
‘𝑇)) ⊆ 𝐴) | 
| 30 | 1, 28, 29 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥
‘𝑇)) ⊆ 𝐴) | 
| 31 | 1, 26, 30 | 3jca 1128 | . . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝐾 ∈ HL ∧ ( ⊥ ‘( ⊥
‘𝑆)) ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥
‘𝑇)) ⊆ 𝐴)) | 
| 32 | 2, 6 | 2polssN 39918 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → 𝑆 ⊆ ( ⊥ ‘( ⊥
‘𝑆))) | 
| 33 | 32 | 3adant3 1132 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ ( ⊥ ‘( ⊥
‘𝑆))) | 
| 34 | 2, 6 | 2polssN 39918 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ ( ⊥ ‘( ⊥
‘𝑇))) | 
| 35 | 34 | 3adant2 1131 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ ( ⊥ ‘( ⊥
‘𝑇))) | 
| 36 | 33, 35 | jca 511 | . . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ⊆ ( ⊥ ‘( ⊥
‘𝑆)) ∧ 𝑇 ⊆ ( ⊥ ‘( ⊥
‘𝑇)))) | 
| 37 | 2, 3 | paddss12 39822 | . . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ ( ⊥
‘( ⊥ ‘𝑆)) ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥
‘𝑇)) ⊆ 𝐴) → ((𝑆 ⊆ ( ⊥ ‘( ⊥
‘𝑆)) ∧ 𝑇 ⊆ ( ⊥ ‘( ⊥
‘𝑇))) → (𝑆 + 𝑇) ⊆ (( ⊥ ‘( ⊥
‘𝑆)) + ( ⊥
‘( ⊥ ‘𝑇))))) | 
| 38 | 31, 36, 37 | sylc 65 | . . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ (( ⊥ ‘( ⊥
‘𝑆)) + ( ⊥
‘( ⊥ ‘𝑇)))) | 
| 39 | 17, 2, 20, 6 | 2polvalN 39917 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘( ⊥
‘𝑆)) =
((pmap‘𝐾)‘((lub‘𝐾)‘𝑆))) | 
| 40 | 39 | 3adant3 1132 | . . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥
‘𝑆)) =
((pmap‘𝐾)‘((lub‘𝐾)‘𝑆))) | 
| 41 | 17, 2, 20, 6 | 2polvalN 39917 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥
‘𝑇)) =
((pmap‘𝐾)‘((lub‘𝐾)‘𝑇))) | 
| 42 | 41 | 3adant2 1131 | . . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥
‘𝑇)) =
((pmap‘𝐾)‘((lub‘𝐾)‘𝑇))) | 
| 43 | 40, 42 | oveq12d 7450 | . . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (( ⊥ ‘( ⊥
‘𝑆)) + ( ⊥
‘( ⊥ ‘𝑇))) = (((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)) + ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇)))) | 
| 44 | 38, 43 | sseqtrd 4019 | . . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ (((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)) + ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇)))) | 
| 45 |  | hllat 39365 | . . . . . . . . . 10
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) | 
| 46 | 45 | 3ad2ant1 1133 | . . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝐾 ∈ Lat) | 
| 47 |  | simp2 1137 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ 𝐴) | 
| 48 | 47, 15 | sstrdi 3995 | . . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ (Base‘𝐾)) | 
| 49 | 14, 17 | clatlubcl 18549 | . . . . . . . . . 10
⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑆) ∈ (Base‘𝐾)) | 
| 50 | 10, 48, 49 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘𝑆) ∈ (Base‘𝐾)) | 
| 51 |  | simp3 1138 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ 𝐴) | 
| 52 | 51, 15 | sstrdi 3995 | . . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ (Base‘𝐾)) | 
| 53 | 14, 17 | clatlubcl 18549 | . . . . . . . . . 10
⊢ ((𝐾 ∈ CLat ∧ 𝑇 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑇) ∈ (Base‘𝐾)) | 
| 54 | 10, 52, 53 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘𝑇) ∈ (Base‘𝐾)) | 
| 55 |  | eqid 2736 | . . . . . . . . . 10
⊢
(join‘𝐾) =
(join‘𝐾) | 
| 56 | 14, 55, 20, 3 | pmapjoin 39855 | . . . . . . . . 9
⊢ ((𝐾 ∈ Lat ∧
((lub‘𝐾)‘𝑆) ∈ (Base‘𝐾) ∧ ((lub‘𝐾)‘𝑇) ∈ (Base‘𝐾)) → (((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)) + ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇))) ⊆ ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇)))) | 
| 57 | 46, 50, 54, 56 | syl3anc 1372 | . . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)) + ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇))) ⊆ ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇)))) | 
| 58 | 44, 57 | sstrd 3993 | . . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇)))) | 
| 59 | 14, 55, 17 | lubun 18561 | . . . . . . . . 9
⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ (Base‘𝐾) ∧ 𝑇 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) = (((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))) | 
| 60 | 10, 48, 52, 59 | syl3anc 1372 | . . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) = (((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))) | 
| 61 | 60 | fveq2d 6909 | . . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇)))) | 
| 62 | 58, 61 | sseqtrrd 4020 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) | 
| 63 |  | eqid 2736 | . . . . . . 7
⊢
(le‘𝐾) =
(le‘𝐾) | 
| 64 | 14, 63, 17 | lubss 18559 | . . . . . 6
⊢ ((𝐾 ∈ CLat ∧
((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) ⊆ (Base‘𝐾) ∧ (𝑆 + 𝑇) ⊆ ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) → ((lub‘𝐾)‘(𝑆 + 𝑇))(le‘𝐾)((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))) | 
| 65 | 10, 22, 62, 64 | syl3anc 1372 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 + 𝑇))(le‘𝐾)((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))) | 
| 66 | 4, 15 | sstrdi 3995 | . . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ (Base‘𝐾)) | 
| 67 | 14, 17 | clatlubcl 18549 | . . . . . . 7
⊢ ((𝐾 ∈ CLat ∧ (𝑆 + 𝑇) ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘(𝑆 + 𝑇)) ∈ (Base‘𝐾)) | 
| 68 | 10, 66, 67 | syl2anc 584 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 + 𝑇)) ∈ (Base‘𝐾)) | 
| 69 | 14, 17 | clatlubcl 18549 | . . . . . . 7
⊢ ((𝐾 ∈ CLat ∧
((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) ∈ (Base‘𝐾)) | 
| 70 | 10, 22, 69 | syl2anc 584 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) ∈ (Base‘𝐾)) | 
| 71 | 14, 63, 20 | pmaple 39764 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧
((lub‘𝐾)‘(𝑆 + 𝑇)) ∈ (Base‘𝐾) ∧ ((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) ∈ (Base‘𝐾)) → (((lub‘𝐾)‘(𝑆 + 𝑇))(le‘𝐾)((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) ↔ ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 + 𝑇))) ⊆ ((pmap‘𝐾)‘((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))))) | 
| 72 | 1, 68, 70, 71 | syl3anc 1372 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (((lub‘𝐾)‘(𝑆 + 𝑇))(le‘𝐾)((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) ↔ ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 + 𝑇))) ⊆ ((pmap‘𝐾)‘((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))))) | 
| 73 | 65, 72 | mpbid 232 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 + 𝑇))) ⊆ ((pmap‘𝐾)‘((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))))) | 
| 74 | 17, 2, 20, 6 | 2polvalN 39917 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑆 + 𝑇) ⊆ 𝐴) → ( ⊥ ‘( ⊥
‘(𝑆 + 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 + 𝑇)))) | 
| 75 | 1, 4, 74 | syl2anc 584 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥
‘(𝑆 + 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 + 𝑇)))) | 
| 76 | 17, 2, 20, 6 | 2polvalN 39917 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ (𝑆 ∪ 𝑇) ⊆ 𝐴) → ( ⊥ ‘( ⊥
‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) | 
| 77 | 1, 13, 76 | syl2anc 584 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥
‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) | 
| 78 | 17, 2, 20 | 2pmaplubN 39929 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ (𝑆 ∪ 𝑇) ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) | 
| 79 | 1, 13, 78 | syl2anc 584 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) | 
| 80 | 77, 79 | eqtr4d 2779 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥
‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))))) | 
| 81 | 73, 75, 80 | 3sstr4d 4038 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥
‘(𝑆 + 𝑇))) ⊆ ( ⊥ ‘( ⊥
‘(𝑆 ∪ 𝑇)))) | 
| 82 | 2, 6 | 2polcon4bN 39921 | . . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑆 + 𝑇) ⊆ 𝐴 ∧ (𝑆 ∪ 𝑇) ⊆ 𝐴) → (( ⊥ ‘( ⊥
‘(𝑆 + 𝑇))) ⊆ ( ⊥ ‘( ⊥
‘(𝑆 ∪ 𝑇))) ↔ ( ⊥ ‘(𝑆 ∪ 𝑇)) ⊆ ( ⊥ ‘(𝑆 + 𝑇)))) | 
| 83 | 1, 4, 13, 82 | syl3anc 1372 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (( ⊥ ‘( ⊥
‘(𝑆 + 𝑇))) ⊆ ( ⊥ ‘( ⊥
‘(𝑆 ∪ 𝑇))) ↔ ( ⊥ ‘(𝑆 ∪ 𝑇)) ⊆ ( ⊥ ‘(𝑆 + 𝑇)))) | 
| 84 | 81, 83 | mpbid 232 | . 2
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 ∪ 𝑇)) ⊆ ( ⊥ ‘(𝑆 + 𝑇))) | 
| 85 | 8, 84 | eqssd 4000 | 1
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = ( ⊥ ‘(𝑆 ∪ 𝑇))) |