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 ˙ = 0 W
lss0v.z Z = 0 X
lss0v.l L = LSubSp W
Assertion lss0v W LMod U L Z = 0 ˙

Proof

Step Hyp Ref Expression
1 lss0v.x X = W 𝑠 U
2 lss0v.o 0 ˙ = 0 W
3 lss0v.z Z = 0 X
4 lss0v.l L = LSubSp W
5 0ss U
6 eqid LSpan W = LSpan W
7 eqid LSpan X = LSpan X
8 1 6 7 4 lsslsp W LMod U L U LSpan W = LSpan X
9 5 8 mp3an3 W LMod U L LSpan W = LSpan X
10 2 6 lsp0 W LMod LSpan W = 0 ˙
11 10 adantr W LMod U L LSpan W = 0 ˙
12 1 4 lsslmod W LMod U L X LMod
13 3 7 lsp0 X LMod LSpan X = Z
14 12 13 syl W LMod U L LSpan X = Z
15 9 11 14 3eqtr3rd W LMod U L Z = 0 ˙
16 15 unieqd W LMod U L Z = 0 ˙
17 3 fvexi Z V
18 17 unisn Z = Z
19 2 fvexi 0 ˙ V
20 19 unisn 0 ˙ = 0 ˙
21 16 18 20 3eqtr3g W LMod U L Z = 0 ˙