Proof of Theorem paddatclN
| Step | Hyp | Ref
| Expression |
| 1 | | hlclat 39359 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat) |
| 2 | 1 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → 𝐾 ∈ CLat) |
| 3 | | paddatcl.a |
. . . . . . . 8
⊢ 𝐴 = (Atoms‘𝐾) |
| 4 | | paddatcl.c |
. . . . . . . 8
⊢ 𝐶 = (PSubCl‘𝐾) |
| 5 | 3, 4 | psubclssatN 39943 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶) → 𝑋 ⊆ 𝐴) |
| 6 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 7 | 6, 3 | atssbase 39291 |
. . . . . . 7
⊢ 𝐴 ⊆ (Base‘𝐾) |
| 8 | 5, 7 | sstrdi 3996 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶) → 𝑋 ⊆ (Base‘𝐾)) |
| 9 | 8 | 3adant3 1133 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → 𝑋 ⊆ (Base‘𝐾)) |
| 10 | | eqid 2737 |
. . . . . 6
⊢
(lub‘𝐾) =
(lub‘𝐾) |
| 11 | 6, 10 | clatlubcl 18548 |
. . . . 5
⊢ ((𝐾 ∈ CLat ∧ 𝑋 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) |
| 12 | 2, 9, 11 | syl2anc 584 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) |
| 13 | | eqid 2737 |
. . . . 5
⊢
(join‘𝐾) =
(join‘𝐾) |
| 14 | | eqid 2737 |
. . . . 5
⊢
(pmap‘𝐾) =
(pmap‘𝐾) |
| 15 | | paddatcl.p |
. . . . 5
⊢ + =
(+𝑃‘𝐾) |
| 16 | 6, 13, 3, 14, 15 | pmapjat1 39855 |
. . . 4
⊢ ((𝐾 ∈ HL ∧
((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾) ∧ 𝑄 ∈ 𝐴) → ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄)) = (((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) + ((pmap‘𝐾)‘𝑄))) |
| 17 | 12, 16 | syld3an2 1413 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄)) = (((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) + ((pmap‘𝐾)‘𝑄))) |
| 18 | 10, 14, 4 | pmapidclN 39944 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶) → ((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) = 𝑋) |
| 19 | 18 | 3adant3 1133 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) = 𝑋) |
| 20 | 3, 14 | pmapat 39765 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴) → ((pmap‘𝐾)‘𝑄) = {𝑄}) |
| 21 | 20 | 3adant2 1132 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → ((pmap‘𝐾)‘𝑄) = {𝑄}) |
| 22 | 19, 21 | oveq12d 7449 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → (((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) + ((pmap‘𝐾)‘𝑄)) = (𝑋 + {𝑄})) |
| 23 | 17, 22 | eqtr2d 2778 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → (𝑋 + {𝑄}) = ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄))) |
| 24 | | simp1 1137 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → 𝐾 ∈ HL) |
| 25 | | hllat 39364 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
| 26 | 25 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → 𝐾 ∈ Lat) |
| 27 | 6, 3 | atbase 39290 |
. . . . 5
⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾)) |
| 28 | 27 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → 𝑄 ∈ (Base‘𝐾)) |
| 29 | 6, 13 | latjcl 18484 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧
((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → (((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄) ∈ (Base‘𝐾)) |
| 30 | 26, 12, 28, 29 | syl3anc 1373 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → (((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄) ∈ (Base‘𝐾)) |
| 31 | 6, 14, 4 | pmapsubclN 39948 |
. . 3
⊢ ((𝐾 ∈ HL ∧
(((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄) ∈ (Base‘𝐾)) → ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄)) ∈ 𝐶) |
| 32 | 24, 30, 31 | syl2anc 584 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄)) ∈ 𝐶) |
| 33 | 23, 32 | eqeltrd 2841 |
1
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → (𝑋 + {𝑄}) ∈ 𝐶) |