Metamath Proof Explorer

Theorem f1lindf

Description: Rearranging and deleting elements from an independent family gives an independent family. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Assertion f1lindf 
|- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F o. G ) LIndF 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 3adant3 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> F : dom F --> ( Base ` W ) )
5 f1f 
 |-  ( G : K -1-1-> dom F -> G : K --> dom F )
6 5 3ad2ant3 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G : K --> dom F )
7 fco 
 |-  ( ( F : dom F --> ( Base ` W ) /\ G : K --> dom F ) -> ( F o. G ) : K --> ( Base ` W ) )
8 4 6 7 syl2anc 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F o. G ) : K --> ( Base ` W ) )
9 8 ffdmd 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F o. G ) : dom ( F o. G ) --> ( Base ` W ) )
10 simpl2 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> F LIndF W )
11 6 adantr 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> G : K --> dom F )
12 8 fdmd 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> dom ( F o. G ) = K )
13 12 eleq2d 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( x e. dom ( F o. G ) <-> x e. K ) )
14 13 biimpa 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> x e. K )
15 11 14 ffvelcdmd 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( G ` x ) e. dom F )
16 15 adantrr 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( G ` x ) e. dom F )
17 eldifi 
 |-  ( k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -> k e. ( Base ` ( Scalar ` W ) ) )
18 17 ad2antll 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> k e. ( Base ` ( Scalar ` W ) ) )
19 eldifsni 
 |-  ( k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -> k =/= ( 0g ` ( Scalar ` W ) ) )
20 19 ad2antll 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> k =/= ( 0g ` ( Scalar ` W ) ) )
21 eqid 
 |-  ( .s ` W ) = ( .s ` W )
22 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
23 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
24 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
25 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
26 21 22 23 24 25 lindfind 
 |-  ( ( ( F LIndF W /\ ( G ` x ) e. dom F ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ k =/= ( 0g ` ( Scalar ` W ) ) ) ) -> -. ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) )
27 10 16 18 20 26 syl22anc 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> -. ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) )
28 f1fn 
 |-  ( G : K -1-1-> dom F -> G Fn K )
29 28 3ad2ant3 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G Fn K )
30 29 adantr 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> G Fn K )
31 fvco2 
 |-  ( ( G Fn K /\ x e. K ) -> ( ( F o. G ) ` x ) = ( F ` ( G ` x ) ) )
32 30 14 31 syl2anc 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( ( F o. G ) ` x ) = ( F ` ( G ` x ) ) )
33 32 oveq2d 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( k ( .s ` W ) ( ( F o. G ) ` x ) ) = ( k ( .s ` W ) ( F ` ( G ` x ) ) ) )
34 33 eleq1d 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) <-> ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) ) )
35 simpl1 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> W e. LMod )
36 imassrn 
 |-  ( F " ( dom F \ { ( G ` x ) } ) ) C_ ran F
