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 = ( 0_g ‘ 𝑊 )
	lspun0.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lspun0.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lspun0.x	⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
Assertion	lspun0	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑋 ∪ { 0 } ) ) = ( 𝑁 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		lspun0.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspun0.o	⊢ 0 = ( 0_g ‘ 𝑊 )
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 } ) ) = ( 𝑁 ‘ 𝑋 ) )

Metamath Proof Explorer

Theorem lspun0

Proof