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	⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
	lss0v.o	⊢ 0 = ( 0g ‘ 𝑊 )
	lss0v.z	⊢ 𝑍 = ( 0g ‘ 𝑋 )
	lss0v.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
Assertion	lss0v	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → 𝑍 = 0 )

Proof

Step	Hyp	Ref	Expression
1		lss0v.x	⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
2		lss0v.o	⊢ 0 = ( 0g ‘ 𝑊 )
3		lss0v.z	⊢ 𝑍 = ( 0g ‘ 𝑋 )
4		lss0v.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
5		0ss	⊢ ∅ ⊆ 𝑈
6		eqid	⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
7		eqid	⊢ ( LSpan ‘ 𝑋 ) = ( LSpan ‘ 𝑋 )
8	1 6 7 4	lsslsp	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ ∅ ⊆ 𝑈 ) → ( ( LSpan ‘ 𝑊 ) ‘ ∅ ) = ( ( LSpan ‘ 𝑋 ) ‘ ∅ ) )
9	5 8	mp3an3	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → ( ( LSpan ‘ 𝑊 ) ‘ ∅ ) = ( ( LSpan ‘ 𝑋 ) ‘ ∅ ) )
10	2 6	lsp0	⊢ ( 𝑊 ∈ LMod → ( ( LSpan ‘ 𝑊 ) ‘ ∅ ) = { 0 } )
11	10	adantr	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → ( ( LSpan ‘ 𝑊 ) ‘ ∅ ) = { 0 } )
12	1 4	lsslmod	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → 𝑋 ∈ LMod )
13	3 7	lsp0	⊢ ( 𝑋 ∈ LMod → ( ( LSpan ‘ 𝑋 ) ‘ ∅ ) = { 𝑍 } )
14	12 13	syl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → ( ( LSpan ‘ 𝑋 ) ‘ ∅ ) = { 𝑍 } )
15	9 11 14	3eqtr3rd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → { 𝑍 } = { 0 } )
16	15	unieqd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → ∪ { 𝑍 } = ∪ { 0 } )
17	3	fvexi	⊢ 𝑍 ∈ V
18	17	unisn	⊢ ∪ { 𝑍 } = 𝑍
19	2	fvexi	⊢ 0 ∈ V
20	19	unisn	⊢ ∪ { 0 } = 0
21	16 18 20	3eqtr3g	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → 𝑍 = 0 )