Metamath Proof Explorer

Theorem linindslinci

Description: The implications of being a linearly independent subset and a linear combination of this subset being 0. (Contributed by AV, 24-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 linindslinci ( ( 𝑆 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 1 2 3 4 5 linindsi ⊢ ( 𝑆 linIndS 𝑀 → ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
7 breq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 finSupp 0 ↔ 𝐹 finSupp 0 ) )
8 oveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 𝐹 ( linC ‘ 𝑀 ) 𝑆 ) )
9 8 eqeq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ↔ ( 𝐹 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) )
10 7 9 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ↔ ( 𝐹 finSupp 0 ∧ ( 𝐹 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) )
11 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
12 11 eqeq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ ( 𝐹 ‘ 𝑥 ) = 0 ) )
13 12 ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ↔ ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) = 0 ) )
14 10 13 imbi12d ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ↔ ( ( 𝐹 finSupp 0 ∧ ( 𝐹 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) = 0 ) ) )
15 14 rspcv ⊢ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) → ( ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) → ( ( 𝐹 finSupp 0 ∧ ( 𝐹 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) = 0 ) ) )
16 15 com23 ⊢ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) → ( ( 𝐹 finSupp 0 ∧ ( 𝐹 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ( ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) → ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) = 0 ) ) )
17 16 3impib ⊢ ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ 𝐹 finSupp 0 ∧ ( 𝐹 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ( ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) → ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) = 0 ) )
18 17 com12 ⊢ ( ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) → ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ 𝐹 finSupp 0 ∧ ( 𝐹 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) = 0 ) )
19 6 18 simpl2im ⊢ ( 𝑆 linIndS 𝑀 → ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ 𝐹 finSupp 0 ∧ ( 𝐹 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) = 0 ) )
20 19 imp ⊢ ( ( 𝑆 linIndS 𝑀 ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ 𝐹 finSupp 0 ∧ ( 𝐹 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) = 0 )