# Metamath Proof Explorer

## Theorem 2pmaplubN

Description: Double projective map of an LUB. (Contributed by NM, 6-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses sspmaplub.u ${⊢}{U}=\mathrm{lub}\left({K}\right)$
sspmaplub.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
sspmaplub.m ${⊢}{M}=\mathrm{pmap}\left({K}\right)$
Assertion 2pmaplubN ${⊢}\left({K}\in \mathrm{HL}\wedge {S}\subseteq {A}\right)\to {M}\left({U}\left({M}\left({U}\left({S}\right)\right)\right)\right)={M}\left({U}\left({S}\right)\right)$

### Proof

Step Hyp Ref Expression
1 sspmaplub.u ${⊢}{U}=\mathrm{lub}\left({K}\right)$
2 sspmaplub.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
3 sspmaplub.m ${⊢}{M}=\mathrm{pmap}\left({K}\right)$
4 eqid ${⊢}{\perp }_{𝑃}\left({K}\right)={\perp }_{𝑃}\left({K}\right)$
5 1 2 3 4 2polvalN ${⊢}\left({K}\in \mathrm{HL}\wedge {S}\subseteq {A}\right)\to {\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({S}\right)\right)={M}\left({U}\left({S}\right)\right)$
6 5 fveq2d ${⊢}\left({K}\in \mathrm{HL}\wedge {S}\subseteq {A}\right)\to {\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({S}\right)\right)\right)={\perp }_{𝑃}\left({K}\right)\left({M}\left({U}\left({S}\right)\right)\right)$
7 6 fveq2d ${⊢}\left({K}\in \mathrm{HL}\wedge {S}\subseteq {A}\right)\to {\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({S}\right)\right)\right)\right)={\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({M}\left({U}\left({S}\right)\right)\right)\right)$
8 2 4 polssatN ${⊢}\left({K}\in \mathrm{HL}\wedge {S}\subseteq {A}\right)\to {\perp }_{𝑃}\left({K}\right)\left({S}\right)\subseteq {A}$
9 2 4 3polN ${⊢}\left({K}\in \mathrm{HL}\wedge {\perp }_{𝑃}\left({K}\right)\left({S}\right)\subseteq {A}\right)\to {\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({S}\right)\right)\right)\right)={\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({S}\right)\right)$
10 8 9 syldan ${⊢}\left({K}\in \mathrm{HL}\wedge {S}\subseteq {A}\right)\to {\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({S}\right)\right)\right)\right)={\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({S}\right)\right)$
11 7 10 eqtr3d ${⊢}\left({K}\in \mathrm{HL}\wedge {S}\subseteq {A}\right)\to {\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({M}\left({U}\left({S}\right)\right)\right)\right)={\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({S}\right)\right)$
12 hlclat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{CLat}$
13 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
14 13 2 atssbase ${⊢}{A}\subseteq {\mathrm{Base}}_{{K}}$
15 sstr ${⊢}\left({S}\subseteq {A}\wedge {A}\subseteq {\mathrm{Base}}_{{K}}\right)\to {S}\subseteq {\mathrm{Base}}_{{K}}$
16 14 15 mpan2 ${⊢}{S}\subseteq {A}\to {S}\subseteq {\mathrm{Base}}_{{K}}$
17 13 1 clatlubcl ${⊢}\left({K}\in \mathrm{CLat}\wedge {S}\subseteq {\mathrm{Base}}_{{K}}\right)\to {U}\left({S}\right)\in {\mathrm{Base}}_{{K}}$
18 12 16 17 syl2an ${⊢}\left({K}\in \mathrm{HL}\wedge {S}\subseteq {A}\right)\to {U}\left({S}\right)\in {\mathrm{Base}}_{{K}}$
19 13 2 3 pmapssat ${⊢}\left({K}\in \mathrm{HL}\wedge {U}\left({S}\right)\in {\mathrm{Base}}_{{K}}\right)\to {M}\left({U}\left({S}\right)\right)\subseteq {A}$
20 18 19 syldan ${⊢}\left({K}\in \mathrm{HL}\wedge {S}\subseteq {A}\right)\to {M}\left({U}\left({S}\right)\right)\subseteq {A}$
21 1 2 3 4 2polvalN ${⊢}\left({K}\in \mathrm{HL}\wedge {M}\left({U}\left({S}\right)\right)\subseteq {A}\right)\to {\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({M}\left({U}\left({S}\right)\right)\right)\right)={M}\left({U}\left({M}\left({U}\left({S}\right)\right)\right)\right)$
22 20 21 syldan ${⊢}\left({K}\in \mathrm{HL}\wedge {S}\subseteq {A}\right)\to {\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({M}\left({U}\left({S}\right)\right)\right)\right)={M}\left({U}\left({M}\left({U}\left({S}\right)\right)\right)\right)$
23 11 22 eqtr3d ${⊢}\left({K}\in \mathrm{HL}\wedge {S}\subseteq {A}\right)\to {\perp }_{𝑃}\left({K}\right)\left({\perp }_{𝑃}\left({K}\right)\left({S}\right)\right)={M}\left({U}\left({M}\left({U}\left({S}\right)\right)\right)\right)$
24 23 5 eqtr3d ${⊢}\left({K}\in \mathrm{HL}\wedge {S}\subseteq {A}\right)\to {M}\left({U}\left({M}\left({U}\left({S}\right)\right)\right)\right)={M}\left({U}\left({S}\right)\right)$