This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lspsnss2

Description: Comparable spans of singletons must have proportional vectors. See lspsneq for equal span version. (Contributed by NM, 7-Jun-2015)

Ref Expression
Hypotheses lspsnss2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspsnss2.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
lspsnss2.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
lspsnss2.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
lspsnss2.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lspsnss2.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lspsnss2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lspsnss2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion lspsnss2 ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ↔ ∃ 𝑘 ∈ 𝐾 𝑋 = ( 𝑘 · 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 lspsnss2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspsnss2.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
3 lspsnss2.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
4 lspsnss2.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
5 lspsnss2.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
6 lspsnss2.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
7 lspsnss2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
8 lspsnss2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
9 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
10 1 9 5 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
11 6 8 10 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
12 1 9 5 6 11 7 ellspsn5b ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ) )
13 2 3 1 4 5 ellspsn ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ↔ ∃ 𝑘 ∈ 𝐾 𝑋 = ( 𝑘 · 𝑌 ) ) )
14 6 8 13 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ↔ ∃ 𝑘 ∈ 𝐾 𝑋 = ( 𝑘 · 𝑌 ) ) )
15 12 14 bitr3d ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ↔ ∃ 𝑘 ∈ 𝐾 𝑋 = ( 𝑘 · 𝑌 ) ) )