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

Metamath Proof Explorer

Theorem pmapssat

Description: The projective map of a Hilbert lattice is a set of atoms. (Contributed by NM, 14-Jan-2012)

	Ref	Expression
Hypotheses	pmapssat.b	$⊢ B = {Base}_{K}$
	pmapssat.a	$⊢ A = Atoms (K)$
	pmapssat.m	$⊢ M = pmap (K)$
Assertion	pmapssat	$⊢ (K \in C \land X \in B) \to M (X) \subseteq A$

Step	Hyp	Ref	Expression
1		pmapssat.b	$⊢ B = {Base}_{K}$
2		pmapssat.a	$⊢ A = Atoms (K)$
3		pmapssat.m	$⊢ M = pmap (K)$
4		eqid	$⊢ \leq_{K} = \leq_{K}$
5	1 4 2 3	pmapval	$⊢ (K \in C \land X \in B) \to M (X) = \{p \in A \| p \leq_{K} X\}$
6		ssrab2	$⊢ \{p \in A \| p \leq_{K} X\} \subseteq A$
7	5 6	eqsstrdi	$⊢ (K \in C \land X \in B) \to M (X) \subseteq A$