Metamath Proof Explorer

Theorem lindff

Description: Functional property of a linearly independent family. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Hypothesis lindff.b 
|- B = ( Base ` W )
Assertion lindff 
|- ( ( F LIndF W /\ W e. Y ) -> F : dom F --> B )

Proof

Step Hyp Ref Expression
1 lindff.b 
 |-  B = ( Base ` W )
2 simpl 
 |-  ( ( F LIndF W /\ W e. Y ) -> F LIndF W )
3 rellindf 
 |-  Rel LIndF
4 3 brrelex1i 
 |-  ( F LIndF W -> F e. _V )
5 eqid 
 |-  ( .s ` W ) = ( .s ` W )
6 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
7 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
8 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
9 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
10 1 5 6 7 8 9 islindf 
 |-  ( ( W e. Y /\ F e. _V ) -> ( F LIndF W <-> ( F : dom F --> B /\ 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 } ) ) ) ) ) )
11 4 10 sylan2 
 |-  ( ( W e. Y /\ F LIndF W ) -> ( F LIndF W <-> ( F : dom F --> B /\ 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 } ) ) ) ) ) )
12 11 ancoms 
 |-  ( ( F LIndF W /\ W e. Y ) -> ( F LIndF W <-> ( F : dom F --> B /\ 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 } ) ) ) ) ) )
13 2 12 mpbid 
 |-  ( ( F LIndF W /\ W e. Y ) -> ( F : dom F --> B /\ 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 } ) ) ) ) )
14 13 simpld 
 |-  ( ( F LIndF W /\ W e. Y ) -> F : dom F --> B )