Proof of Theorem paddatclN
Step | Hyp | Ref
| Expression |
1 | | hlclat 34645 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat) |
2 | 1 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → 𝐾 ∈ CLat) |
3 | | paddatcl.a |
. . . . . . . 8
⊢ 𝐴 = (Atoms‘𝐾) |
4 | | paddatcl.c |
. . . . . . . 8
⊢ 𝐶 = (PSubCl‘𝐾) |
5 | 3, 4 | psubclssatN 35227 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶) → 𝑋 ⊆ 𝐴) |
6 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘𝐾) =
(Base‘𝐾) |
7 | 6, 3 | atssbase 34577 |
. . . . . . 7
⊢ 𝐴 ⊆ (Base‘𝐾) |
8 | 5, 7 | syl6ss 3615 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶) → 𝑋 ⊆ (Base‘𝐾)) |
9 | 8 | 3adant3 1081 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → 𝑋 ⊆ (Base‘𝐾)) |
10 | | eqid 2622 |
. . . . . 6
⊢
(lub‘𝐾) =
(lub‘𝐾) |
11 | 6, 10 | clatlubcl 17112 |
. . . . 5
⊢ ((𝐾 ∈ CLat ∧ 𝑋 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) |
12 | 2, 9, 11 | syl2anc 693 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) |
13 | | eqid 2622 |
. . . . 5
⊢
(join‘𝐾) =
(join‘𝐾) |
14 | | eqid 2622 |
. . . . 5
⊢
(pmap‘𝐾) =
(pmap‘𝐾) |
15 | | paddatcl.p |
. . . . 5
⊢ + =
(+𝑃‘𝐾) |
16 | 6, 13, 3, 14, 15 | pmapjat1 35139 |
. . . 4
⊢ ((𝐾 ∈ HL ∧
((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾) ∧ 𝑄 ∈ 𝐴) → ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄)) = (((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) + ((pmap‘𝐾)‘𝑄))) |
17 | 12, 16 | syld3an2 1373 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄)) = (((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) + ((pmap‘𝐾)‘𝑄))) |
18 | 10, 14, 4 | pmapidclN 35228 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶) → ((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) = 𝑋) |
19 | 18 | 3adant3 1081 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) = 𝑋) |
20 | 3, 14 | pmapat 35049 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴) → ((pmap‘𝐾)‘𝑄) = {𝑄}) |
21 | 20 | 3adant2 1080 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → ((pmap‘𝐾)‘𝑄) = {𝑄}) |
22 | 19, 21 | oveq12d 6668 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → (((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) + ((pmap‘𝐾)‘𝑄)) = (𝑋 + {𝑄})) |
23 | 17, 22 | eqtr2d 2657 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → (𝑋 + {𝑄}) = ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄))) |
24 | | simp1 1061 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → 𝐾 ∈ HL) |
25 | | hllat 34650 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
26 | 25 | 3ad2ant1 1082 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → 𝐾 ∈ Lat) |
27 | 6, 3 | atbase 34576 |
. . . . 5
⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾)) |
28 | 27 | 3ad2ant3 1084 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → 𝑄 ∈ (Base‘𝐾)) |
29 | 6, 13 | latjcl 17051 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧
((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → (((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄) ∈ (Base‘𝐾)) |
30 | 26, 12, 28, 29 | syl3anc 1326 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → (((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄) ∈ (Base‘𝐾)) |
31 | 6, 14, 4 | pmapsubclN 35232 |
. . 3
⊢ ((𝐾 ∈ HL ∧
(((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄) ∈ (Base‘𝐾)) → ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄)) ∈ 𝐶) |
32 | 24, 30, 31 | syl2anc 693 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑋)(join‘𝐾)𝑄)) ∈ 𝐶) |
33 | 23, 32 | eqeltrd 2701 |
1
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → (𝑋 + {𝑄}) ∈ 𝐶) |