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 0 ˙ = 0 W
lspsn0.n N = LSpan W
Assertion lspuni0 W LMod N = 0 ˙

Proof

Step Hyp Ref Expression
1 lspsn0.z 0 ˙ = 0 W
2 lspsn0.n N = LSpan W
3 1 2 lsp0 W LMod N = 0 ˙
4 3 unieqd W LMod N = 0 ˙
5 1 fvexi 0 ˙ V
6 5 unisn 0 ˙ = 0 ˙
7 4 6 eqtrdi W LMod N = 0 ˙