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=BaseW
Assertion lindff ⊢FLIndFW∧W∈Y→F:dom⁡F⟶B

Proof

Step Hyp Ref Expression
1 lindff.b ⊢B=BaseW
2 simpl ⊢FLIndFW∧W∈Y→FLIndFW
3 rellindf ⊢Rel⁡LIndF
4 3 brrelex1i ⊢FLIndFW→F∈V
5 eqid ⊢⋅W=⋅W
6 eqid ⊢LSpan⁡W=LSpan⁡W
7 eqid ⊢Scalar⁡W=Scalar⁡W
8 eqid ⊢BaseScalar⁡W=BaseScalar⁡W
9 eqid ⊢0Scalar⁡W=0Scalar⁡W
10 1 5 6 7 8 9 islindf ⊢W∈Y∧F∈V→FLIndFW↔F:dom⁡F⟶B∧∀x∈dom⁡F∀k∈BaseScalar⁡W∖0Scalar⁡W¬k⋅WF⁡x∈LSpan⁡W⁡Fdom⁡F∖x
11 4 10 sylan2 ⊢W∈Y∧FLIndFW→FLIndFW↔F:dom⁡F⟶B∧∀x∈dom⁡F∀k∈BaseScalar⁡W∖0Scalar⁡W¬k⋅WF⁡x∈LSpan⁡W⁡Fdom⁡F∖x
12 11 ancoms ⊢FLIndFW∧W∈Y→FLIndFW↔F:dom⁡F⟶B∧∀x∈dom⁡F∀k∈BaseScalar⁡W∖0Scalar⁡W¬k⋅WF⁡x∈LSpan⁡W⁡Fdom⁡F∖x
13 2 12 mpbid ⊢FLIndFW∧W∈Y→F:dom⁡F⟶B∧∀x∈dom⁡F∀k∈BaseScalar⁡W∖0Scalar⁡W¬k⋅WF⁡x∈LSpan⁡W⁡Fdom⁡F∖x
14 13 simpld ⊢FLIndFW∧W∈Y→F:dom⁡F⟶B