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 \in HL \land X \in B \land Y \in B) \to (M (X) = M (Y) \leftrightarrow X = Y)$

Step	Hyp	Ref	Expression
1		pmap11.b	$⊢ B = {Base}_{K}$
2		pmap11.m	$⊢ M = pmap (K)$
3		eqss	$⊢ M (X) = M (Y) \leftrightarrow (M (X) \subseteq M (Y) \land M (Y) \subseteq M (X))$
4		hllat	$⊢ K \in HL \to K \in Lat$
5		eqid	$⊢ \leq_{K} = \leq_{K}$
6	1 5	latasymb	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((X \leq_{K} Y \land Y \leq_{K} X) \leftrightarrow X = Y)$
7	4 6	syl3an1	$⊢ (K \in HL \land X \in B \land Y \in B) \to ((X \leq_{K} Y \land Y \leq_{K} X) \leftrightarrow X = Y)$
8	1 5 2	pmaple	$⊢ (K \in HL \land X \in B \land Y \in B) \to (X \leq_{K} Y \leftrightarrow M (X) \subseteq M (Y))$
9	1 5 2	pmaple	$⊢ (K \in HL \land Y \in B \land X \in B) \to (Y \leq_{K} X \leftrightarrow M (Y) \subseteq M (X))$
10	9	3com23	$⊢ (K \in HL \land X \in B \land Y \in B) \to (Y \leq_{K} X \leftrightarrow M (Y) \subseteq M (X))$
11	8 10	anbi12d	$⊢ (K \in HL \land X \in B \land Y \in B) \to ((X \leq_{K} Y \land Y \leq_{K} X) \leftrightarrow (M (X) \subseteq M (Y) \land M (Y) \subseteq M (X)))$
12	7 11	bitr3d	$⊢ (K \in HL \land X \in B \land Y \in B) \to (X = Y \leftrightarrow (M (X) \subseteq M (Y) \land M (Y) \subseteq M (X)))$
13	3 12	bitr4id	$⊢ (K \in HL \land X \in B \land Y \in B) \to (M (X) = M (Y) \leftrightarrow X = Y)$

Metamath Proof Explorer