Proof of Theorem pmapj2N
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp1 1136 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ HL) | 
| 2 |  | hllat 39365 | . . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) | 
| 3 | 2 | 3ad2ant1 1133 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat) | 
| 4 |  | hlop 39364 | . . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) | 
| 5 | 4 | 3ad2ant1 1133 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ OP) | 
| 6 |  | simp2 1137 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵) | 
| 7 |  | pmapj2.b | . . . . . 6
⊢ 𝐵 = (Base‘𝐾) | 
| 8 |  | eqid 2736 | . . . . . 6
⊢
(oc‘𝐾) =
(oc‘𝐾) | 
| 9 | 7, 8 | opoccl 39196 | . . . . 5
⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵) | 
| 10 | 5, 6, 9 | syl2anc 584 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵) | 
| 11 |  | simp3 1138 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) | 
| 12 | 7, 8 | opoccl 39196 | . . . . 5
⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘𝑌) ∈ 𝐵) | 
| 13 | 5, 11, 12 | syl2anc 584 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘𝑌) ∈ 𝐵) | 
| 14 |  | eqid 2736 | . . . . 5
⊢
(meet‘𝐾) =
(meet‘𝐾) | 
| 15 | 7, 14 | latmcl 18486 | . . . 4
⊢ ((𝐾 ∈ Lat ∧
((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)) ∈ 𝐵) | 
| 16 | 3, 10, 13, 15 | syl3anc 1372 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)) ∈ 𝐵) | 
| 17 |  | pmapj2.m | . . . 4
⊢ 𝑀 = (pmap‘𝐾) | 
| 18 |  | pmapj2.o | . . . 4
⊢  ⊥ =
(⊥𝑃‘𝐾) | 
| 19 | 7, 8, 17, 18 | polpmapN 39915 | . . 3
⊢ ((𝐾 ∈ HL ∧
(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)) ∈ 𝐵) → ( ⊥ ‘(𝑀‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))) = (𝑀‘((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))))) | 
| 20 | 1, 16, 19 | syl2anc 584 | . 2
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑀‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))) = (𝑀‘((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))))) | 
| 21 | 7, 8, 17, 18 | polpmapN 39915 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘(𝑀‘𝑋)) = (𝑀‘((oc‘𝐾)‘𝑋))) | 
| 22 | 21 | 3adant3 1132 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑀‘𝑋)) = (𝑀‘((oc‘𝐾)‘𝑋))) | 
| 23 | 7, 8, 17, 18 | polpmapN 39915 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑀‘𝑌)) = (𝑀‘((oc‘𝐾)‘𝑌))) | 
| 24 | 23 | 3adant2 1131 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑀‘𝑌)) = (𝑀‘((oc‘𝐾)‘𝑌))) | 
| 25 | 22, 24 | ineq12d 4220 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘(𝑀‘𝑋)) ∩ ( ⊥ ‘(𝑀‘𝑌))) = ((𝑀‘((oc‘𝐾)‘𝑋)) ∩ (𝑀‘((oc‘𝐾)‘𝑌)))) | 
| 26 |  | eqid 2736 | . . . . . . 7
⊢
(Atoms‘𝐾) =
(Atoms‘𝐾) | 
| 27 | 7, 26, 17 | pmapssat 39762 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ⊆ (Atoms‘𝐾)) | 
| 28 | 27 | 3adant3 1132 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑀‘𝑋) ⊆ (Atoms‘𝐾)) | 
| 29 | 7, 26, 17 | pmapssat 39762 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵) → (𝑀‘𝑌) ⊆ (Atoms‘𝐾)) | 
| 30 | 29 | 3adant2 1131 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑀‘𝑌) ⊆ (Atoms‘𝐾)) | 
| 31 |  | pmapj2.p | . . . . . 6
⊢  + =
(+𝑃‘𝐾) | 
| 32 | 26, 31, 18 | poldmj1N 39931 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑀‘𝑋) ⊆ (Atoms‘𝐾) ∧ (𝑀‘𝑌) ⊆ (Atoms‘𝐾)) → ( ⊥ ‘((𝑀‘𝑋) + (𝑀‘𝑌))) = (( ⊥ ‘(𝑀‘𝑋)) ∩ ( ⊥ ‘(𝑀‘𝑌)))) | 
| 33 | 1, 28, 30, 32 | syl3anc 1372 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘((𝑀‘𝑋) + (𝑀‘𝑌))) = (( ⊥ ‘(𝑀‘𝑋)) ∩ ( ⊥ ‘(𝑀‘𝑌)))) | 
| 34 | 7, 14, 26, 17 | pmapmeet 39776 | . . . . 5
⊢ ((𝐾 ∈ HL ∧
((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (𝑀‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))) = ((𝑀‘((oc‘𝐾)‘𝑋)) ∩ (𝑀‘((oc‘𝐾)‘𝑌)))) | 
| 35 | 1, 10, 13, 34 | syl3anc 1372 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑀‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))) = ((𝑀‘((oc‘𝐾)‘𝑋)) ∩ (𝑀‘((oc‘𝐾)‘𝑌)))) | 
| 36 | 25, 33, 35 | 3eqtr4rd 2787 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑀‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))) = ( ⊥ ‘((𝑀‘𝑋) + (𝑀‘𝑌)))) | 
| 37 | 36 | fveq2d 6909 | . 2
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑀‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))) = ( ⊥ ‘( ⊥
‘((𝑀‘𝑋) + (𝑀‘𝑌))))) | 
| 38 |  | hlol 39363 | . . . 4
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) | 
| 39 |  | pmapj2.j | . . . . 5
⊢  ∨ =
(join‘𝐾) | 
| 40 | 7, 39, 14, 8 | oldmm4 39222 | . . . 4
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))) = (𝑋 ∨ 𝑌)) | 
| 41 | 38, 40 | syl3an1 1163 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))) = (𝑋 ∨ 𝑌)) | 
| 42 | 41 | fveq2d 6909 | . 2
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑀‘((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))) = (𝑀‘(𝑋 ∨ 𝑌))) | 
| 43 | 20, 37, 42 | 3eqtr3rd 2785 | 1
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑀‘(𝑋 ∨ 𝑌)) = ( ⊥ ‘( ⊥
‘((𝑀‘𝑋) + (𝑀‘𝑌))))) |