Proof of Theorem paddatclN
Step | Hyp | Ref
| Expression |
1 | | hlclat 37368 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat) |
2 | 1 | 3ad2ant1 1132 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → 𝐾 ∈ CLat) |
3 | | paddatcl.a |
. . . . . . . 8
⊢ 𝐴 = (Atoms‘𝐾) |
4 | | paddatcl.c |
. . . . . . . 8
⊢ 𝐶 = (PSubCl‘𝐾) |
5 | 3, 4 | psubclssatN 37951 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶) → 𝑋 ⊆ 𝐴) |
6 | | eqid 2740 |
. . . . . . . 8
⊢
(Base‘𝐾) =
(Base‘𝐾) |
7 | 6, 3 | atssbase 37300 |
. . . . . . 7
⊢ 𝐴 ⊆ (Base‘𝐾) |
8 | 5, 7 | sstrdi 3938 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶) → 𝑋 ⊆ (Base‘𝐾)) |
9 | 8 | 3adant3 1131 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → 𝑋 ⊆ (Base‘𝐾)) |
10 | | eqid 2740 |
. . . . . 6
⊢
(lub‘𝐾) =
(lub‘𝐾) |
11 | 6, 10 | clatlubcl 18219 |
. . . . 5
⊢ ((𝐾 ∈ CLat ∧ 𝑋 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) |
12 | 2, 9, 11 | syl2anc 584 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) |
13 | | eqid 2740 |
. . . . 5
⊢
(join‘𝐾) =
(join‘𝐾) |
14 | | eqid 2740 |
. . . . 5
⊢
(pmap‘𝐾) =
(pmap‘𝐾) |
15 | | paddatcl.p |
. . . . 5
⊢ + =
(+𝑃‘𝐾) |
16 | 6, 13, 3, 14, 15 | pmapjat1 37863 |
. . . 4
⊢ ((𝐾 ∈ HL ∧
((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾) ∧ 𝑄 ∈ 𝐴) → ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄)) = (((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) + ((pmap‘𝐾)‘𝑄))) |
17 | 12, 16 | syld3an2 1410 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄)) = (((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) + ((pmap‘𝐾)‘𝑄))) |
18 | 10, 14, 4 | pmapidclN 37952 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶) → ((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) = 𝑋) |
19 | 18 | 3adant3 1131 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) = 𝑋) |
20 | 3, 14 | pmapat 37773 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴) → ((pmap‘𝐾)‘𝑄) = {𝑄}) |
21 | 20 | 3adant2 1130 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → ((pmap‘𝐾)‘𝑄) = {𝑄}) |
22 | 19, 21 | oveq12d 7289 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → (((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) + ((pmap‘𝐾)‘𝑄)) = (𝑋 + {𝑄})) |
23 | 17, 22 | eqtr2d 2781 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → (𝑋 + {𝑄}) = ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄))) |
24 | | simp1 1135 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → 𝐾 ∈ HL) |
25 | | hllat 37373 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
26 | 25 | 3ad2ant1 1132 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → 𝐾 ∈ Lat) |
27 | 6, 3 | atbase 37299 |
. . . . 5
⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾)) |
28 | 27 | 3ad2ant3 1134 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → 𝑄 ∈ (Base‘𝐾)) |
29 | 6, 13 | latjcl 18155 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧
((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → (((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄) ∈ (Base‘𝐾)) |
30 | 26, 12, 28, 29 | syl3anc 1370 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → (((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄) ∈ (Base‘𝐾)) |
31 | 6, 14, 4 | pmapsubclN 37956 |
. . 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 ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → (𝑋 + {𝑄}) ∈ 𝐶) |