Theorem 0ellsp

Description: Zero is in all spans. (Contributed by Thierry Arnoux, 8-May-2023)

	Ref	Expression
Hypotheses	0ellsp.1	⊢ 0 = ( 0g ‘ 𝑊 )
	0ellsp.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	0ellsp.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion	0ellsp	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ⊆ 𝐵 ) → 0 ∈ ( 𝑁 ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		0ellsp.1	⊢ 0 = ( 0g ‘ 𝑊 )
2		0ellsp.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
3		0ellsp.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
5	2 4 3	lspcl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑁 ‘ 𝑆 ) ∈ ( LSubSp ‘ 𝑊 ) )
6	1 4	lss0cl	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝑆 ) ∈ ( LSubSp ‘ 𝑊 ) ) → 0 ∈ ( 𝑁 ‘ 𝑆 ) )
7	5 6	syldan	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ⊆ 𝐵 ) → 0 ∈ ( 𝑁 ‘ 𝑆 ) )