pmapeq0

Description: A projective map value is zero iff its argument is lattice zero. (Contributed by NM, 27-Jan-2012)

	Ref	Expression
Hypotheses	pmapeq0.b	$⊢ B = {Base}_{K}$
	pmapeq0.z	$⊢ \underset{˙}{0} = 0. (K)$
	pmapeq0.m	$⊢ M = pmap (K)$
Assertion	pmapeq0	$⊢ (K \in HL \land X \in B) \to (M (X) = \emptyset \leftrightarrow X = \underset{˙}{0})$

Step	Hyp	Ref	Expression
1		pmapeq0.b	$⊢ B = {Base}_{K}$
2		pmapeq0.z	$⊢ \underset{˙}{0} = 0. (K)$
3		pmapeq0.m	$⊢ M = pmap (K)$
4		hlatl	$⊢ K \in HL \to K \in AtLat$
5	4	adantr	$⊢ (K \in HL \land X \in B) \to K \in AtLat$
6	2 3	pmap0	$⊢ K \in AtLat \to M (\underset{˙}{0}) = \emptyset$
7	5 6	syl	$⊢ (K \in HL \land X \in B) \to M (\underset{˙}{0}) = \emptyset$
8	7	eqeq2d	$⊢ (K \in HL \land X \in B) \to (M (X) = M (\underset{˙}{0}) \leftrightarrow M (X) = \emptyset)$
9		hlop	$⊢ K \in HL \to K \in OP$
10	9	adantr	$⊢ (K \in HL \land X \in B) \to K \in OP$
11	1 2	op0cl	$⊢ K \in OP \to \underset{˙}{0} \in B$
12	10 11	syl	$⊢ (K \in HL \land X \in B) \to \underset{˙}{0} \in B$
13	1 3	pmap11	$⊢ (K \in HL \land X \in B \land \underset{˙}{0} \in B) \to (M (X) = M (\underset{˙}{0}) \leftrightarrow X = \underset{˙}{0})$
14	12 13	mpd3an3	$⊢ (K \in HL \land X \in B) \to (M (X) = M (\underset{˙}{0}) \leftrightarrow X = \underset{˙}{0})$
15	8 14	bitr3d	$⊢ (K \in HL \land X \in B) \to (M (X) = \emptyset \leftrightarrow X = \underset{˙}{0})$

Metamath Proof Explorer