This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 1 4 lsslmod ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → 𝑋 ∈ LMod )
11 3 7 lsp0 ⊢ ( 𝑋 ∈ LMod → ( ( LSpan ‘ 𝑋 ) ‘ ∅ ) = { 𝑍 } )
12 10 11 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → ( ( LSpan ‘ 𝑋 ) ‘ ∅ ) = { 𝑍 } )
13 2 6 lsp0 ⊢ ( 𝑊 ∈ LMod → ( ( LSpan ‘ 𝑊 ) ‘ ∅ ) = { 0 } )
14 13 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → ( ( LSpan ‘ 𝑊 ) ‘ ∅ ) = { 0 } )
15 9 12 14 3eqtr3d ⊢ ( ( 𝑊 ∈ 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 )