Theorem lssuni

Description: The union of all subspaces is the vector space. (Contributed by NM, 13-Mar-2015)

	Ref	Expression
Hypotheses	lssss.v	|- V = ( Base ` W )
	lssss.s	|- S = ( LSubSp ` W )
	lssuni.w	|- ( ph -> W e. LMod )
Assertion	lssuni	|- ( ph -> U. S = V )

Proof

Step	Hyp	Ref	Expression
1		lssss.v	|- V = ( Base ` W )
2		lssss.s	|- S = ( LSubSp ` W )
3		lssuni.w	|- ( ph -> W e. LMod )
4		rabid2	|- ( S = { x e. S | x C_ V } <-> A. x e. S x C_ V )
5	1 2	lssss	|- ( x e. S -> x C_ V )
6	4 5	mprgbir	|- S = { x e. S | x C_ V }
7	6	unieqi	|- U. S = U. { x e. S | x C_ V }
8	1 2	lss1	|- ( W e. LMod -> V e. S )
9		unimax	|- ( V e. S -> U. { x e. S | x C_ V } = V )
10	3 8 9	3syl	|- ( ph -> U. { x e. S | x C_ V } = V )
11	7 10	eqtrid	|- ( ph -> U. S = V )