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 ∈ Y → F : dom ⁡ F ⟶ B

Proof

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