Metamath Proof Explorer


Theorem lss0v

Description: The zero vector in a submodule equals the zero vector in the including module. (Contributed by NM, 15-Mar-2015)

Ref Expression
Hypotheses lss0v.x X=W𝑠U
lss0v.o 0˙=0W
lss0v.z Z=0X
lss0v.l L=LSubSpW
Assertion lss0v WLModULZ=0˙

Proof

Step Hyp Ref Expression
1 lss0v.x X=W𝑠U
2 lss0v.o 0˙=0W
3 lss0v.z Z=0X
4 lss0v.l L=LSubSpW
5 0ss U
6 eqid LSpanW=LSpanW
7 eqid LSpanX=LSpanX
8 1 6 7 4 lsslsp WLModULULSpanX=LSpanW
9 5 8 mp3an3 WLModULLSpanX=LSpanW
10 1 4 lsslmod WLModULXLMod
11 3 7 lsp0 XLModLSpanX=Z
12 10 11 syl WLModULLSpanX=Z
13 2 6 lsp0 WLModLSpanW=0˙
14 13 adantr WLModULLSpanW=0˙
15 9 12 14 3eqtr3d WLModULZ=0˙
16 15 unieqd WLModULZ=0˙
17 3 fvexi ZV
18 17 unisn Z=Z
19 2 fvexi 0˙V
20 19 unisn 0˙=0˙
21 16 18 20 3eqtr3g WLModULZ=0˙