This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lspuni0

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

	Ref	Expression
Hypotheses	lspsn0.z	$⊢ \underset{˙}{0} = 0_{W}$
	lspsn0.n	$⊢ N = LSpan (W)$
Assertion	lspuni0	$⊢ W \in LMod \to ⋃ N (\emptyset) = \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		lspsn0.z	$⊢ \underset{˙}{0} = 0_{W}$
2		lspsn0.n	$⊢ N = LSpan (W)$
3	1 2	lsp0	$⊢ W \in LMod \to N (\emptyset) = \{\underset{˙}{0}\}$
4	3	unieqd	$⊢ W \in LMod \to ⋃ N (\emptyset) = ⋃ \{\underset{˙}{0}\}$
5	1	fvexi	$⊢ \underset{˙}{0} \in V$
6	5	unisn	$⊢ ⋃ \{\underset{˙}{0}\} = \underset{˙}{0}$
7	4 6	eqtrdi	$⊢ W \in LMod \to ⋃ N (\emptyset) = \underset{˙}{0}$