Metamath Proof Explorer

Theorem lspsnvs

Description: A nonzero scalar product does not change the span of a singleton. ( spansncol analog.) (Contributed by NM, 23-Apr-2014)

Ref Expression
Hypotheses lspsnvs.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspsnvs.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lspsnvs.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
lspsnvs.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
lspsnvs.o ⊢ 0 = ( 0g ‘ 𝐹 )
lspsnvs.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion lspsnvs ( ( 𝑊 ∈ LVec ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑅 · 𝑋 ) } ) = ( 𝑁 ‘ { 𝑋 } ) )

Proof

Step Hyp Ref Expression
1 lspsnvs.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspsnvs.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 lspsnvs.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 lspsnvs.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 lspsnvs.o ⊢ 0 = ( 0g ‘ 𝐹 )
6 lspsnvs.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
7 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
8 7 3ad2ant1 ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉 ) → 𝑊 ∈ LMod )
9 simp2l ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉 ) → 𝑅 ∈ 𝐾 )
10 simp3 ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
11 2 4 1 3 6 lspsnvsi ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑅 · 𝑋 ) } ) ⊆ ( 𝑁 ‘ { 𝑋 } ) )
12 8 9 10 11 syl3anc ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑅 · 𝑋 ) } ) ⊆ ( 𝑁 ‘ { 𝑋 } ) )
13 2 lvecdrng ⊢ ( 𝑊 ∈ LVec → 𝐹 ∈ DivRing )
14 13 3ad2ant1 ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉 ) → 𝐹 ∈ DivRing )
15 simp2r ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉 ) → 𝑅 ≠ 0 )
16 eqid ⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
17 eqid ⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
18 eqid ⊢ ( invr ‘ 𝐹 ) = ( invr ‘ 𝐹 )
19 4 5 16 17 18 drnginvrl ⊢ ( ( 𝐹 ∈ DivRing ∧ 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝑅 ) ( .r ‘ 𝐹 ) 𝑅 ) = ( 1r ‘ 𝐹 ) )
20 14 9 15 19 syl3anc ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝑅 ) ( .r ‘ 𝐹 ) 𝑅 ) = ( 1r ‘ 𝐹 ) )
21 20 oveq1d ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉 ) → ( ( ( ( invr ‘ 𝐹 ) ‘ 𝑅 ) ( .r ‘ 𝐹 ) 𝑅 ) · 𝑋 ) = ( ( 1r ‘ 𝐹 ) · 𝑋 ) )
22 4 5 18 drnginvrcl ⊢ ( ( 𝐹 ∈ DivRing ∧ 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) → ( ( invr ‘ 𝐹 ) ‘ 𝑅 ) ∈ 𝐾 )
23 14 9 15 22 syl3anc ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉 ) → ( ( invr ‘ 𝐹 ) ‘ 𝑅 ) ∈ 𝐾 )
24 1 2 3 4 16 lmodvsass ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( ( invr ‘ 𝐹 ) ‘ 𝑅 ) ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( ( ( invr ‘ 𝐹 ) ‘ 𝑅 ) ( .r ‘ 𝐹 ) 𝑅 ) · 𝑋 ) = ( ( ( invr ‘ 𝐹 ) ‘ 𝑅 ) · ( 𝑅 · 𝑋 ) ) )
25 8 23 9 10 24 syl13anc ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉 ) → ( ( ( ( invr ‘ 𝐹 ) ‘ 𝑅 ) ( .r ‘ 𝐹 ) 𝑅 ) · 𝑋 ) = ( ( ( invr ‘ 𝐹 ) ‘ 𝑅 ) · ( 𝑅 · 𝑋 ) ) )
26 1 2 3 17 lmodvs1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 1r ‘ 𝐹 ) · 𝑋 ) = 𝑋 )
27 8 10 26 syl2anc ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉 ) → ( ( 1r ‘ 𝐹 ) · 𝑋 ) = 𝑋 )
28 21 25 27 3eqtr3d ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝑅 ) · ( 𝑅 · 𝑋 ) ) = 𝑋 )
29 28 sneqd ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉 ) → { ( ( ( invr ‘ 𝐹 ) ‘ 𝑅 ) · ( 𝑅 · 𝑋 ) ) } = { 𝑋 } )
30 29 fveq2d ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { ( ( ( invr ‘ 𝐹 ) ‘ 𝑅 ) · ( 𝑅 · 𝑋 ) ) } ) = ( 𝑁 ‘ { 𝑋 } ) )
31 1 2 3 4 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑅 · 𝑋 ) ∈ 𝑉 )
32 8 9 10 31 syl3anc ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑅 · 𝑋 ) ∈ 𝑉 )
33 2 4 1 3 6 lspsnvsi ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( invr ‘ 𝐹 ) ‘ 𝑅 ) ∈ 𝐾 ∧ ( 𝑅 · 𝑋 ) ∈ 𝑉 ) → ( 𝑁 ‘ { ( ( ( invr ‘ 𝐹 ) ‘ 𝑅 ) · ( 𝑅 · 𝑋 ) ) } ) ⊆ ( 𝑁 ‘ { ( 𝑅 · 𝑋 ) } ) )
34 8 23 32 33 syl3anc ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { ( ( ( invr ‘ 𝐹 ) ‘ 𝑅 ) · ( 𝑅 · 𝑋 ) ) } ) ⊆ ( 𝑁 ‘ { ( 𝑅 · 𝑋 ) } ) )
35 30 34 eqsstrrd ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { ( 𝑅 · 𝑋 ) } ) )
36 12 35 eqssd ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑅 · 𝑋 ) } ) = ( 𝑁 ‘ { 𝑋 } ) )