Theorem lspuni0

Description: Union of the span of the empty set. (Contributed by NM, 14-Mar-2015)

	Ref	Expression
Hypotheses	lspsn0.z	|- .0. = ( 0g ` W )
	lspsn0.n	|- N = ( LSpan ` W )
Assertion	lspuni0	|- ( W e. LMod -> U. ( N ` (/) ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		lspsn0.z	|- .0. = ( 0g ` W )
2		lspsn0.n	|- N = ( LSpan ` W )
3	1 2	lsp0	|- ( W e. LMod -> ( N ` (/) ) = { .0. } )
4	3	unieqd	|- ( W e. LMod -> U. ( N ` (/) ) = U. { .0. } )
5	1	fvexi	|- .0. e. _V
6	5	unisn	|- U. { .0. } = .0.
7	4 6	eqtrdi	|- ( W e. LMod -> U. ( N ` (/) ) = .0. )