Proof of Theorem poldmj1N
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | paddun.a | . . 3
⊢ 𝐴 = (Atoms‘𝐾) | 
| 2 |  | paddun.p | . . 3
⊢  + =
(+𝑃‘𝐾) | 
| 3 |  | paddun.o | . . 3
⊢  ⊥ =
(⊥𝑃‘𝐾) | 
| 4 | 1, 2, 3 | paddunN 39930 | . 2
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = ( ⊥ ‘(𝑆 ∪ 𝑇))) | 
| 5 |  | simp1 1136 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝐾 ∈ HL) | 
| 6 |  | unss 4189 | . . . . 5
⊢ ((𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) ↔ (𝑆 ∪ 𝑇) ⊆ 𝐴) | 
| 7 | 6 | biimpi 216 | . . . 4
⊢ ((𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ 𝐴) | 
| 8 | 7 | 3adant1 1130 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ 𝐴) | 
| 9 |  | eqid 2736 | . . . 4
⊢
(lub‘𝐾) =
(lub‘𝐾) | 
| 10 |  | eqid 2736 | . . . 4
⊢
(oc‘𝐾) =
(oc‘𝐾) | 
| 11 |  | eqid 2736 | . . . 4
⊢
(pmap‘𝐾) =
(pmap‘𝐾) | 
| 12 | 9, 10, 1, 11, 3 | polval2N 39909 | . . 3
⊢ ((𝐾 ∈ HL ∧ (𝑆 ∪ 𝑇) ⊆ 𝐴) → ( ⊥ ‘(𝑆 ∪ 𝑇)) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))) | 
| 13 | 5, 8, 12 | syl2anc 584 | . 2
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 ∪ 𝑇)) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))) | 
| 14 |  | hlop 39364 | . . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) | 
| 15 | 14 | 3ad2ant1 1133 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝐾 ∈ OP) | 
| 16 |  | hlclat 39360 | . . . . . . 7
⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat) | 
| 17 | 16 | 3ad2ant1 1133 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝐾 ∈ CLat) | 
| 18 |  | simp2 1137 | . . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ 𝐴) | 
| 19 |  | eqid 2736 | . . . . . . . 8
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 20 | 19, 1 | atssbase 39292 | . . . . . . 7
⊢ 𝐴 ⊆ (Base‘𝐾) | 
| 21 | 18, 20 | sstrdi 3995 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ (Base‘𝐾)) | 
| 22 | 19, 9 | clatlubcl 18549 | . . . . . 6
⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑆) ∈ (Base‘𝐾)) | 
| 23 | 17, 21, 22 | syl2anc 584 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘𝑆) ∈ (Base‘𝐾)) | 
| 24 | 19, 10 | opoccl 39196 | . . . . 5
⊢ ((𝐾 ∈ OP ∧
((lub‘𝐾)‘𝑆) ∈ (Base‘𝐾)) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑆)) ∈ (Base‘𝐾)) | 
| 25 | 15, 23, 24 | syl2anc 584 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑆)) ∈ (Base‘𝐾)) | 
| 26 |  | simp3 1138 | . . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ 𝐴) | 
| 27 | 26, 20 | sstrdi 3995 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ (Base‘𝐾)) | 
| 28 | 19, 9 | clatlubcl 18549 | . . . . . 6
⊢ ((𝐾 ∈ CLat ∧ 𝑇 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑇) ∈ (Base‘𝐾)) | 
| 29 | 17, 27, 28 | syl2anc 584 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘𝑇) ∈ (Base‘𝐾)) | 
| 30 | 19, 10 | opoccl 39196 | . . . . 5
⊢ ((𝐾 ∈ OP ∧
((lub‘𝐾)‘𝑇) ∈ (Base‘𝐾)) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑇)) ∈ (Base‘𝐾)) | 
| 31 | 15, 29, 30 | syl2anc 584 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑇)) ∈ (Base‘𝐾)) | 
| 32 |  | eqid 2736 | . . . . 5
⊢
(meet‘𝐾) =
(meet‘𝐾) | 
| 33 | 19, 32, 1, 11 | pmapmeet 39776 | . . . 4
⊢ ((𝐾 ∈ 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 1372 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑆))(meet‘𝐾)((oc‘𝐾)‘((lub‘𝐾)‘𝑇)))) = (((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑆))) ∩ ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑇))))) | 
| 35 |  | eqid 2736 | . . . . . . . 8
⊢
(join‘𝐾) =
(join‘𝐾) | 
| 36 | 19, 35, 9 | lubun 18561 | . . . . . . 7
⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ (Base‘𝐾) ∧ 𝑇 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) = (((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))) | 
| 37 | 17, 21, 27, 36 | syl3anc 1372 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) = (((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))) | 
| 38 | 37 | fveq2d 6909 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((oc‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) = ((oc‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇)))) | 
| 39 |  | hlol 39363 | . . . . . . 7
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) | 
| 40 | 39 | 3ad2ant1 1133 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝐾 ∈ OL) | 
| 41 | 19, 35, 32, 10 | oldmj1 39223 | . . . . . 6
⊢ ((𝐾 ∈ OL ∧
((lub‘𝐾)‘𝑆) ∈ (Base‘𝐾) ∧ ((lub‘𝐾)‘𝑇) ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))) = (((oc‘𝐾)‘((lub‘𝐾)‘𝑆))(meet‘𝐾)((oc‘𝐾)‘((lub‘𝐾)‘𝑇)))) | 
| 42 | 40, 23, 29, 41 | syl3anc 1372 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((oc‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))) = (((oc‘𝐾)‘((lub‘𝐾)‘𝑆))(meet‘𝐾)((oc‘𝐾)‘((lub‘𝐾)‘𝑇)))) | 
| 43 | 38, 42 | eqtrd 2776 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((oc‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) = (((oc‘𝐾)‘((lub‘𝐾)‘𝑆))(meet‘𝐾)((oc‘𝐾)‘((lub‘𝐾)‘𝑇)))) | 
| 44 | 43 | fveq2d 6909 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) = ((pmap‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑆))(meet‘𝐾)((oc‘𝐾)‘((lub‘𝐾)‘𝑇))))) | 
| 45 | 9, 10, 1, 11, 3 | polval2N 39909 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘𝑆) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑆)))) | 
| 46 | 45 | 3adant3 1132 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑆) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑆)))) | 
| 47 | 9, 10, 1, 11, 3 | polval2N 39909 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑇) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑇)))) | 
| 48 | 47 | 3adant2 1131 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑇) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑇)))) | 
| 49 | 46, 48 | ineq12d 4220 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (( ⊥ ‘𝑆) ∩ ( ⊥ ‘𝑇)) = (((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑆))) ∩ ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑇))))) | 
| 50 | 34, 44, 49 | 3eqtr4d 2786 | . 2
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) = (( ⊥ ‘𝑆) ∩ ( ⊥ ‘𝑇))) | 
| 51 | 4, 13, 50 | 3eqtrd 2780 | 1
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = (( ⊥ ‘𝑆) ∩ ( ⊥ ‘𝑇))) |