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 
|- V = ( Base ` W )
lspsnvs.f 
|- F = ( Scalar ` W )
lspsnvs.t 
|- .x. = ( .s ` W )
lspsnvs.k 
|- K = ( Base ` F )
lspsnvs.o 
|- .0. = ( 0g ` F )
lspsnvs.n 
|- N = ( LSpan ` W )
Assertion lspsnvs 
|- ( ( W e. LVec /\ ( R e. K /\ R =/= .0. ) /\ X e. V ) -> ( N ` { ( R .x. X ) } ) = ( N ` { X } ) )

Proof

Step Hyp Ref Expression
1 lspsnvs.v 
 |-  V = ( Base ` W )
2 lspsnvs.f 
 |-  F = ( Scalar ` W )
3 lspsnvs.t 
 |-  .x. = ( .s ` W )
4 lspsnvs.k 
 |-  K = ( Base ` F )
5 lspsnvs.o 
 |-  .0. = ( 0g ` F )
6 lspsnvs.n 
 |-  N = ( LSpan ` W )
7 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
8 7 3ad2ant1 
 |-  ( ( W e. LVec /\ ( R e. K /\ R =/= .0. ) /\ X e. V ) -> W e. LMod )
9 simp2l 
 |-  ( ( W e. LVec /\ ( R e. K /\ R =/= .0. ) /\ X e. V ) -> R e. K )
10 simp3 
 |-  ( ( W e. LVec /\ ( R e. K /\ R =/= .0. ) /\ X e. V ) -> X e. V )
11 2 4 1 3 6 lspsnvsi 
 |-  ( ( W e. LMod /\ R e. K /\ X e. V ) -> ( N ` { ( R .x. X ) } ) C_ ( N ` { X } ) )
12 8 9 10 11 syl3anc 
 |-  ( ( W e. LVec /\ ( R e. K /\ R =/= .0. ) /\ X e. V ) -> ( N ` { ( R .x. X ) } ) C_ ( N ` { X } ) )
13 2 lvecdrng 
 |-  ( W e. LVec -> F e. DivRing )
14 13 3ad2ant1 
 |-  ( ( W e. LVec /\ ( R e. K /\ R =/= .0. ) /\ X e. V ) -> F e. DivRing )
15 simp2r 
 |-  ( ( W e. LVec /\ ( R e. K /\ R =/= .0. ) /\ X e. V ) -> R =/= .0. )
16 eqid 
 |-  ( .r ` F ) = ( .r ` F )
17 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
18 eqid 
 |-  ( invr ` F ) = ( invr ` F )
19 4 5 16 17 18 drnginvrl 
 |-  ( ( F e. DivRing /\ R e. K /\ R =/= .0. ) -> ( ( ( invr ` F ) ` R ) ( .r ` F ) R ) = ( 1r ` F ) )
20 14 9 15 19 syl3anc 
 |-  ( ( W e. LVec /\ ( R e. K /\ R =/= .0. ) /\ X e. V ) -> ( ( ( invr ` F ) ` R ) ( .r ` F ) R ) = ( 1r ` F ) )
21 20 oveq1d 
 |-  ( ( W e. LVec /\ ( R e. K /\ R =/= .0. ) /\ X e. V ) -> ( ( ( ( invr ` F ) ` R ) ( .r ` F ) R ) .x. X ) = ( ( 1r ` F ) .x. X ) )
22 4 5 18 drnginvrcl 
 |-  ( ( F e. DivRing /\ R e. K /\ R =/= .0. ) -> ( ( invr ` F ) ` R ) e. K )
23 14 9 15 22 syl3anc 
 |-  ( ( W e. LVec /\ ( R e. K /\ R =/= .0. ) /\ X e. V ) -> ( ( invr ` F ) ` R ) e. K )
24 1 2 3 4 16 lmodvsass 
 |-  ( ( W e. LMod /\ ( ( ( invr ` F ) ` R ) e. K /\ R e. K /\ X e. V ) ) -> ( ( ( ( invr ` F ) ` R ) ( .r ` F ) R ) .x. X ) = ( ( ( invr ` F ) ` R ) .x. ( R .x. X ) ) )
25 8 23 9 10 24 syl13anc 
 |-  ( ( W e. LVec /\ ( R e. K /\ R =/= .0. ) /\ X e. V ) -> ( ( ( ( invr ` F ) ` R ) ( .r ` F ) R ) .x. X ) = ( ( ( invr ` F ) ` R ) .x. ( R .x. X ) ) )
26 1 2 3 17 lmodvs1 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( 1r ` F ) .x. X ) = X )
27 8 10 26 syl2anc 
 |-  ( ( W e. LVec /\ ( R e. K /\ R =/= .0. ) /\ X e. V ) -> ( ( 1r ` F ) .x. X ) = X )
28 21 25 27 3eqtr3d 
 |-  ( ( W e. LVec /\ ( R e. K /\ R =/= .0. ) /\ X e. V ) -> ( ( ( invr ` F ) ` R ) .x. ( R .x. X ) ) = X )
29 28 sneqd 
 |-  ( ( W e. LVec /\ ( R e. K /\ R =/= .0. ) /\ X e. V ) -> { ( ( ( invr ` F ) ` R ) .x. ( R .x. X ) ) } = { X } )
30 29 fveq2d 
 |-  ( ( W e. LVec /\ ( R e. K /\ R =/= .0. ) /\ X e. V ) -> ( N ` { ( ( ( invr ` F ) ` R ) .x. ( R .x. X ) ) } ) = ( N ` { X } ) )
31 1 2 3 4 lmodvscl 
 |-  ( ( W e. LMod /\ R e. K /\ X e. V ) -> ( R .x. X ) e. V )
32 8 9 10 31 syl3anc 
 |-  ( ( W e. LVec /\ ( R e. K /\ R =/= .0. ) /\ X e. V ) -> ( R .x. X ) e. V )
33 2 4 1 3 6 lspsnvsi 
 |-  ( ( W e. LMod /\ ( ( invr ` F ) ` R ) e. K /\ ( R .x. X ) e. V ) -> ( N ` { ( ( ( invr ` F ) ` R ) .x. ( R .x. X ) ) } ) C_ ( N ` { ( R .x. X ) } ) )
34 8 23 32 33 syl3anc 
 |-  ( ( W e. LVec /\ ( R e. K /\ R =/= .0. ) /\ X e. V ) -> ( N ` { ( ( ( invr ` F ) ` R ) .x. ( R .x. X ) ) } ) C_ ( N ` { ( R .x. X ) } ) )
35 30 34 eqsstrrd 
 |-  ( ( W e. LVec /\ ( R e. K /\ R =/= .0. ) /\ X e. V ) -> ( N ` { X } ) C_ ( N ` { ( R .x. X ) } ) )
36 12 35 eqssd 
 |-  ( ( W e. LVec /\ ( R e. K /\ R =/= .0. ) /\ X e. V ) -> ( N ` { ( R .x. X ) } ) = ( N ` { X } ) )