Metamath Proof Explorer

Theorem snlindsntorlem

Description: Lemma for snlindsntor . (Contributed by AV, 15-Apr-2019)

Ref Expression
Hypotheses snlindsntor.b 
|- B = ( Base ` M )
snlindsntor.r 
|- R = ( Scalar ` M )
snlindsntor.s 
|- S = ( Base ` R )
snlindsntor.0 
|- .0. = ( 0g ` R )
snlindsntor.z 
|- Z = ( 0g ` M )
snlindsntor.t 
|- .x. = ( .s ` M )
Assertion snlindsntorlem 
|- ( ( M e. LMod /\ X e. B ) -> ( A. f e. ( S ^m { X } ) ( ( f ( linC ` M ) { X } ) = Z -> ( f ` X ) = .0. ) -> A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) )

Proof

Step Hyp Ref Expression
1 snlindsntor.b 
 |-  B = ( Base ` M )
2 snlindsntor.r 
 |-  R = ( Scalar ` M )
3 snlindsntor.s 
 |-  S = ( Base ` R )
4 snlindsntor.0 
 |-  .0. = ( 0g ` R )
5 snlindsntor.z 
 |-  Z = ( 0g ` M )
6 snlindsntor.t 
 |-  .x. = ( .s ` M )
7 eqidd 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ s e. S ) -> { <. X , s >. } = { <. X , s >. } )
8 fsng 
 |-  ( ( X e. B /\ s e. S ) -> ( { <. X , s >. } : { X } --> { s } <-> { <. X , s >. } = { <. X , s >. } ) )
9 8 adantll 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ s e. S ) -> ( { <. X , s >. } : { X } --> { s } <-> { <. X , s >. } = { <. X , s >. } ) )
10 7 9 mpbird 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ s e. S ) -> { <. X , s >. } : { X } --> { s } )
11 snssi 
 |-  ( s e. S -> { s } C_ S )
12 11 adantl 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ s e. S ) -> { s } C_ S )
13 10 12 fssd 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ s e. S ) -> { <. X , s >. } : { X } --> S )
14 3 fvexi 
 |-  S e. _V
15 snex 
 |-  { X } e. _V
16 14 15 pm3.2i 
 |-  ( S e. _V /\ { X } e. _V )
17 elmapg 
 |-  ( ( S e. _V /\ { X } e. _V ) -> ( { <. X , s >. } e. ( S ^m { X } ) <-> { <. X , s >. } : { X } --> S ) )
18 16 17 mp1i 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ s e. S ) -> ( { <. X , s >. } e. ( S ^m { X } ) <-> { <. X , s >. } : { X } --> S ) )
19 13 18 mpbird 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ s e. S ) -> { <. X , s >. } e. ( S ^m { X } ) )
20 oveq1 
 |-  ( f = { <. X , s >. } -> ( f ( linC ` M ) { X } ) = ( { <. X , s >. } ( linC ` M ) { X } ) )
21 20 eqeq1d 
 |-  ( f = { <. X , s >. } -> ( ( f ( linC ` M ) { X } ) = Z <-> ( { <. X , s >. } ( linC ` M ) { X } ) = Z ) )
22 fveq1 
 |-  ( f = { <. X , s >. } -> ( f ` X ) = ( { <. X , s >. } ` X ) )
23 22 eqeq1d 
 |-  ( f = { <. X , s >. } -> ( ( f ` X ) = .0. <-> ( { <. X , s >. } ` X ) = .0. ) )
24 21 23 imbi12d 
 |-  ( f = { <. X , s >. } -> ( ( ( f ( linC ` M ) { X } ) = Z -> ( f ` X ) = .0. ) <-> ( ( { <. X , s >. } ( linC ` M ) { X } ) = Z -> ( { <. X , s >. } ` X ) = .0. ) ) )
25 1 2 3 6 lincvalsng 
 |-  ( ( M e. LMod /\ X e. B /\ s e. S ) -> ( { <. X , s >. } ( linC ` M ) { X } ) = ( s .x. X ) )
26 25 3expa 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ s e. S ) -> ( { <. X , s >. } ( linC ` M ) { X } ) = ( s .x. X ) )
27 26 eqeq1d 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ s e. S ) -> ( ( { <. X , s >. } ( linC ` M ) { X } ) = Z <-> ( s .x. X ) = Z ) )
28 fvsng 
 |-  ( ( X e. B /\ s e. S ) -> ( { <. X , s >. } ` X ) = s )
29 28 adantll 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ s e. S ) -> ( { <. X , s >. } ` X ) = s )
30 29 eqeq1d 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ s e. S ) -> ( ( { <. X , s >. } ` X ) = .0. <-> s = .0. ) )
31 27 30 imbi12d 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ s e. S ) -> ( ( ( { <. X , s >. } ( linC ` M ) { X } ) = Z -> ( { <. X , s >. } ` X ) = .0. ) <-> ( ( s .x. X ) = Z -> s = .0. ) ) )
32 24 31 sylan9bbr 
 |-  ( ( ( ( M e. LMod /\ X e. B ) /\ s e. S ) /\ f = { <. X , s >. } ) -> ( ( ( f ( linC ` M ) { X } ) = Z -> ( f ` X ) = .0. ) <-> ( ( s .x. X ) = Z -> s = .0. ) ) )
33 19 32 rspcdv 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ s e. S ) -> ( A. f e. ( S ^m { X } ) ( ( f ( linC ` M ) { X } ) = Z -> ( f ` X ) = .0. ) -> ( ( s .x. X ) = Z -> s = .0. ) ) )
34 33 ralrimdva 
 |-  ( ( M e. LMod /\ X e. B ) -> ( A. f e. ( S ^m { X } ) ( ( f ( linC ` M ) { X } ) = Z -> ( f ` X ) = .0. ) -> A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) )