Metamath Proof Explorer

Theorem pmap11

Description: The projective map of a Hilbert lattice is one-to-one. Part of Theorem 15.5 of MaedaMaeda p. 62. (Contributed by NM, 22-Oct-2011)

Ref Expression
Hypotheses pmap11.b ⊢ B = Base K
pmap11.m ⊢ M = pmap ⁡ K
Assertion pmap11 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → M ⁡ X = M ⁡ Y ↔ X = Y

Proof

Step Hyp Ref Expression
1 pmap11.b ⊢ B = Base K
2 pmap11.m ⊢ M = pmap ⁡ K
3 eqss ⊢ M ⁡ X = M ⁡ Y ↔ M ⁡ X ⊆ M ⁡ Y ∧ M ⁡ Y ⊆ M ⁡ X
4 hllat ⊢ K ∈ HL → K ∈ Lat
5 eqid ⊢ ≤ K = ≤ K
6 1 5 latasymb ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ≤ K Y ∧ Y ≤ K X ↔ X = Y
7 4 6 syl3an1 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X ≤ K Y ∧ Y ≤ K X ↔ X = Y
8 1 5 2 pmaple ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X ≤ K Y ↔ M ⁡ X ⊆ M ⁡ Y
9 1 5 2 pmaple ⊢ K ∈ HL ∧ Y ∈ B ∧ X ∈ B → Y ≤ K X ↔ M ⁡ Y ⊆ M ⁡ X
10 9 3com23 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → Y ≤ K X ↔ M ⁡ Y ⊆ M ⁡ X
11 8 10 anbi12d ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X ≤ K Y ∧ Y ≤ K X ↔ M ⁡ X ⊆ M ⁡ Y ∧ M ⁡ Y ⊆ M ⁡ X
12 7 11 bitr3d ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X = Y ↔ M ⁡ X ⊆ M ⁡ Y ∧ M ⁡ Y ⊆ M ⁡ X
13 3 12 bitr4id ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → M ⁡ X = M ⁡ Y ↔ X = Y