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 ⁡ X ⁡ ∅ = LSpan ⁡ W ⁡ ∅
9 5 8 mp3an3 ⊢ W ∈ LMod ∧ U ∈ L → LSpan ⁡ X ⁡ ∅ = LSpan ⁡ W ⁡ ∅
10 1 4 lsslmod ⊢ W ∈ LMod ∧ U ∈ L → X ∈ LMod
11 3 7 lsp0 ⊢ X ∈ LMod → LSpan ⁡ X ⁡ ∅ = Z
12 10 11 syl ⊢ W ∈ LMod ∧ U ∈ L → LSpan ⁡ X ⁡ ∅ = Z
13 2 6 lsp0 ⊢ W ∈ LMod → LSpan ⁡ W ⁡ ∅ = 0 ˙
14 13 adantr ⊢ W ∈ LMod ∧ U ∈ L → LSpan ⁡ W ⁡ ∅ = 0 ˙
15 9 12 14 3eqtr3d ⊢ 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 ˙