Metamath Proof Explorer

Theorem lspsneleq

Description: Membership relation that implies equality of spans. ( spansneleq analog.) (Contributed by NM, 4-Jul-2014)

Ref Expression
Hypotheses lspsneleq.v 
|- V = ( Base ` W )
lspsneleq.o 
|- .0. = ( 0g ` W )
lspsneleq.n 
|- N = ( LSpan ` W )
lspsneleq.w 
|- ( ph -> W e. LVec )
lspsneleq.x 
|- ( ph -> X e. V )
lspsneleq.y 
|- ( ph -> Y e. ( N ` { X } ) )
lspsneleq.z 
|- ( ph -> Y =/= .0. )
Assertion lspsneleq 
|- ( ph -> ( N ` { Y } ) = ( N ` { X } ) )

Proof

Step Hyp Ref Expression
1 lspsneleq.v 
 |-  V = ( Base ` W )
2 lspsneleq.o 
 |-  .0. = ( 0g ` W )
3 lspsneleq.n 
 |-  N = ( LSpan ` W )
4 lspsneleq.w 
 |-  ( ph -> W e. LVec )
5 lspsneleq.x 
 |-  ( ph -> X e. V )
6 lspsneleq.y 
 |-  ( ph -> Y e. ( N ` { X } ) )
7 lspsneleq.z 
 |-  ( ph -> Y =/= .0. )
8 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
9 4 8 syl 
 |-  ( ph -> W e. LMod )
10 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
11 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
12 eqid 
 |-  ( .s ` W ) = ( .s ` W )
13 10 11 1 12 3 ellspsn 
 |-  ( ( W e. LMod /\ X e. V ) -> ( Y e. ( N ` { X } ) <-> E. k e. ( Base ` ( Scalar ` W ) ) Y = ( k ( .s ` W ) X ) ) )
14 9 5 13 syl2anc 
 |-  ( ph -> ( Y e. ( N ` { X } ) <-> E. k e. ( Base ` ( Scalar ` W ) ) Y = ( k ( .s ` W ) X ) ) )
15 simpr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ Y = ( k ( .s ` W ) X ) ) -> Y = ( k ( .s ` W ) X ) )
16 15 sneqd 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ Y = ( k ( .s ` W ) X ) ) -> { Y } = { ( k ( .s ` W ) X ) } )
17 16 fveq2d 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ Y = ( k ( .s ` W ) X ) ) -> ( N ` { Y } ) = ( N ` { ( k ( .s ` W ) X ) } ) )
18 4 ad2antrr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ Y = ( k ( .s ` W ) X ) ) -> W e. LVec )
19 simplr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ Y = ( k ( .s ` W ) X ) ) -> k e. ( Base ` ( Scalar ` W ) ) )
20 7 ad2antrr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ Y = ( k ( .s ` W ) X ) ) -> Y =/= .0. )
21 simplr 
 |-  ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ Y = ( k ( .s ` W ) X ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> Y = ( k ( .s ` W ) X ) )
22 simpr 
 |-  ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ Y = ( k ( .s ` W ) X ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> k = ( 0g ` ( Scalar ` W ) ) )
23 22 oveq1d 
 |-  ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ Y = ( k ( .s ` W ) X ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> ( k ( .s ` W ) X ) = ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) X ) )
24 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
25 1 10 12 24 2 lmod0vs 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) X ) = .0. )
26 9 5 25 syl2anc 
 |-  ( ph -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) X ) = .0. )
27 26 ad3antrrr 
 |-  ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ Y = ( k ( .s ` W ) X ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) X ) = .0. )
28 21 23 27 3eqtrd 
 |-  ( ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ Y = ( k ( .s ` W ) X ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> Y = .0. )
29 28 ex 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ Y = ( k ( .s ` W ) X ) ) -> ( k = ( 0g ` ( Scalar ` W ) ) -> Y = .0. ) )
30 29 necon3d 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ Y = ( k ( .s ` W ) X ) ) -> ( Y =/= .0. -> k =/= ( 0g ` ( Scalar ` W ) ) ) )
31 20 30 mpd 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ Y = ( k ( .s ` W ) X ) ) -> k =/= ( 0g ` ( Scalar ` W ) ) )
32 5 ad2antrr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ Y = ( k ( .s ` W ) X ) ) -> X e. V )
33 1 10 12 11 24 3 lspsnvs 
 |-  ( ( W e. LVec /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ k =/= ( 0g ` ( Scalar ` W ) ) ) /\ X e. V ) -> ( N ` { ( k ( .s ` W ) X ) } ) = ( N ` { X } ) )
34 18 19 31 32 33 syl121anc 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ Y = ( k ( .s ` W ) X ) ) -> ( N ` { ( k ( .s ` W ) X ) } ) = ( N ` { X } ) )
35 17 34 eqtrd 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ Y = ( k ( .s ` W ) X ) ) -> ( N ` { Y } ) = ( N ` { X } ) )
36 35 rexlimdva2 
 |-  ( ph -> ( E. k e. ( Base ` ( Scalar ` W ) ) Y = ( k ( .s ` W ) X ) -> ( N ` { Y } ) = ( N ` { X } ) ) )
37 14 36 sylbid 
 |-  ( ph -> ( Y e. ( N ` { X } ) -> ( N ` { Y } ) = ( N ` { X } ) ) )
38 6 37 mpd 
 |-  ( ph -> ( N ` { Y } ) = ( N ` { X } ) )