Theorem lssats2

Description: A way to express atomisticity (a subspace is the union of its atoms). (Contributed by NM, 3-Feb-2015)

	Ref	Expression
Hypotheses	lssats2.s	|- S = ( LSubSp ` W )
	lssats2.n	|- N = ( LSpan ` W )
	lssats2.w	|- ( ph -> W e. LMod )
	lssats2.u	|- ( ph -> U e. S )
Assertion	lssats2	|- ( ph -> U = U_ x e. U ( N ` { x } ) )

Proof

Step	Hyp	Ref	Expression
1		lssats2.s	|- S = ( LSubSp ` W )
2		lssats2.n	|- N = ( LSpan ` W )
3		lssats2.w	|- ( ph -> W e. LMod )
4		lssats2.u	|- ( ph -> U e. S )
5		simpr	|- ( ( ph /\ y e. U ) -> y e. U )
6	3	adantr	|- ( ( ph /\ y e. U ) -> W e. LMod )
7		eqid	|- ( Base ` W ) = ( Base ` W )
8	7 1	lssel	|- ( ( U e. S /\ y e. U ) -> y e. ( Base ` W ) )
9	4 8	sylan	|- ( ( ph /\ y e. U ) -> y e. ( Base ` W ) )
10	7 2	lspsnid	|- ( ( W e. LMod /\ y e. ( Base ` W ) ) -> y e. ( N ` { y } ) )
11	6 9 10	syl2anc	|- ( ( ph /\ y e. U ) -> y e. ( N ` { y } ) )
12		sneq	|- ( x = y -> { x } = { y } )
13	12	fveq2d	|- ( x = y -> ( N ` { x } ) = ( N ` { y } ) )
14	13	eleq2d	|- ( x = y -> ( y e. ( N ` { x } ) <-> y e. ( N ` { y } ) ) )
15	14	rspcev	|- ( ( y e. U /\ y e. ( N ` { y } ) ) -> E. x e. U y e. ( N ` { x } ) )
16	5 11 15	syl2anc	|- ( ( ph /\ y e. U ) -> E. x e. U y e. ( N ` { x } ) )
17	16	ex	|- ( ph -> ( y e. U -> E. x e. U y e. ( N ` { x } ) ) )
18	3	adantr	|- ( ( ph /\ x e. U ) -> W e. LMod )
19	4	adantr	|- ( ( ph /\ x e. U ) -> U e. S )
20		simpr	|- ( ( ph /\ x e. U ) -> x e. U )
21	1 2 18 19 20	ellspsn5	|- ( ( ph /\ x e. U ) -> ( N ` { x } ) C_ U )
22	21	sseld	|- ( ( ph /\ x e. U ) -> ( y e. ( N ` { x } ) -> y e. U ) )
23	22	rexlimdva	|- ( ph -> ( E. x e. U y e. ( N ` { x } ) -> y e. U ) )
24	17 23	impbid	|- ( ph -> ( y e. U <-> E. x e. U y e. ( N ` { x } ) ) )
25		eliun	|- ( y e. U_ x e. U ( N ` { x } ) <-> E. x e. U y e. ( N ` { x } ) )
26	24 25	bitr4di	|- ( ph -> ( y e. U <-> y e. U_ x e. U ( N ` { x } ) ) )
27	26	eqrdv	|- ( ph -> U = U_ x e. U ( N ` { x } ) )