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

Metamath Proof Explorer

Theorem pmapval

Description: Value of the projective map of a Hilbert lattice. Definition in Theorem 15.5 of MaedaMaeda p. 62. (Contributed by NM, 2-Oct-2011)

Ref Expression
Hypotheses pmapfval.b ⊢ B = Base K
pmapfval.l ⊢ ≤ ˙ = ≤ K
pmapfval.a ⊢ A = Atoms ⁡ K
pmapfval.m ⊢ M = pmap ⁡ K
Assertion pmapval ⊢ K ∈ C ∧ X ∈ B → M ⁡ X = a ∈ A | a ≤ ˙ X

Proof

Step Hyp Ref Expression
1 pmapfval.b ⊢ B = Base K
2 pmapfval.l ⊢ ≤ ˙ = ≤ K
3 pmapfval.a ⊢ A = Atoms ⁡ K
4 pmapfval.m ⊢ M = pmap ⁡ K
5 1 2 3 4 pmapfval ⊢ K ∈ C → M = x ∈ B ⟼ a ∈ A | a ≤ ˙ x
6 5 fveq1d ⊢ K ∈ C → M ⁡ X = x ∈ B ⟼ a ∈ A | a ≤ ˙ x ⁡ X
7 breq2 ⊢ x = X → a ≤ ˙ x ↔ a ≤ ˙ X
8 7 rabbidv ⊢ x = X → a ∈ A | a ≤ ˙ x = a ∈ A | a ≤ ˙ X
9 eqid ⊢ x ∈ B ⟼ a ∈ A | a ≤ ˙ x = x ∈ B ⟼ a ∈ A | a ≤ ˙ x
10 3 fvexi ⊢ A ∈ V
11 10 rabex ⊢ a ∈ A | a ≤ ˙ X ∈ V
12 8 9 11 fvmpt ⊢ X ∈ B → x ∈ B ⟼ a ∈ A | a ≤ ˙ x ⁡ X = a ∈ A | a ≤ ˙ X
13 6 12 sylan9eq ⊢ K ∈ C ∧ X ∈ B → M ⁡ X = a ∈ A | a ≤ ˙ X