Metamath Proof Explorer


Theorem lspun0

Description: The span of a union with the zero subspace. (Contributed by NM, 22-May-2015)

Ref Expression
Hypotheses lspun0.v V = Base W
lspun0.o 0 ˙ = 0 W
lspun0.n N = LSpan W
lspun0.w φ W LMod
lspun0.x φ X V
Assertion lspun0 φ N X 0 ˙ = N X

Proof

Step Hyp Ref Expression
1 lspun0.v V = Base W
2 lspun0.o 0 ˙ = 0 W
3 lspun0.n N = LSpan W
4 lspun0.w φ W LMod
5 lspun0.x φ X V
6 1 2 lmod0vcl W LMod 0 ˙ V
7 4 6 syl φ 0 ˙ V
8 7 snssd φ 0 ˙ V
9 1 3 lspun W LMod X V 0 ˙ V N X 0 ˙ = N N X N 0 ˙
10 4 5 8 9 syl3anc φ N X 0 ˙ = N N X N 0 ˙
11 2 3 lspsn0 W LMod N 0 ˙ = 0 ˙
12 4 11 syl φ N 0 ˙ = 0 ˙
13 12 uneq2d φ N X N 0 ˙ = N X 0 ˙
14 eqid LSubSp W = LSubSp W
15 1 14 3 lspcl W LMod X V N X LSubSp W
16 4 5 15 syl2anc φ N X LSubSp W
17 2 14 lss0ss W LMod N X LSubSp W 0 ˙ N X
18 4 16 17 syl2anc φ 0 ˙ N X
19 ssequn2 0 ˙ N X N X 0 ˙ = N X
20 18 19 sylib φ N X 0 ˙ = N X
21 13 20 eqtrd φ N X N 0 ˙ = N X
22 21 fveq2d φ N N X N 0 ˙ = N N X
23 1 3 lspidm W LMod X V N N X = N X
24 4 5 23 syl2anc φ N N X = N X
25 22 24 eqtrd φ N N X N 0 ˙ = N X
26 10 25 eqtrd φ N X 0 ˙ = N X