Metamath Proof Explorer

Theorem lspun0

Description: The span of a union with the zero subspace. (Contributed by NM, 22-May-2015)

Ref Expression
Hypotheses lspun0.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspun0.o ⊢ 0 = ( 0g ‘ 𝑊 )
lspun0.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lspun0.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lspun0.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
Assertion lspun0 ( 𝜑 → ( 𝑁 ‘ ( 𝑋 ∪ { 0 } ) ) = ( 𝑁 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 lspun0.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspun0.o ⊢ 0 = ( 0g ‘ 𝑊 )
3 lspun0.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lspun0.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
5 lspun0.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
6 1 2 lmod0vcl ⊢ ( 𝑊 ∈ LMod → 0 ∈ 𝑉 )
7 4 6 syl ⊢ ( 𝜑 → 0 ∈ 𝑉 )
8 7 snssd ⊢ ( 𝜑 → { 0 } ⊆ 𝑉 )
9 1 3 lspun ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ⊆ 𝑉 ∧ { 0 } ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝑋 ∪ { 0 } ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ 𝑋 ) ∪ ( 𝑁 ‘ { 0 } ) ) ) )
10 4 5 8 9 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑋 ∪ { 0 } ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ 𝑋 ) ∪ ( 𝑁 ‘ { 0 } ) ) ) )
11 2 3 lspsn0 ⊢ ( 𝑊 ∈ LMod → ( 𝑁 ‘ { 0 } ) = { 0 } )
12 4 11 syl ⊢ ( 𝜑 → ( 𝑁 ‘ { 0 } ) = { 0 } )
13 12 uneq2d ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) ∪ ( 𝑁 ‘ { 0 } ) ) = ( ( 𝑁 ‘ 𝑋 ) ∪ { 0 } ) )
14 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
15 1 14 3 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑊 ) )
16 4 5 15 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑊 ) )
17 2 14 lss0ss ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑊 ) ) → { 0 } ⊆ ( 𝑁 ‘ 𝑋 ) )
18 4 16 17 syl2anc ⊢ ( 𝜑 → { 0 } ⊆ ( 𝑁 ‘ 𝑋 ) )
19 ssequn2 ⊢ ( { 0 } ⊆ ( 𝑁 ‘ 𝑋 ) ↔ ( ( 𝑁 ‘ 𝑋 ) ∪ { 0 } ) = ( 𝑁 ‘ 𝑋 ) )
20 18 19 sylib ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) ∪ { 0 } ) = ( 𝑁 ‘ 𝑋 ) )
21 13 20 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) ∪ ( 𝑁 ‘ { 0 } ) ) = ( 𝑁 ‘ 𝑋 ) )
22 21 fveq2d ⊢ ( 𝜑 → ( 𝑁 ‘ ( ( 𝑁 ‘ 𝑋 ) ∪ ( 𝑁 ‘ { 0 } ) ) ) = ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) )
23 1 3 lspidm ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = ( 𝑁 ‘ 𝑋 ) )
24 4 5 23 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = ( 𝑁 ‘ 𝑋 ) )
25 22 24 eqtrd ⊢ ( 𝜑 → ( 𝑁 ‘ ( ( 𝑁 ‘ 𝑋 ) ∪ ( 𝑁 ‘ { 0 } ) ) ) = ( 𝑁 ‘ 𝑋 ) )
26 10 25 eqtrd ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑋 ∪ { 0 } ) ) = ( 𝑁 ‘ 𝑋 ) )