Theorem islsat

Description: The predicate "is a 1-dim subspace (atom)" (of a left module or left vector space). (Contributed by NM, 9-Apr-2014) (Revised by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Hypotheses	lsatset.v	|- V = ( Base ` W )
	lsatset.n	|- N = ( LSpan ` W )
	lsatset.z	|- .0. = ( 0g ` W )
	lsatset.a	|- A = ( LSAtoms ` W )
Assertion	islsat	|- ( W e. X -> ( U e. A <-> E. x e. ( V \ { .0. } ) U = ( N ` { x } ) ) )

Proof

Step	Hyp	Ref	Expression
1		lsatset.v	|- V = ( Base ` W )
2		lsatset.n	|- N = ( LSpan ` W )
3		lsatset.z	|- .0. = ( 0g ` W )
4		lsatset.a	|- A = ( LSAtoms ` W )
5	1 2 3 4	lsatset	|- ( W e. X -> A = ran ( x e. ( V \ { .0. } ) |-> ( N ` { x } ) ) )
6	5	eleq2d	|- ( W e. X -> ( U e. A <-> U e. ran ( x e. ( V \ { .0. } ) |-> ( N ` { x } ) ) ) )
7		eqid	|- ( x e. ( V \ { .0. } ) |-> ( N ` { x } ) ) = ( x e. ( V \ { .0. } ) |-> ( N ` { x } ) )
8		fvex	|- ( N ` { x } ) e. _V
9	7 8	elrnmpti	|- ( U e. ran ( x e. ( V \ { .0. } ) |-> ( N ` { x } ) ) <-> E. x e. ( V \ { .0. } ) U = ( N ` { x } ) )
10	6 9	bitrdi	|- ( W e. X -> ( U e. A <-> E. x e. ( V \ { .0. } ) U = ( N ` { x } ) ) )