37 4 frnd 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ran F C_ ( Base ` W ) )
38 36 37 sstrid 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F " ( dom F \ { ( G ` x ) } ) ) C_ ( Base ` W ) )
39 38 adantr 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( F " ( dom F \ { ( G ` x ) } ) ) C_ ( Base ` W ) )
40 imaco 
 |-  ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) = ( F " ( G " ( dom ( F o. G ) \ { x } ) ) )
41 12 difeq1d 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( dom ( F o. G ) \ { x } ) = ( K \ { x } ) )
42 41 imaeq2d 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( G " ( dom ( F o. G ) \ { x } ) ) = ( G " ( K \ { x } ) ) )
43 df-f1 
 |-  ( G : K -1-1-> dom F <-> ( G : K --> dom F /\ Fun `' G ) )
44 43 simprbi 
 |-  ( G : K -1-1-> dom F -> Fun `' G )
45 44 3ad2ant3 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> Fun `' G )
46 imadif 
 |-  ( Fun `' G -> ( G " ( K \ { x } ) ) = ( ( G " K ) \ ( G " { x } ) ) )
47 45 46 syl 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( G " ( K \ { x } ) ) = ( ( G " K ) \ ( G " { x } ) ) )
48 42 47 eqtrd 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( G " ( dom ( F o. G ) \ { x } ) ) = ( ( G " K ) \ ( G " { x } ) ) )
49 48 adantr 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( G " ( dom ( F o. G ) \ { x } ) ) = ( ( G " K ) \ ( G " { x } ) ) )
50 fnsnfv 
 |-  ( ( G Fn K /\ x e. K ) -> { ( G ` x ) } = ( G " { x } ) )
51 29 50 sylan 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> { ( G ` x ) } = ( G " { x } ) )
52 51 difeq2d 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( ( G " K ) \ { ( G ` x ) } ) = ( ( G " K ) \ ( G " { x } ) ) )
53 imassrn 
 |-  ( G " K ) C_ ran G
54 6 adantr 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> G : K --> dom F )
55 54 frnd 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ran G C_ dom F )
56 53 55 sstrid 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( G " K ) C_ dom F )
57 56 ssdifd 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( ( G " K ) \ { ( G ` x ) } ) C_ ( dom F \ { ( G ` x ) } ) )
58 52 57 eqsstrrd 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( ( G " K ) \ ( G " { x } ) ) C_ ( dom F \ { ( G ` x ) } ) )
59 49 58 eqsstrd 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( G " ( dom ( F o. G ) \ { x } ) ) C_ ( dom F \ { ( G ` x ) } ) )
60 imass2 
 |-  ( ( G " ( dom ( F o. G ) \ { x } ) ) C_ ( dom F \ { ( G ` x ) } ) -> ( F " ( G " ( dom ( F o. G ) \ { x } ) ) ) C_ ( F " ( dom F \ { ( G ` x ) } ) ) )
61 59 60 syl 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( F " ( G " ( dom ( F o. G ) \ { x } ) ) ) C_ ( F " ( dom F \ { ( G ` x ) } ) ) )
62 40 61 eqsstrid 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) C_ ( F " ( dom F \ { ( G ` x ) } ) ) )
63 1 22 lspss 
 |-  ( ( W e. LMod /\ ( F " ( dom F \ { ( G ` x ) } ) ) C_ ( Base ` W ) /\ ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) C_ ( F " ( dom F \ { ( G ` x ) } ) ) ) -> ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) C_ ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) )
64 35 39 62 63 syl3anc 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) C_ ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) )
65 14 64 syldan 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) C_ ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) )
66 65 sseld 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) -> ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) ) )
67 34 66 sylbid 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) -> ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) ) )
68 67 adantrr 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) -> ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) ) )
69 27 68 mtod 
 |-  ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> -. ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) )
70 69 ralrimivva 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> A. x e. dom ( F o. G ) A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) )
71 simp1 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> W e. LMod )
72 rellindf 
 |-  Rel LIndF
73 72 brrelex1i 
 |-  ( F LIndF W -> F e. _V )
74 73 3ad2ant2 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> F e. _V )
75 simp3 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G : K -1-1-> dom F )
76 74 dmexd 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> dom F e. _V )
77 f1dmex 
 |-  ( ( G : K -1-1-> dom F /\ dom F e. _V ) -> K e. _V )
78 75 76 77 syl2anc 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> K e. _V )
79 6 78 fexd 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G e. _V )
80 coexg 
 |-  ( ( F e. _V /\ G e. _V ) -> ( F o. G ) e. _V )
81 74 79 80 syl2anc 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F o. G ) e. _V )
82 1 21 22 23 25 24 islindf 
 |-  ( ( W e. LMod /\ ( F o. G ) e. _V ) -> ( ( F o. G ) LIndF W <-> ( ( F o. G ) : dom ( F o. G ) --> ( Base ` W ) /\ A. x e. dom ( F o. G ) A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) ) ) )
83 71 81 82 syl2anc 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( ( F o. G ) LIndF W <-> ( ( F o. G ) : dom ( F o. G ) --> ( Base ` W ) /\ A. x e. dom ( F o. G ) A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) ) ) )
84 9 70 83 mpbir2and 
 |-  ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F o. G ) LIndF W )