This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( Base ‘ 𝑊 )
Assertion lindff ( ( 𝐹 LIndF 𝑊 ∧ 𝑊 ∈ 𝑌 ) → 𝐹 : dom 𝐹 ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 lindff.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 simpl ⊢ ( ( 𝐹 LIndF 𝑊 ∧ 𝑊 ∈ 𝑌 ) → 𝐹 LIndF 𝑊 )
3 rellindf ⊢ Rel LIndF
4 3 brrelex1i ⊢ ( 𝐹 LIndF 𝑊 → 𝐹 ∈ V )
5 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
6 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
7 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
8 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
9 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
10 1 5 6 7 8 9 islindf ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐹 ∈ V ) → ( 𝐹 LIndF 𝑊 ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )
11 4 10 sylan2 ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐹 LIndF 𝑊 ) → ( 𝐹 LIndF 𝑊 ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )
12 11 ancoms ⊢ ( ( 𝐹 LIndF 𝑊 ∧ 𝑊 ∈ 𝑌 ) → ( 𝐹 LIndF 𝑊 ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )
13 2 12 mpbid ⊢ ( ( 𝐹 LIndF 𝑊 ∧ 𝑊 ∈ 𝑌 ) → ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) )
14 13 simpld ⊢ ( ( 𝐹 LIndF 𝑊 ∧ 𝑊 ∈ 𝑌 ) → 𝐹 : dom 𝐹 ⟶ 𝐵 )