Metamath Proof Explorer

Theorem lsslindf

Description: Linear independence is unchanged by working in a subspace. (Contributed by Stefan O'Rear, 24-Feb-2015) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypotheses lsslindf.u 
|- U = ( LSubSp ` W )
lsslindf.x 
|- X = ( W |`s S )
Assertion lsslindf 
|- ( ( W e. LMod /\ S e. U /\ ran F C_ S ) -> ( F LIndF X <-> F LIndF W ) )

Proof

Step Hyp Ref Expression
1 lsslindf.u 
 |-  U = ( LSubSp ` W )
2 lsslindf.x 
 |-  X = ( W |`s S )
3 rellindf 
 |-  Rel LIndF
4 3 brrelex1i 
 |-  ( F LIndF X -> F e. _V )
5 4 a1i 
 |-  ( ( W e. LMod /\ S e. U /\ ran F C_ S ) -> ( F LIndF X -> F e. _V ) )
6 3 brrelex1i 
 |-  ( F LIndF W -> F e. _V )
7 6 a1i 
 |-  ( ( W e. LMod /\ S e. U /\ ran F C_ S ) -> ( F LIndF W -> F e. _V ) )
8 simpr 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F : dom F --> ( Base ` X ) ) -> F : dom F --> ( Base ` X ) )
9 eqid 
 |-  ( Base ` W ) = ( Base ` W )
10 2 9 ressbasss 
 |-  ( Base ` X ) C_ ( Base ` W )
11 fss 
 |-  ( ( F : dom F --> ( Base ` X ) /\ ( Base ` X ) C_ ( Base ` W ) ) -> F : dom F --> ( Base ` W ) )
12 8 10 11 sylancl 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F : dom F --> ( Base ` X ) ) -> F : dom F --> ( Base ` W ) )
13 ffn 
 |-  ( F : dom F --> ( Base ` W ) -> F Fn dom F )
14 13 adantl 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F : dom F --> ( Base ` W ) ) -> F Fn dom F )
15 simp3 
 |-  ( ( W e. LMod /\ S e. U /\ ran F C_ S ) -> ran F C_ S )
16 9 1 lssss 
 |-  ( S e. U -> S C_ ( Base ` W ) )
17 16 3ad2ant2 
 |-  ( ( W e. LMod /\ S e. U /\ ran F C_ S ) -> S C_ ( Base ` W ) )
18 2 9 ressbas2 
 |-  ( S C_ ( Base ` W ) -> S = ( Base ` X ) )
19 17 18 syl 
 |-  ( ( W e. LMod /\ S e. U /\ ran F C_ S ) -> S = ( Base ` X ) )
20 15 19 sseqtrd 
 |-  ( ( W e. LMod /\ S e. U /\ ran F C_ S ) -> ran F C_ ( Base ` X ) )
21 20 adantr 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F : dom F --> ( Base ` W ) ) -> ran F C_ ( Base ` X ) )
22 df-f 
 |-  ( F : dom F --> ( Base ` X ) <-> ( F Fn dom F /\ ran F C_ ( Base ` X ) ) )
23 14 21 22 sylanbrc 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F : dom F --> ( Base ` W ) ) -> F : dom F --> ( Base ` X ) )
24 12 23 impbida 
 |-  ( ( W e. LMod /\ S e. U /\ ran F C_ S ) -> ( F : dom F --> ( Base ` X ) <-> F : dom F --> ( Base ` W ) ) )
25 24 adantr 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> ( F : dom F --> ( Base ` X ) <-> F : dom F --> ( Base ` W ) ) )
26 simpl2 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> S e. U )
27 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
28 2 27 resssca 
 |-  ( S e. U -> ( Scalar ` W ) = ( Scalar ` X ) )
29 28 eqcomd 
 |-  ( S e. U -> ( Scalar ` X ) = ( Scalar ` W ) )
30 26 29 syl 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> ( Scalar ` X ) = ( Scalar ` W ) )
31 30 fveq2d 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> ( Base ` ( Scalar ` X ) ) = ( Base ` ( Scalar ` W ) ) )
32 30 fveq2d 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> ( 0g ` ( Scalar ` X ) ) = ( 0g ` ( Scalar ` W ) ) )
33 32 sneqd 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> { ( 0g ` ( Scalar ` X ) ) } = { ( 0g ` ( Scalar ` W ) ) } )
34 31 33 difeq12d 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> ( ( Base ` ( Scalar ` X ) ) \ { ( 0g ` ( Scalar ` X ) ) } ) = ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) )
35 eqid 
 |-  ( .s ` W ) = ( .s ` W )
36 2 35 ressvsca 
 |-  ( S e. U -> ( .s ` W ) = ( .s ` X ) )
37 36 eqcomd 
 |-  ( S e. U -> ( .s ` X ) = ( .s ` W ) )
