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 𝐹 ⟶ 𝐵 )