Theorem islinindfiss

Description: The property of being a linearly independent finite subset. (Contributed by AV, 27-Apr-2019)

	Ref	Expression
Hypotheses	islininds.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	islininds.z	⊢ 𝑍 = ( 0g ‘ 𝑀 )
	islininds.r	⊢ 𝑅 = ( Scalar ‘ 𝑀 )
	islininds.e	⊢ 𝐸 = ( Base ‘ 𝑅 )
	islininds.0	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	islinindfiss	⊢ ( ( 𝑀 ∈ 𝑊 ∧ 𝑆 ∈ Fin ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( 𝑆 linIndS 𝑀 ↔ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		islininds.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		islininds.z	⊢ 𝑍 = ( 0g ‘ 𝑀 )
3		islininds.r	⊢ 𝑅 = ( Scalar ‘ 𝑀 )
4		islininds.e	⊢ 𝐸 = ( Base ‘ 𝑅 )
5		islininds.0	⊢ 0 = ( 0g ‘ 𝑅 )
6	1 2 3 4 5	islinindfis	⊢ ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊 ) → ( 𝑆 linIndS 𝑀 ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )
7	6	ancoms	⊢ ( ( 𝑀 ∈ 𝑊 ∧ 𝑆 ∈ Fin ) → ( 𝑆 linIndS 𝑀 ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )
8	7	3adant3	⊢ ( ( 𝑀 ∈ 𝑊 ∧ 𝑆 ∈ Fin ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( 𝑆 linIndS 𝑀 ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )
9	8	3anibar	⊢ ( ( 𝑀 ∈ 𝑊 ∧ 𝑆 ∈ Fin ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( 𝑆 linIndS 𝑀 ↔ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )