Proof of Theorem pmapojoinN
| Step | Hyp | Ref
| Expression |
| 1 | | pmapojoin.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
| 2 | | pmapojoin.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
| 3 | | pmapojoin.m |
. . . 4
⊢ 𝑀 = (pmap‘𝐾) |
| 4 | | pmapojoin.p |
. . . 4
⊢ + =
(+𝑃‘𝐾) |
| 5 | | eqid 2737 |
. . . 4
⊢
(⊥𝑃‘𝐾) = (⊥𝑃‘𝐾) |
| 6 | 1, 2, 3, 4, 5 | pmapj2N 39931 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑀‘(𝑋 ∨ 𝑌)) =
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘((𝑀‘𝑋) + (𝑀‘𝑌))))) |
| 7 | 6 | adantr 480 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ ( ⊥ ‘𝑌)) → (𝑀‘(𝑋 ∨ 𝑌)) =
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘((𝑀‘𝑋) + (𝑀‘𝑌))))) |
| 8 | | simpl1 1192 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ ( ⊥ ‘𝑌)) → 𝐾 ∈ HL) |
| 9 | | simpl2 1193 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ ( ⊥ ‘𝑌)) → 𝑋 ∈ 𝐵) |
| 10 | | eqid 2737 |
. . . . . 6
⊢
(PSubCl‘𝐾) =
(PSubCl‘𝐾) |
| 11 | 1, 3, 10 | pmapsubclN 39948 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ∈ (PSubCl‘𝐾)) |
| 12 | 8, 9, 11 | syl2anc 584 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ ( ⊥ ‘𝑌)) → (𝑀‘𝑋) ∈ (PSubCl‘𝐾)) |
| 13 | | simpl3 1194 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ ( ⊥ ‘𝑌)) → 𝑌 ∈ 𝐵) |
| 14 | 1, 3, 10 | pmapsubclN 39948 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵) → (𝑀‘𝑌) ∈ (PSubCl‘𝐾)) |
| 15 | 8, 13, 14 | syl2anc 584 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ ( ⊥ ‘𝑌)) → (𝑀‘𝑌) ∈ (PSubCl‘𝐾)) |
| 16 | | hlop 39363 |
. . . . . . . . 9
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
| 17 | 16 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ OP) |
| 18 | | simp3 1139 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) |
| 19 | | pmapojoin.o |
. . . . . . . . 9
⊢ ⊥ =
(oc‘𝐾) |
| 20 | 1, 19 | opoccl 39195 |
. . . . . . . 8
⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑌) ∈ 𝐵) |
| 21 | 17, 18, 20 | syl2anc 584 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑌) ∈ 𝐵) |
| 22 | | pmapojoin.l |
. . . . . . . 8
⊢ ≤ =
(le‘𝐾) |
| 23 | 1, 22, 3 | pmaple 39763 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘𝑌) ∈ 𝐵) → (𝑋 ≤ ( ⊥ ‘𝑌) ↔ (𝑀‘𝑋) ⊆ (𝑀‘( ⊥ ‘𝑌)))) |
| 24 | 21, 23 | syld3an3 1411 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ ( ⊥ ‘𝑌) ↔ (𝑀‘𝑋) ⊆ (𝑀‘( ⊥ ‘𝑌)))) |
| 25 | 24 | biimpa 476 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ ( ⊥ ‘𝑌)) → (𝑀‘𝑋) ⊆ (𝑀‘( ⊥ ‘𝑌))) |
| 26 | 1, 19, 3, 5 | polpmapN 39914 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵) →
((⊥𝑃‘𝐾)‘(𝑀‘𝑌)) = (𝑀‘( ⊥ ‘𝑌))) |
| 27 | 8, 13, 26 | syl2anc 584 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ ( ⊥ ‘𝑌)) →
((⊥𝑃‘𝐾)‘(𝑀‘𝑌)) = (𝑀‘( ⊥ ‘𝑌))) |
| 28 | 25, 27 | sseqtrrd 4021 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ ( ⊥ ‘𝑌)) → (𝑀‘𝑋) ⊆
((⊥𝑃‘𝐾)‘(𝑀‘𝑌))) |
| 29 | 4, 5, 10 | osumclN 39969 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ (𝑀‘𝑋) ∈ (PSubCl‘𝐾) ∧ (𝑀‘𝑌) ∈ (PSubCl‘𝐾)) ∧ (𝑀‘𝑋) ⊆
((⊥𝑃‘𝐾)‘(𝑀‘𝑌))) → ((𝑀‘𝑋) + (𝑀‘𝑌)) ∈ (PSubCl‘𝐾)) |
| 30 | 8, 12, 15, 28, 29 | syl31anc 1375 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ ( ⊥ ‘𝑌)) → ((𝑀‘𝑋) + (𝑀‘𝑌)) ∈ (PSubCl‘𝐾)) |
| 31 | 5, 10 | psubcli2N 39941 |
. . 3
⊢ ((𝐾 ∈ HL ∧ ((𝑀‘𝑋) + (𝑀‘𝑌)) ∈ (PSubCl‘𝐾)) →
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘((𝑀‘𝑋) + (𝑀‘𝑌)))) = ((𝑀‘𝑋) + (𝑀‘𝑌))) |
| 32 | 8, 30, 31 | syl2anc 584 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ ( ⊥ ‘𝑌)) →
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘((𝑀‘𝑋) + (𝑀‘𝑌)))) = ((𝑀‘𝑋) + (𝑀‘𝑌))) |
| 33 | 7, 32 | eqtrd 2777 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ ( ⊥ ‘𝑌)) → (𝑀‘(𝑋 ∨ 𝑌)) = ((𝑀‘𝑋) + (𝑀‘𝑌))) |