Theorem 0ellsp

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

	Ref	Expression
Hypotheses	0ellsp.1	|- .0. = ( 0g ` W )
	0ellsp.b	|- B = ( Base ` W )
	0ellsp.n	|- N = ( LSpan ` W )
Assertion	0ellsp	|- ( ( W e. LMod /\ S C_ B ) -> .0. e. ( N ` S ) )

Proof

Step	Hyp	Ref	Expression
1		0ellsp.1	|- .0. = ( 0g ` W )
2		0ellsp.b	|- B = ( Base ` W )
3		0ellsp.n	|- N = ( LSpan ` W )
4		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
5	2 4 3	lspcl	|- ( ( W e. LMod /\ S C_ B ) -> ( N ` S ) e. ( LSubSp ` W ) )
6	1 4	lss0cl	|- ( ( W e. LMod /\ ( N ` S ) e. ( LSubSp ` W ) ) -> .0. e. ( N ` S ) )
7	5 6	syldan	|- ( ( W e. LMod /\ S C_ B ) -> .0. e. ( N ` S ) )