Theorem lplnn0N

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

	Ref	Expression
Hypotheses	lplnn0.z	|- .0. = ( 0. ` K )
	lplnn0.p	|- P = ( LPlanes ` K )
Assertion	lplnn0N	|- ( ( K e. HL /\ X e. P ) -> X =/= .0. )

Proof

Step	Hyp	Ref	Expression
1		lplnn0.z	|- .0. = ( 0. ` K )
2		lplnn0.p	|- P = ( LPlanes ` K )
3		eqid	|- ( Atoms ` K ) = ( Atoms ` K )
4	3	atex	|- ( K e. HL -> ( Atoms ` K ) =/= (/) )
5		n0	|- ( ( Atoms ` K ) =/= (/) <-> E. p p e. ( Atoms ` K ) )
6	4 5	sylib	|- ( K e. HL -> E. p p e. ( Atoms ` K ) )
7	6	adantr	|- ( ( K e. HL /\ X e. P ) -> E. p p e. ( Atoms ` K ) )
8		eqid	|- ( le ` K ) = ( le ` K )
9	8 3 2	lplnnleat	|- ( ( K e. HL /\ X e. P /\ p e. ( Atoms ` K ) ) -> -. X ( le ` K ) p )
10	9	3expa	|- ( ( ( K e. HL /\ X e. P ) /\ p e. ( Atoms ` K ) ) -> -. X ( le ` K ) p )
11		hlop	|- ( K e. HL -> K e. OP )
12	11	ad2antrr	|- ( ( ( K e. HL /\ X e. P ) /\ p e. ( Atoms ` K ) ) -> K e. OP )
13		eqid	|- ( Base ` K ) = ( Base ` K )
14	13 3	atbase	|- ( p e. ( Atoms ` K ) -> p e. ( Base ` K ) )
15	14	adantl	|- ( ( ( K e. HL /\ X e. P ) /\ p e. ( Atoms ` K ) ) -> p e. ( Base ` K ) )
16	13 8 1	op0le	|- ( ( K e. OP /\ p e. ( Base ` K ) ) -> .0. ( le ` K ) p )
17	12 15 16	syl2anc	|- ( ( ( K e. HL /\ X e. P ) /\ p e. ( Atoms ` K ) ) -> .0. ( le ` K ) p )
18		breq1	|- ( X = .0. -> ( X ( le ` K ) p <-> .0. ( le ` K ) p ) )
19	17 18	syl5ibrcom	|- ( ( ( K e. HL /\ X e. P ) /\ p e. ( Atoms ` K ) ) -> ( X = .0. -> X ( le ` K ) p ) )
20	19	necon3bd	|- ( ( ( K e. HL /\ X e. P ) /\ p e. ( Atoms ` K ) ) -> ( -. X ( le ` K ) p -> X =/= .0. ) )
21	10 20	mpd	|- ( ( ( K e. HL /\ X e. P ) /\ p e. ( Atoms ` K ) ) -> X =/= .0. )
22	7 21	exlimddv	|- ( ( K e. HL /\ X e. P ) -> X =/= .0. )