Metamath Proof Explorer

Theorem lindfrn

Description: The range of an independent family is an independent set. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Assertion lindfrn 
|- ( ( W e. LMod /\ F LIndF W ) -> ran F e. ( LIndS ` W ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` W ) = ( Base ` W )
2 1 lindff 
 |-  ( ( F LIndF W /\ W e. LMod ) -> F : dom F --> ( Base ` W ) )
3 2 ancoms 
 |-  ( ( W e. LMod /\ F LIndF W ) -> F : dom F --> ( Base ` W ) )
4 3 frnd 
 |-  ( ( W e. LMod /\ F LIndF W ) -> ran F C_ ( Base ` W ) )
5 simpll 
 |-  ( ( ( W e. LMod /\ F LIndF W ) /\ y e. dom F ) -> W e. LMod )
6 imassrn 
 |-  ( F " ( dom F \ { y } ) ) C_ ran F
7 6 4 sstrid 
 |-  ( ( W e. LMod /\ F LIndF W ) -> ( F " ( dom F \ { y } ) ) C_ ( Base ` W ) )
8 7 adantr 
 |-  ( ( ( W e. LMod /\ F LIndF W ) /\ y e. dom F ) -> ( F " ( dom F \ { y } ) ) C_ ( Base ` W ) )
9 3 ffund 
 |-  ( ( W e. LMod /\ F LIndF W ) -> Fun F )
10 eldifsn 
 |-  ( x e. ( ran F \ { ( F ` y ) } ) <-> ( x e. ran F /\ x =/= ( F ` y ) ) )
11 funfn 
 |-  ( Fun F <-> F Fn dom F )
12 fvelrnb 
 |-  ( F Fn dom F -> ( x e. ran F <-> E. k e. dom F ( F ` k ) = x ) )
13 11 12 sylbi 
 |-  ( Fun F -> ( x e. ran F <-> E. k e. dom F ( F ` k ) = x ) )
14 13 adantr 
 |-  ( ( Fun F /\ y e. dom F ) -> ( x e. ran F <-> E. k e. dom F ( F ` k ) = x ) )
15 difss 
 |-  ( dom F \ { y } ) C_ dom F
16 15 jctr 
 |-  ( Fun F -> ( Fun F /\ ( dom F \ { y } ) C_ dom F ) )
17 16 ad2antrr 
 |-  ( ( ( Fun F /\ y e. dom F ) /\ ( k e. dom F /\ ( F ` k ) =/= ( F ` y ) ) ) -> ( Fun F /\ ( dom F \ { y } ) C_ dom F ) )
18 simpl 
 |-  ( ( k e. dom F /\ ( F ` k ) =/= ( F ` y ) ) -> k e. dom F )
19 fveq2 
 |-  ( k = y -> ( F ` k ) = ( F ` y ) )
20 19 necon3i 
 |-  ( ( F ` k ) =/= ( F ` y ) -> k =/= y )
21 20 adantl 
 |-  ( ( k e. dom F /\ ( F ` k ) =/= ( F ` y ) ) -> k =/= y )
22 eldifsn 
 |-  ( k e. ( dom F \ { y } ) <-> ( k e. dom F /\ k =/= y ) )
23 18 21 22 sylanbrc 
 |-  ( ( k e. dom F /\ ( F ` k ) =/= ( F ` y ) ) -> k e. ( dom F \ { y } ) )
24 23 adantl 
 |-  ( ( ( Fun F /\ y e. dom F ) /\ ( k e. dom F /\ ( F ` k ) =/= ( F ` y ) ) ) -> k e. ( dom F \ { y } ) )
25 funfvima2 
 |-  ( ( Fun F /\ ( dom F \ { y } ) C_ dom F ) -> ( k e. ( dom F \ { y } ) -> ( F ` k ) e. ( F " ( dom F \ { y } ) ) ) )
26 17 24 25 sylc 
 |-  ( ( ( Fun F /\ y e. dom F ) /\ ( k e. dom F /\ ( F ` k ) =/= ( F ` y ) ) ) -> ( F ` k ) e. ( F " ( dom F \ { y } ) ) )
27 26 expr 
 |-  ( ( ( Fun F /\ y e. dom F ) /\ k e. dom F ) -> ( ( F ` k ) =/= ( F ` y ) -> ( F ` k ) e. ( F " ( dom F \ { y } ) ) ) )
28 neeq1 
 |-  ( ( F ` k ) = x -> ( ( F ` k ) =/= ( F ` y ) <-> x =/= ( F ` y ) ) )
29 eleq1 
 |-  ( ( F ` k ) = x -> ( ( F ` k ) e. ( F " ( dom F \ { y } ) ) <-> x e. ( F " ( dom F \ { y } ) ) ) )
30 28 29 imbi12d 
 |-  ( ( F ` k ) = x -> ( ( ( F ` k ) =/= ( F ` y ) -> ( F ` k ) e. ( F " ( dom F \ { y } ) ) ) <-> ( x =/= ( F ` y ) -> x e. ( F " ( dom F \ { y } ) ) ) ) )
31 27 30 syl5ibcom 
 |-  ( ( ( Fun F /\ y e. dom F ) /\ k e. dom F ) -> ( ( F ` k ) = x -> ( x =/= ( F ` y ) -> x e. ( F " ( dom F \ { y } ) ) ) ) )
32 31 rexlimdva 
 |-  ( ( Fun F /\ y e. dom F ) -> ( E. k e. dom F ( F ` k ) = x -> ( x =/= ( F ` y ) -> x e. ( F " ( dom F \ { y } ) ) ) ) )
33 14 32 sylbid 
 |-  ( ( Fun F /\ y e. dom F ) -> ( x e. ran F -> ( x =/= ( F ` y ) -> x e. ( F " ( dom F \ { y } ) ) ) ) )
34 33 impd 
 |-  ( ( Fun F /\ y e. dom F ) -> ( ( x e. ran F /\ x =/= ( F ` y ) ) -> x e. ( F " ( dom F \ { y } ) ) ) )
35 10 34 biimtrid 
 |-  ( ( Fun F /\ y e. dom F ) -> ( x e. ( ran F \ { ( F ` y ) } ) -> x e. ( F " ( dom F \ { y } ) ) ) )
36 35 ssrdv 
 |-  ( ( Fun F /\ y e. dom F ) -> ( ran F \ { ( F ` y ) } ) C_ ( F " ( dom F \ { y } ) ) )
37 9 36 sylan 
 |-  ( ( ( W e. LMod /\ F LIndF W ) /\ y e. dom F ) -> ( ran F \ { ( F ` y ) } ) C_ ( F " ( dom F \ { y } ) ) )
38 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
39 1 38 lspss 
 |-  ( ( W e. LMod /\ ( F " ( dom F \ { y } ) ) C_ ( Base ` W ) /\ ( ran F \ { ( F ` y ) } ) C_ ( F " ( dom F \ { y } ) ) ) -> ( ( LSpan ` W ) ` ( ran F \ { ( F ` y ) } ) ) C_ ( ( LSpan ` W ) ` ( F " ( dom F \ { y } ) ) ) )
40 5 8 37 39 syl3anc 
 |-  ( ( ( W e. LMod /\ F LIndF W ) /\ y e. dom F ) -> ( ( LSpan ` W ) ` ( ran F \ { ( F ` y ) } ) ) C_ ( ( LSpan ` W ) ` ( F " ( dom F \ { y } ) ) ) )
41 40 adantrr 
 |-  ( ( ( W e. LMod /\ F LIndF W ) /\ ( y e. dom F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( ( LSpan ` W ) ` ( ran F \ { ( F ` y ) } ) ) C_ ( ( LSpan ` W ) ` ( F " ( dom F \ { y } ) ) ) )
42 simplr 
 |-  ( ( ( W e. LMod /\ F LIndF W ) /\ ( y e. dom F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> F LIndF W )
43 simprl 
 |-  ( ( ( W e. LMod /\ F LIndF W ) /\ ( y e. dom F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> y e. dom F )
44 eldifi 
 |-  ( k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -> k e. ( Base ` ( Scalar ` W ) ) )
45 44 ad2antll 
 |-  ( ( ( W e. LMod /\ F LIndF W ) /\ ( y e. dom F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> k e. ( Base ` ( Scalar ` W ) ) )
46 eldifsni 
 |-  ( k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -> k =/= ( 0g ` ( Scalar ` W ) ) )
47 46 ad2antll 
 |-  ( ( ( W e. LMod /\ F LIndF W ) /\ ( y e. dom F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> k =/= ( 0g ` ( Scalar ` W ) ) )
48 eqid 
 |-  ( .s ` W ) = ( .s ` W )
49 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
50 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
51 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
52 48 38 49 50 51 lindfind 
 |-  ( ( ( F LIndF W /\ y e. dom F ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ k =/= ( 0g ` ( Scalar ` W ) ) ) ) -> -. ( k ( .s ` W ) ( F ` y ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { y } ) ) ) )
53 42 43 45 47 52 syl22anc 
 |-  ( ( ( W e. LMod /\ F LIndF W ) /\ ( y e. dom F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> -. ( k ( .s ` W ) ( F ` y ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { y } ) ) ) )
54 41 53 ssneldd 
 |-  ( ( ( W e. LMod /\ F LIndF W ) /\ ( y e. dom F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> -. ( k ( .s ` W ) ( F ` y ) ) e. ( ( LSpan ` W ) ` ( ran F \ { ( F ` y ) } ) ) )
55 54 ralrimivva 
 |-  ( ( W e. LMod /\ F LIndF W ) -> A. y e. dom F A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) ( F ` y ) ) e. ( ( LSpan ` W ) ` ( ran F \ { ( F ` y ) } ) ) )
56 9 funfnd 
 |-  ( ( W e. LMod /\ F LIndF W ) -> F Fn dom F )
57 oveq2 
 |-  ( x = ( F ` y ) -> ( k ( .s ` W ) x ) = ( k ( .s ` W ) ( F ` y ) ) )
58 sneq 
 |-  ( x = ( F ` y ) -> { x } = { ( F ` y ) } )
59 58 difeq2d 
 |-  ( x = ( F ` y ) -> ( ran F \ { x } ) = ( ran F \ { ( F ` y ) } ) )
60 59 fveq2d 
 |-  ( x = ( F ` y ) -> ( ( LSpan ` W ) ` ( ran F \ { x } ) ) = ( ( LSpan ` W ) ` ( ran F \ { ( F ` y ) } ) ) )
61 57 60 eleq12d 
 |-  ( x = ( F ` y ) -> ( ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ran F \ { x } ) ) <-> ( k ( .s ` W ) ( F ` y ) ) e. ( ( LSpan ` W ) ` ( ran F \ { ( F ` y ) } ) ) ) )
62 61 notbid 
 |-  ( x = ( F ` y ) -> ( -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ran F \ { x } ) ) <-> -. ( k ( .s ` W ) ( F ` y ) ) e. ( ( LSpan ` W ) ` ( ran F \ { ( F ` y ) } ) ) ) )
63 62 ralbidv 
 |-  ( x = ( F ` y ) -> ( A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ran F \ { x } ) ) <-> A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) ( F ` y ) ) e. ( ( LSpan ` W ) ` ( ran F \ { ( F ` y ) } ) ) ) )
64 63 ralrn 
 |-  ( F Fn dom F -> ( A. x e. ran F A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ran F \ { x } ) ) <-> A. y e. dom F A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) ( F ` y ) ) e. ( ( LSpan ` W ) ` ( ran F \ { ( F ` y ) } ) ) ) )
65 56 64 syl 
 |-  ( ( W e. LMod /\ F LIndF W ) -> ( A. x e. ran F A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ran F \ { x } ) ) <-> A. y e. dom F A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) ( F ` y ) ) e. ( ( LSpan ` W ) ` ( ran F \ { ( F ` y ) } ) ) ) )
66 55 65 mpbird 
 |-  ( ( W e. LMod /\ F LIndF W ) -> A. x e. ran F A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ran F \ { x } ) ) )
67 1 48 38 49 51 50 islinds2 
 |-  ( W e. LMod -> ( ran F e. ( LIndS ` W ) <-> ( ran F C_ ( Base ` W ) /\ A. x e. ran F A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ran F \ { x } ) ) ) ) )
68 67 adantr 
 |-  ( ( W e. LMod /\ F LIndF W ) -> ( ran F e. ( LIndS ` W ) <-> ( ran F C_ ( Base ` W ) /\ A. x e. ran F A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ran F \ { x } ) ) ) ) )
69 4 66 68 mpbir2and 
 |-  ( ( W e. LMod /\ F LIndF W ) -> ran F e. ( LIndS ` W ) )