Metamath Proof Explorer

Theorem lcosslsp

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

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

Proof

Step Hyp Ref Expression
1 lspeqvlco.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 ellcoellss ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑠 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑠 ) → ∀ 𝑦 ∈ ( 𝑀 LinCo 𝑉 ) 𝑦 ∈ 𝑠 )
3 2 3exp ⊢ ( 𝑀 ∈ LMod → ( 𝑠 ∈ ( LSubSp ‘ 𝑀 ) → ( 𝑉 ⊆ 𝑠 → ∀ 𝑦 ∈ ( 𝑀 LinCo 𝑉 ) 𝑦 ∈ 𝑠 ) ) )
4 3 ad2antrr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ ( 𝑀 LinCo 𝑉 ) ) → ( 𝑠 ∈ ( LSubSp ‘ 𝑀 ) → ( 𝑉 ⊆ 𝑠 → ∀ 𝑦 ∈ ( 𝑀 LinCo 𝑉 ) 𝑦 ∈ 𝑠 ) ) )
5 4 imp ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ ( 𝑀 LinCo 𝑉 ) ) ∧ 𝑠 ∈ ( LSubSp ‘ 𝑀 ) ) → ( 𝑉 ⊆ 𝑠 → ∀ 𝑦 ∈ ( 𝑀 LinCo 𝑉 ) 𝑦 ∈ 𝑠 ) )
6 elequ1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝑠 ↔ 𝑥 ∈ 𝑠 ) )
7 6 rspcv ⊢ ( 𝑥 ∈ ( 𝑀 LinCo 𝑉 ) → ( ∀ 𝑦 ∈ ( 𝑀 LinCo 𝑉 ) 𝑦 ∈ 𝑠 → 𝑥 ∈ 𝑠 ) )
8 7 ad2antlr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ ( 𝑀 LinCo 𝑉 ) ) ∧ 𝑠 ∈ ( LSubSp ‘ 𝑀 ) ) → ( ∀ 𝑦 ∈ ( 𝑀 LinCo 𝑉 ) 𝑦 ∈ 𝑠 → 𝑥 ∈ 𝑠 ) )
9 5 8 syld ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ ( 𝑀 LinCo 𝑉 ) ) ∧ 𝑠 ∈ ( LSubSp ‘ 𝑀 ) ) → ( 𝑉 ⊆ 𝑠 → 𝑥 ∈ 𝑠 ) )
10 9 ralrimiva ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ ( 𝑀 LinCo 𝑉 ) ) → ∀ 𝑠 ∈ ( LSubSp ‘ 𝑀 ) ( 𝑉 ⊆ 𝑠 → 𝑥 ∈ 𝑠 ) )
11 vex ⊢ 𝑥 ∈ V
12 11 elintrab ⊢ ( 𝑥 ∈ ∩ { 𝑠 ∈ ( LSubSp ‘ 𝑀 ) ∣ 𝑉 ⊆ 𝑠 } ↔ ∀ 𝑠 ∈ ( LSubSp ‘ 𝑀 ) ( 𝑉 ⊆ 𝑠 → 𝑥 ∈ 𝑠 ) )
13 10 12 sylibr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ ( 𝑀 LinCo 𝑉 ) ) → 𝑥 ∈ ∩ { 𝑠 ∈ ( LSubSp ‘ 𝑀 ) ∣ 𝑉 ⊆ 𝑠 } )
14 simpll ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ ( 𝑀 LinCo 𝑉 ) ) → 𝑀 ∈ LMod )
15 elpwi ⊢ ( 𝑉 ∈ 𝒫 𝐵 → 𝑉 ⊆ 𝐵 )
16 15 ad2antlr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ ( 𝑀 LinCo 𝑉 ) ) → 𝑉 ⊆ 𝐵 )
17 eqid ⊢ ( LSubSp ‘ 𝑀 ) = ( LSubSp ‘ 𝑀 )
18 eqid ⊢ ( LSpan ‘ 𝑀 ) = ( LSpan ‘ 𝑀 )
19 1 17 18 lspval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) → ( ( LSpan ‘ 𝑀 ) ‘ 𝑉 ) = ∩ { 𝑠 ∈ ( LSubSp ‘ 𝑀 ) ∣ 𝑉 ⊆ 𝑠 } )
20 14 16 19 syl2anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ ( 𝑀 LinCo 𝑉 ) ) → ( ( LSpan ‘ 𝑀 ) ‘ 𝑉 ) = ∩ { 𝑠 ∈ ( LSubSp ‘ 𝑀 ) ∣ 𝑉 ⊆ 𝑠 } )
21 13 20 eleqtrrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ ( 𝑀 LinCo 𝑉 ) ) → 𝑥 ∈ ( ( LSpan ‘ 𝑀 ) ‘ 𝑉 ) )
22 21 ex ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑥 ∈ ( 𝑀 LinCo 𝑉 ) → 𝑥 ∈ ( ( LSpan ‘ 𝑀 ) ‘ 𝑉 ) ) )
23 22 ssrdv ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 LinCo 𝑉 ) ⊆ ( ( LSpan ‘ 𝑀 ) ‘ 𝑉 ) )