Theorem lspsslco

Description: Lemma for lspeqlco . (Contributed by AV, 17-Apr-2019)

	Ref	Expression
Hypothesis	lspeqvlco.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
Assertion	lspsslco	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( ( LSpan ‘ 𝑀 ) ‘ 𝑉 ) ⊆ ( 𝑀 LinCo 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		lspeqvlco.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		simpl	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑀 ∈ LMod )
3	1	pweqi	⊢ 𝒫 𝐵 = 𝒫 ( Base ‘ 𝑀 )
4	3	eleq2i	⊢ ( 𝑉 ∈ 𝒫 𝐵 ↔ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
5		lincolss	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑀 LinCo 𝑉 ) ∈ ( LSubSp ‘ 𝑀 ) )
6	4 5	sylan2b	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 LinCo 𝑉 ) ∈ ( LSubSp ‘ 𝑀 ) )
7		lcoss	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑉 ⊆ ( 𝑀 LinCo 𝑉 ) )
8	4 7	sylan2b	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑉 ⊆ ( 𝑀 LinCo 𝑉 ) )
9		eqid	⊢ ( LSubSp ‘ 𝑀 ) = ( LSubSp ‘ 𝑀 )
10		eqid	⊢ ( LSpan ‘ 𝑀 ) = ( LSpan ‘ 𝑀 )
11	9 10	lspssp	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑀 LinCo 𝑉 ) ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ ( 𝑀 LinCo 𝑉 ) ) → ( ( LSpan ‘ 𝑀 ) ‘ 𝑉 ) ⊆ ( 𝑀 LinCo 𝑉 ) )
12	2 6 8 11	syl3anc	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( ( LSpan ‘ 𝑀 ) ‘ 𝑉 ) ⊆ ( 𝑀 LinCo 𝑉 ) )