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 = lub ⁡ K
sspmaplub.a ⊢ A = Atoms ⁡ K
sspmaplub.m ⊢ M = pmap ⁡ K
Assertion 2pmaplubN ⊢ K ∈ HL ∧ S ⊆ A → M ⁡ U ⁡ M ⁡ U ⁡ S = M ⁡ U ⁡ S

Proof

Step Hyp Ref Expression
1 sspmaplub.u ⊢ U = lub ⁡ K
2 sspmaplub.a ⊢ A = Atoms ⁡ K
3 sspmaplub.m ⊢ M = pmap ⁡ K
4 eqid ⊢ ⊥ 𝑃 ⁡ K = ⊥ 𝑃 ⁡ K
5 1 2 3 4 2polvalN ⊢ K ∈ HL ∧ S ⊆ A → ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ S = M ⁡ U ⁡ S
6 5 fveq2d ⊢ K ∈ HL ∧ S ⊆ A → ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ S = ⊥ 𝑃 ⁡ K ⁡ M ⁡ U ⁡ S
7 6 fveq2d ⊢ K ∈ HL ∧ S ⊆ A → ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ S = ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ M ⁡ U ⁡ S
8 2 4 polssatN ⊢ K ∈ HL ∧ S ⊆ A → ⊥ 𝑃 ⁡ K ⁡ S ⊆ A
9 2 4 3polN ⊢ K ∈ HL ∧ ⊥ 𝑃 ⁡ K ⁡ S ⊆ A → ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ S = ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ S
10 8 9 syldan ⊢ K ∈ HL ∧ S ⊆ A → ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ S = ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ S
11 7 10 eqtr3d ⊢ K ∈ HL ∧ S ⊆ A → ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ M ⁡ U ⁡ S = ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ S
12 hlclat ⊢ K ∈ HL → K ∈ CLat
13 eqid ⊢ Base K = Base K
14 13 2 atssbase ⊢ A ⊆ Base K
15 sstr ⊢ S ⊆ A ∧ A ⊆ Base K → S ⊆ Base K
16 14 15 mpan2 ⊢ S ⊆ A → S ⊆ Base K
17 13 1 clatlubcl ⊢ K ∈ CLat ∧ S ⊆ Base K → U ⁡ S ∈ Base K
18 12 16 17 syl2an ⊢ K ∈ HL ∧ S ⊆ A → U ⁡ S ∈ Base K
19 13 2 3 pmapssat ⊢ K ∈ HL ∧ U ⁡ S ∈ Base K → M ⁡ U ⁡ S ⊆ A
20 18 19 syldan ⊢ K ∈ HL ∧ S ⊆ A → M ⁡ U ⁡ S ⊆ A
21 1 2 3 4 2polvalN ⊢ K ∈ HL ∧ M ⁡ U ⁡ S ⊆ A → ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ M ⁡ U ⁡ S = M ⁡ U ⁡ M ⁡ U ⁡ S
22 20 21 syldan ⊢ K ∈ HL ∧ S ⊆ A → ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ M ⁡ U ⁡ S = M ⁡ U ⁡ M ⁡ U ⁡ S
23 11 22 eqtr3d ⊢ K ∈ HL ∧ S ⊆ A → ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ S = M ⁡ U ⁡ M ⁡ U ⁡ S
24 23 5 eqtr3d ⊢ K ∈ HL ∧ S ⊆ A → M ⁡ U ⁡ M ⁡ U ⁡ S = M ⁡ U ⁡ S