Metamath Proof Explorer

Theorem linindsi

Description: The implications of being a linearly independent subset. (Contributed by AV, 13-Apr-2019) (Revised by AV, 30-Jul-2019)

Ref Expression
Hypotheses islininds.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
islininds.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
islininds.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
islininds.e ⊢ 𝐸 = ( Base ‘ 𝑅 )
islininds.0 ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion linindsi ( 𝑆 linIndS 𝑀 → ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( 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 linindsv ⊢ ( 𝑆 linIndS 𝑀 → ( 𝑆 ∈ V ∧ 𝑀 ∈ V ) )
7 1 2 3 4 5 islininds ⊢ ( ( 𝑆 ∈ V ∧ 𝑀 ∈ V ) → ( 𝑆 linIndS 𝑀 ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )
8 6 7 syl ⊢ ( 𝑆 linIndS 𝑀 → ( 𝑆 linIndS 𝑀 ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )
9 8 ibi ⊢ ( 𝑆 linIndS 𝑀 → ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )