Metamath Proof Explorer

Theorem 0nellinds

Description: The group identity cannot be an element of an independent set. (Contributed by Thierry Arnoux, 8-May-2023)

Ref Expression
Hypothesis 0nellinds.1 
|- .0. = ( 0g ` W )
Assertion 0nellinds 
|- ( ( W e. LVec /\ F e. ( LIndS ` W ) ) -> -. .0. e. F )

Proof

Step Hyp Ref Expression
1 0nellinds.1 
 |-  .0. = ( 0g ` W )
2 oveq2 
 |-  ( x = .0. -> ( k ( .s ` W ) x ) = ( k ( .s ` W ) .0. ) )
3 sneq 
 |-  ( x = .0. -> { x } = { .0. } )
4 3 difeq2d 
 |-  ( x = .0. -> ( F \ { x } ) = ( F \ { .0. } ) )
5 4 fveq2d 
 |-  ( x = .0. -> ( ( LSpan ` W ) ` ( F \ { x } ) ) = ( ( LSpan ` W ) ` ( F \ { .0. } ) ) )
6 2 5 eleq12d 
 |-  ( x = .0. -> ( ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( F \ { x } ) ) <-> ( k ( .s ` W ) .0. ) e. ( ( LSpan ` W ) ` ( F \ { .0. } ) ) ) )
7 6 notbid 
 |-  ( x = .0. -> ( -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( F \ { x } ) ) <-> -. ( k ( .s ` W ) .0. ) e. ( ( LSpan ` W ) ` ( F \ { .0. } ) ) ) )
8 7 ralbidv 
 |-  ( x = .0. -> ( A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( F \ { x } ) ) <-> A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) .0. ) e. ( ( LSpan ` W ) ` ( F \ { .0. } ) ) ) )
9 eqid 
 |-  ( Base ` W ) = ( Base ` W )
10 eqid 
 |-  ( .s ` W ) = ( .s ` W )
11 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
12 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
13 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
14 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
15 9 10 11 12 13 14 islinds2 
 |-  ( W e. LVec -> ( F e. ( LIndS ` W ) <-> ( F C_ ( Base ` W ) /\ A. x e. F A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( F \ { x } ) ) ) ) )
16 15 simplbda 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) ) -> A. x e. F A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( F \ { x } ) ) )
17 16 adantr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ .0. e. F ) -> A. x e. F A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( F \ { x } ) ) )
18 simpr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ .0. e. F ) -> .0. e. F )
19 8 17 18 rspcdva 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ .0. e. F ) -> A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) .0. ) e. ( ( LSpan ` W ) ` ( F \ { .0. } ) ) )
20 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
21 eqid 
 |-  ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) )
22 12 13 21 lmod1cl 
 |-  ( W e. LMod -> ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) )
23 20 22 syl 
 |-  ( W e. LVec -> ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) )
24 23 adantr 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) ) -> ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) )
25 12 lvecdrng 
 |-  ( W e. LVec -> ( Scalar ` W ) e. DivRing )
26 14 21 drngunz 
 |-  ( ( Scalar ` W ) e. DivRing -> ( 1r ` ( Scalar ` W ) ) =/= ( 0g ` ( Scalar ` W ) ) )
27 25 26 syl 
 |-  ( W e. LVec -> ( 1r ` ( Scalar ` W ) ) =/= ( 0g ` ( Scalar ` W ) ) )
28 27 adantr 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) ) -> ( 1r ` ( Scalar ` W ) ) =/= ( 0g ` ( Scalar ` W ) ) )
29 eldifsn 
 |-  ( ( 1r ` ( Scalar ` W ) ) e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) <-> ( ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) /\ ( 1r ` ( Scalar ` W ) ) =/= ( 0g ` ( Scalar ` W ) ) ) )
30 24 28 29 sylanbrc 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) ) -> ( 1r ` ( Scalar ` W ) ) e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) )
31 30 adantr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ .0. e. F ) -> ( 1r ` ( Scalar ` W ) ) e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) )
32 20 ad2antrr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ .0. e. F ) -> W e. LMod )
33 12 10 13 1 lmodvs0 
 |-  ( ( W e. LMod /\ ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) ) -> ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) .0. ) = .0. )
34 32 22 33 syl2anc2 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ .0. e. F ) -> ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) .0. ) = .0. )
35 9 linds1 
 |-  ( F e. ( LIndS ` W ) -> F C_ ( Base ` W ) )
36 35 ad2antlr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ .0. e. F ) -> F C_ ( Base ` W ) )
37 36 ssdifssd 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ .0. e. F ) -> ( F \ { .0. } ) C_ ( Base ` W ) )
38 1 9 11 0ellsp 
 |-  ( ( W e. LMod /\ ( F \ { .0. } ) C_ ( Base ` W ) ) -> .0. e. ( ( LSpan ` W ) ` ( F \ { .0. } ) ) )
39 32 37 38 syl2anc 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ .0. e. F ) -> .0. e. ( ( LSpan ` W ) ` ( F \ { .0. } ) ) )
40 34 39 eqeltrd 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ .0. e. F ) -> ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) .0. ) e. ( ( LSpan ` W ) ` ( F \ { .0. } ) ) )
41 oveq1 
 |-  ( k = ( 1r ` ( Scalar ` W ) ) -> ( k ( .s ` W ) .0. ) = ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) .0. ) )
42 41 eleq1d 
 |-  ( k = ( 1r ` ( Scalar ` W ) ) -> ( ( k ( .s ` W ) .0. ) e. ( ( LSpan ` W ) ` ( F \ { .0. } ) ) <-> ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) .0. ) e. ( ( LSpan ` W ) ` ( F \ { .0. } ) ) ) )
43 42 rspcev 
 |-  ( ( ( 1r ` ( Scalar ` W ) ) e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) .0. ) e. ( ( LSpan ` W ) ` ( F \ { .0. } ) ) ) -> E. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ( k ( .s ` W ) .0. ) e. ( ( LSpan ` W ) ` ( F \ { .0. } ) ) )
44 31 40 43 syl2anc 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ .0. e. F ) -> E. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ( k ( .s ` W ) .0. ) e. ( ( LSpan ` W ) ` ( F \ { .0. } ) ) )
45 dfrex2 
 |-  ( E. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ( k ( .s ` W ) .0. ) e. ( ( LSpan ` W ) ` ( F \ { .0. } ) ) <-> -. A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) .0. ) e. ( ( LSpan ` W ) ` ( F \ { .0. } ) ) )
46 44 45 sylib 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ .0. e. F ) -> -. A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) .0. ) e. ( ( LSpan ` W ) ` ( F \ { .0. } ) ) )
47 19 46 pm2.65da 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) ) -> -. .0. e. F )