Metamath Proof Explorer

Theorem polpmapN

Description: The polarity of a projective map. (Contributed by NM, 24-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses polpmap.b ⊢ B = Base K
polpmap.o ⊢ ⊥ ˙ = oc ⁡ K
polpmap.m ⊢ M = pmap ⁡ K
polpmap.p ⊢ P = ⊥ 𝑃 ⁡ K
Assertion polpmapN ⊢ K ∈ HL ∧ X ∈ B → P ⁡ M ⁡ X = M ⁡ ⊥ ˙ ⁡ X

Proof

Step Hyp Ref Expression
1 polpmap.b ⊢ B = Base K
2 polpmap.o ⊢ ⊥ ˙ = oc ⁡ K
3 polpmap.m ⊢ M = pmap ⁡ K
4 polpmap.p ⊢ P = ⊥ 𝑃 ⁡ K
5 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
6 1 5 3 pmapssat ⊢ K ∈ HL ∧ X ∈ B → M ⁡ X ⊆ Atoms ⁡ K
7 eqid ⊢ lub ⁡ K = lub ⁡ K
8 7 2 5 3 4 polval2N ⊢ K ∈ HL ∧ M ⁡ X ⊆ Atoms ⁡ K → P ⁡ M ⁡ X = M ⁡ ⊥ ˙ ⁡ lub ⁡ K ⁡ M ⁡ X
9 6 8 syldan ⊢ K ∈ HL ∧ X ∈ B → P ⁡ M ⁡ X = M ⁡ ⊥ ˙ ⁡ lub ⁡ K ⁡ M ⁡ X
10 eqid ⊢ ≤ K = ≤ K
11 1 10 5 3 pmapval ⊢ K ∈ HL ∧ X ∈ B → M ⁡ X = p ∈ Atoms ⁡ K | p ≤ K X
12 11 fveq2d ⊢ K ∈ HL ∧ X ∈ B → lub ⁡ K ⁡ M ⁡ X = lub ⁡ K ⁡ p ∈ Atoms ⁡ K | p ≤ K X
13 hlomcmat ⊢ K ∈ HL → K ∈ OML ∧ K ∈ CLat ∧ K ∈ AtLat
14 1 10 7 5 atlatmstc ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ AtLat ∧ X ∈ B → lub ⁡ K ⁡ p ∈ Atoms ⁡ K | p ≤ K X = X
15 13 14 sylan ⊢ K ∈ HL ∧ X ∈ B → lub ⁡ K ⁡ p ∈ Atoms ⁡ K | p ≤ K X = X
16 12 15 eqtrd ⊢ K ∈ HL ∧ X ∈ B → lub ⁡ K ⁡ M ⁡ X = X
17 16 fveq2d ⊢ K ∈ HL ∧ X ∈ B → ⊥ ˙ ⁡ lub ⁡ K ⁡ M ⁡ X = ⊥ ˙ ⁡ X
18 17 fveq2d ⊢ K ∈ HL ∧ X ∈ B → M ⁡ ⊥ ˙ ⁡ lub ⁡ K ⁡ M ⁡ X = M ⁡ ⊥ ˙ ⁡ X
19 9 18 eqtrd ⊢ K ∈ HL ∧ X ∈ B → P ⁡ M ⁡ X = M ⁡ ⊥ ˙ ⁡ X