Theorem lspuni0

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

	Ref	Expression
Hypotheses	lspsn0.z	$$⊢\underset{\dot{}}{0}=0_W$$
	lspsn0.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
Assertion	lspuni0	$$⊢W\in \mathrm{LMod}\to \bigcup N\left(\varnothing \right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		lspsn0.z	$$⊢\underset{\dot{}}{0}=0_W$$
2		lspsn0.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
3	1 2	lsp0	$$⊢W\in \mathrm{LMod}\to N\left(\varnothing \right)=\left\{\underset{\dot{}}{0}\right\}$$
4	3	unieqd	$$⊢W\in \mathrm{LMod}\to \bigcup N\left(\varnothing \right)=\bigcup \left\{\underset{\dot{}}{0}\right\}$$
5	1	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
6	5	unisn	$$⊢\bigcup \left\{\underset{\dot{}}{0}\right\}=\underset{\dot{}}{0}$$
7	4 6	eqtrdi	$$⊢W\in \mathrm{LMod}\to \bigcup N\left(\varnothing \right)=\underset{\dot{}}{0}$$