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	|- X = ( W |`s U )
	lss0v.o	|- .0. = ( 0g ` W )
	lss0v.z	|- Z = ( 0g ` X )
	lss0v.l	|- L = ( LSubSp ` W )
Assertion	lss0v	|- ( ( W e. LMod /\ U e. L ) -> Z = .0. )

Proof

Step	Hyp	Ref	Expression
1		lss0v.x	|- X = ( W |`s U )
2		lss0v.o	|- .0. = ( 0g ` W )
3		lss0v.z	|- Z = ( 0g ` X )
4		lss0v.l	|- L = ( LSubSp ` W )
5		0ss	|- (/) C_ U
6		eqid	|- ( LSpan ` W ) = ( LSpan ` W )
7		eqid	|- ( LSpan ` X ) = ( LSpan ` X )
8	1 6 7 4	lsslsp	|- ( ( W e. LMod /\ U e. L /\ (/) C_ U ) -> ( ( LSpan ` W ) ` (/) ) = ( ( LSpan ` X ) ` (/) ) )
9	5 8	mp3an3	|- ( ( W e. LMod /\ U e. L ) -> ( ( LSpan ` W ) ` (/) ) = ( ( LSpan ` X ) ` (/) ) )
10	2 6	lsp0	|- ( W e. LMod -> ( ( LSpan ` W ) ` (/) ) = { .0. } )
11	10	adantr	|- ( ( W e. LMod /\ U e. L ) -> ( ( LSpan ` W ) ` (/) ) = { .0. } )
12	1 4	lsslmod	|- ( ( W e. LMod /\ U e. L ) -> X e. LMod )
13	3 7	lsp0	|- ( X e. LMod -> ( ( LSpan ` X ) ` (/) ) = { Z } )
14	12 13	syl	|- ( ( W e. LMod /\ U e. L ) -> ( ( LSpan ` X ) ` (/) ) = { Z } )
15	9 11 14	3eqtr3rd	|- ( ( W e. LMod /\ U e. L ) -> { Z } = { .0. } )
16	15	unieqd	|- ( ( W e. LMod /\ U e. L ) -> U. { Z } = U. { .0. } )
17	3	fvexi	|- Z e. _V
18	17	unisn	|- U. { Z } = Z
19	2	fvexi	|- .0. e. _V
20	19	unisn	|- U. { .0. } = .0.
21	16 18 20	3eqtr3g	|- ( ( W e. LMod /\ U e. L ) -> Z = .0. )