38 26 37 syl 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> ( .s ` X ) = ( .s ` W ) )
39 38 oveqd 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> ( k ( .s ` X ) ( F ` x ) ) = ( k ( .s ` W ) ( F ` x ) ) )
40 simpl1 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> W e. LMod )
41 imassrn 
 |-  ( F " ( dom F \ { x } ) ) C_ ran F
42 simpl3 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> ran F C_ S )
43 41 42 sstrid 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> ( F " ( dom F \ { x } ) ) C_ S )
44 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
45 eqid 
 |-  ( LSpan ` X ) = ( LSpan ` X )
46 2 44 45 1 lsslsp 
 |-  ( ( W e. LMod /\ S e. U /\ ( F " ( dom F \ { x } ) ) C_ S ) -> ( ( LSpan ` W ) ` ( F " ( dom F \ { x } ) ) ) = ( ( LSpan ` X ) ` ( F " ( dom F \ { x } ) ) ) )
47 40 26 43 46 syl3anc 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> ( ( LSpan ` W ) ` ( F " ( dom F \ { x } ) ) ) = ( ( LSpan ` X ) ` ( F " ( dom F \ { x } ) ) ) )
48 47 eqcomd 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> ( ( LSpan ` X ) ` ( F " ( dom F \ { x } ) ) ) = ( ( LSpan ` W ) ` ( F " ( dom F \ { x } ) ) ) )
49 39 48 eleq12d 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> ( ( k ( .s ` X ) ( F ` x ) ) e. ( ( LSpan ` X ) ` ( F " ( dom F \ { x } ) ) ) <-> ( k ( .s ` W ) ( F ` x ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { x } ) ) ) ) )
50 49 notbid 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> ( -. ( k ( .s ` X ) ( F ` x ) ) e. ( ( LSpan ` X ) ` ( F " ( dom F \ { x } ) ) ) <-> -. ( k ( .s ` W ) ( F ` x ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { x } ) ) ) ) )
51 34 50 raleqbidv 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> ( A. k e. ( ( Base ` ( Scalar ` X ) ) \ { ( 0g ` ( Scalar ` X ) ) } ) -. ( k ( .s ` X ) ( F ` x ) ) e. ( ( LSpan ` X ) ` ( F " ( dom F \ { x } ) ) ) <-> A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) ( F ` x ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { x } ) ) ) ) )
52 51 ralbidv 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> ( A. x e. dom F A. k e. ( ( Base ` ( Scalar ` X ) ) \ { ( 0g ` ( Scalar ` X ) ) } ) -. ( k ( .s ` X ) ( F ` x ) ) e. ( ( LSpan ` X ) ` ( F " ( dom F \ { x } ) ) ) <-> A. x e. dom F A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) ( F ` x ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { x } ) ) ) ) )
53 25 52 anbi12d 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> ( ( F : dom F --> ( Base ` X ) /\ A. x e. dom F A. k e. ( ( Base ` ( Scalar ` X ) ) \ { ( 0g ` ( Scalar ` X ) ) } ) -. ( k ( .s ` X ) ( F ` x ) ) e. ( ( LSpan ` X ) ` ( F " ( dom F \ { x } ) ) ) ) <-> ( F : dom F --> ( Base ` W ) /\ A. x e. dom F A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) ( F ` x ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { x } ) ) ) ) ) )
54 2 ovexi 
 |-  X e. _V
55 54 a1i 
 |-  ( ( W e. LMod /\ S e. U /\ ran F C_ S ) -> X e. _V )
56 eqid 
 |-  ( Base ` X ) = ( Base ` X )
57 eqid 
 |-  ( .s ` X ) = ( .s ` X )
58 eqid 
 |-  ( Scalar ` X ) = ( Scalar ` X )
59 eqid 
 |-  ( Base ` ( Scalar ` X ) ) = ( Base ` ( Scalar ` X ) )
60 eqid 
 |-  ( 0g ` ( Scalar ` X ) ) = ( 0g ` ( Scalar ` X ) )
61 56 57 45 58 59 60 islindf 
 |-  ( ( X e. _V /\ F e. _V ) -> ( F LIndF X <-> ( F : dom F --> ( Base ` X ) /\ A. x e. dom F A. k e. ( ( Base ` ( Scalar ` X ) ) \ { ( 0g ` ( Scalar ` X ) ) } ) -. ( k ( .s ` X ) ( F ` x ) ) e. ( ( LSpan ` X ) ` ( F " ( dom F \ { x } ) ) ) ) ) )
62 55 61 sylan 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> ( F LIndF X <-> ( F : dom F --> ( Base ` X ) /\ A. x e. dom F A. k e. ( ( Base ` ( Scalar ` X ) ) \ { ( 0g ` ( Scalar ` X ) ) } ) -. ( k ( .s ` X ) ( F ` x ) ) e. ( ( LSpan ` X ) ` ( F " ( dom F \ { x } ) ) ) ) ) )
63 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
64 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
65 9 35 44 27 63 64 islindf 
 |-  ( ( W e. LMod /\ F e. _V ) -> ( F LIndF W <-> ( F : dom F --> ( Base ` W ) /\ A. x e. dom F A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) ( F ` x ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { x } ) ) ) ) ) )
66 65 3ad2antl1 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> ( F LIndF W <-> ( F : dom F --> ( Base ` W ) /\ A. x e. dom F A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) ( F ` x ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { x } ) ) ) ) ) )
67 53 62 66 3bitr4d 
 |-  ( ( ( W e. LMod /\ S e. U /\ ran F C_ S ) /\ F e. _V ) -> ( F LIndF X <-> F LIndF W ) )
68 67 ex 
 |-  ( ( W e. LMod /\ S e. U /\ ran F C_ S ) -> ( F e. _V -> ( F LIndF X <-> F LIndF W ) ) )
69 5 7 68 pm5.21ndd 
 |-  ( ( W e. LMod /\ S e. U /\ ran F C_ S ) -> ( F LIndF X <-> F LIndF W ) )