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 𝑋 = ( 𝑊s 𝑈 )
lss0v.o 0 = ( 0g𝑊 )
lss0v.z 𝑍 = ( 0g𝑋 )
lss0v.l 𝐿 = ( LSubSp ‘ 𝑊 )
Assertion lss0v ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿 ) → 𝑍 = 0 )

Proof

Step Hyp Ref Expression
1 lss0v.x 𝑋 = ( 𝑊s 𝑈 )
2 lss0v.o 0 = ( 0g𝑊 )
3 lss0v.z 𝑍 = ( 0g𝑋 )
4 lss0v.l 𝐿 = ( LSubSp ‘ 𝑊 )
5 0ss ∅ ⊆ 𝑈
6 eqid ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
7 eqid ( LSpan ‘ 𝑋 ) = ( LSpan ‘ 𝑋 )
8 1 6 7 4 lsslsp ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿 ∧ ∅ ⊆ 𝑈 ) → ( ( LSpan ‘ 𝑊 ) ‘ ∅ ) = ( ( LSpan ‘ 𝑋 ) ‘ ∅ ) )
9 5 8 mp3an3 ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿 ) → ( ( LSpan ‘ 𝑊 ) ‘ ∅ ) = ( ( LSpan ‘ 𝑋 ) ‘ ∅ ) )
10 2 6 lsp0 ( 𝑊 ∈ LMod → ( ( LSpan ‘ 𝑊 ) ‘ ∅ ) = { 0 } )
11 10 adantr ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿 ) → ( ( LSpan ‘ 𝑊 ) ‘ ∅ ) = { 0 } )
12 1 4 lsslmod ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿 ) → 𝑋 ∈ LMod )
13 3 7 lsp0 ( 𝑋 ∈ LMod → ( ( LSpan ‘ 𝑋 ) ‘ ∅ ) = { 𝑍 } )
14 12 13 syl ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿 ) → ( ( LSpan ‘ 𝑋 ) ‘ ∅ ) = { 𝑍 } )
15 9 11 14 3eqtr3rd ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿 ) → { 𝑍 } = { 0 } )
16 15 unieqd ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿 ) → { 𝑍 } = { 0 } )
17 3 fvexi 𝑍 ∈ V
18 17 unisn { 𝑍 } = 𝑍
19 2 fvexi 0 ∈ V
20 19 unisn { 0 } = 0
21 16 18 20 3eqtr3g ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿 ) → 𝑍 = 0 )