This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pmap1N

Description: Value of the projective map of a Hilbert lattice at lattice unity. Part of Theorem 15.5.1 of MaedaMaeda p. 62. (Contributed by NM, 22-Oct-2011) (New usage is discouraged.)

Ref Expression
Hypotheses pmap1.u ⊢ 1 ˙ = 1. ⁡ K
pmap1.a ⊢ A = Atoms ⁡ K
pmap1.m ⊢ M = pmap ⁡ K
Assertion pmap1N ⊢ K ∈ OP → M ⁡ 1 ˙ = A

Proof

Step Hyp Ref Expression
1 pmap1.u ⊢ 1 ˙ = 1. ⁡ K
2 pmap1.a ⊢ A = Atoms ⁡ K
3 pmap1.m ⊢ M = pmap ⁡ K
4 eqid ⊢ Base K = Base K
5 4 1 op1cl ⊢ K ∈ OP → 1 ˙ ∈ Base K
6 eqid ⊢ ≤ K = ≤ K
7 4 6 2 3 pmapval ⊢ K ∈ OP ∧ 1 ˙ ∈ Base K → M ⁡ 1 ˙ = p ∈ A | p ≤ K 1 ˙
8 5 7 mpdan ⊢ K ∈ OP → M ⁡ 1 ˙ = p ∈ A | p ≤ K 1 ˙
9 4 2 atbase ⊢ p ∈ A → p ∈ Base K
10 4 6 1 ople1 ⊢ K ∈ OP ∧ p ∈ Base K → p ≤ K 1 ˙
11 9 10 sylan2 ⊢ K ∈ OP ∧ p ∈ A → p ≤ K 1 ˙
12 11 ralrimiva ⊢ K ∈ OP → ∀ p ∈ A p ≤ K 1 ˙
13 rabid2 ⊢ A = p ∈ A | p ≤ K 1 ˙ ↔ ∀ p ∈ A p ≤ K 1 ˙
14 12 13 sylibr ⊢ K ∈ OP → A = p ∈ A | p ≤ K 1 ˙
15 8 14 eqtr4d ⊢ K ∈ OP → M ⁡ 1 ˙ = A