lplnn0N

Description: A lattice plane is nonzero. (Contributed by NM, 15-Jul-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lplnn0.z	$⊢ \underset{˙}{0} = 0. (K)$
	lplnn0.p	$⊢ P = LPlanes (K)$
Assertion	lplnn0N	$⊢ (K \in HL \land X \in P) \to X \neq \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		lplnn0.z	$⊢ \underset{˙}{0} = 0. (K)$
2		lplnn0.p	$⊢ P = LPlanes (K)$
3		eqid	$⊢ Atoms (K) = Atoms (K)$
4	3	atex	$⊢ K \in HL \to Atoms (K) \neq \emptyset$
5		n0	$⊢ Atoms (K) \neq \emptyset \leftrightarrow \exists p p \in Atoms (K)$
6	4 5	sylib	$⊢ K \in HL \to \exists p p \in Atoms (K)$
7	6	adantr	$⊢ (K \in HL \land X \in P) \to \exists p p \in Atoms (K)$
8		eqid	$⊢ \leq_{K} = \leq_{K}$
9	8 3 2	lplnnleat	$⊢ (K \in HL \land X \in P \land p \in Atoms (K)) \to \neg X \leq_{K} p$
10	9	3expa	$⊢ ((K \in HL \land X \in P) \land p \in Atoms (K)) \to \neg X \leq_{K} p$
11		hlop	$⊢ K \in HL \to K \in OP$
12	11	ad2antrr	$⊢ ((K \in HL \land X \in P) \land p \in Atoms (K)) \to K \in OP$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14	13 3	atbase	$⊢ p \in Atoms (K) \to p \in {Base}_{K}$
15	14	adantl	$⊢ ((K \in HL \land X \in P) \land p \in Atoms (K)) \to p \in {Base}_{K}$
16	13 8 1	op0le	$⊢ (K \in OP \land p \in {Base}_{K}) \to \underset{˙}{0} \leq_{K} p$
17	12 15 16	syl2anc	$⊢ ((K \in HL \land X \in P) \land p \in Atoms (K)) \to \underset{˙}{0} \leq_{K} p$
18		breq1	$⊢ X = \underset{˙}{0} \to (X \leq_{K} p \leftrightarrow \underset{˙}{0} \leq_{K} p)$
19	17 18	syl5ibrcom	$⊢ ((K \in HL \land X \in P) \land p \in Atoms (K)) \to (X = \underset{˙}{0} \to X \leq_{K} p)$
20	19	necon3bd	$⊢ ((K \in HL \land X \in P) \land p \in Atoms (K)) \to (\neg X \leq_{K} p \to X \neq \underset{˙}{0})$
21	10 20	mpd	$⊢ ((K \in HL \land X \in P) \land p \in Atoms (K)) \to X \neq \underset{˙}{0}$
22	7 21	exlimddv	$⊢ (K \in HL \land X \in P) \to X \neq \underset{˙}{0}$

Metamath Proof Explorer

Theorem lplnn0N

Proof