Theorem lplnbase

Description: A lattice plane is a lattice element. (Contributed by NM, 17-Jun-2012)

	Ref	Expression
Hypotheses	lplnbase.b	|- B = ( Base ` K )
	lplnbase.p	|- P = ( LPlanes ` K )
Assertion	lplnbase	|- ( X e. P -> X e. B )

Proof

Step	Hyp	Ref	Expression
1		lplnbase.b	|- B = ( Base ` K )
2		lplnbase.p	|- P = ( LPlanes ` K )
3		n0i	|- ( X e. P -> -. P = (/) )
4	2	eqeq1i	|- ( P = (/) <-> ( LPlanes ` K ) = (/) )
5	3 4	sylnib	|- ( X e. P -> -. ( LPlanes ` K ) = (/) )
6		fvprc	|- ( -. K e. _V -> ( LPlanes ` K ) = (/) )
7	5 6	nsyl2	|- ( X e. P -> K e. _V )
8		eqid	|- (
9		eqid	|- ( LLines ` K ) = ( LLines ` K )
10	1 8 9 2	islpln	|- ( K e. _V -> ( X e. P <-> ( X e. B /\ E. x e. ( LLines ` K ) x (
11	10	simprbda	|- ( ( K e. _V /\ X e. P ) -> X e. B )
12	7 11	mpancom	|- ( X e. P -> X e. B )