Theorem lspuni0

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

	Ref	Expression
Hypotheses	lspsn0.z	⊢ 0 = ( 0g ‘ 𝑊 )
	lspsn0.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion	lspuni0	⊢ ( 𝑊 ∈ LMod → ∪ ( 𝑁 ‘ ∅ ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		lspsn0.z	⊢ 0 = ( 0g ‘ 𝑊 )
2		lspsn0.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3	1 2	lsp0	⊢ ( 𝑊 ∈ LMod → ( 𝑁 ‘ ∅ ) = { 0 } )
4	3	unieqd	⊢ ( 𝑊 ∈ LMod → ∪ ( 𝑁 ‘ ∅ ) = ∪ { 0 } )
5	1	fvexi	⊢ 0 ∈ V
6	5	unisn	⊢ ∪ { 0 } = 0
7	4 6	eqtrdi	⊢ ( 𝑊 ∈ LMod → ∪ ( 𝑁 ‘ ∅ ) = 0 )