Metamath Proof Explorer

Theorem lcoc0

Description: Properties of a linear combination where all scalars are 0. (Contributed by AV, 12-Apr-2019) (Revised by AV, 28-Jul-2019)

Ref Expression
Hypotheses lincvalsc0.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
lincvalsc0.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
lincvalsc0.0 ⊢ 0 = ( 0g ‘ 𝑆 )
lincvalsc0.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
lincvalsc0.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ 0 )
lcoc0.r ⊢ 𝑅 = ( Base ‘ 𝑆 )
Assertion lcoc0 ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ∧ ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = 𝑍 ) )

Proof

Step Hyp Ref Expression
1 lincvalsc0.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 lincvalsc0.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
3 lincvalsc0.0 ⊢ 0 = ( 0g ‘ 𝑆 )
4 lincvalsc0.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
5 lincvalsc0.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ 0 )
6 lcoc0.r ⊢ 𝑅 = ( Base ‘ 𝑆 )
7 2 6 3 lmod0cl ⊢ ( 𝑀 ∈ LMod → 0 ∈ 𝑅 )
8 7 ad2antrr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝑉 ) → 0 ∈ 𝑅 )
9 8 5 fmptd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝐹 : 𝑉 ⟶ 𝑅 )
10 6 fvexi ⊢ 𝑅 ∈ V
11 10 a1i ⊢ ( 𝑀 ∈ LMod → 𝑅 ∈ V )
12 elmapg ⊢ ( ( 𝑅 ∈ V ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ∈ ( 𝑅 ↑m 𝑉 ) ↔ 𝐹 : 𝑉 ⟶ 𝑅 ) )
13 11 12 sylan ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ∈ ( 𝑅 ↑m 𝑉 ) ↔ 𝐹 : 𝑉 ⟶ 𝑅 ) )
14 9 13 mpbird ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝐹 ∈ ( 𝑅 ↑m 𝑉 ) )
15 eqidd ⊢ ( 𝑥 = 𝑣 → 0 = 0 )
16 15 cbvmptv ⊢ ( 𝑥 ∈ 𝑉 ↦ 0 ) = ( 𝑣 ∈ 𝑉 ↦ 0 )
17 5 16 eqtri ⊢ 𝐹 = ( 𝑣 ∈ 𝑉 ↦ 0 )
18 simpr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑉 ∈ 𝒫 𝐵 )
19 3 fvexi ⊢ 0 ∈ V
20 19 a1i ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 0 ∈ V )
21 19 a1i ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → 0 ∈ V )
22 17 18 20 21 mptsuppd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 supp 0 ) = { 𝑣 ∈ 𝑉 ∣ 0 ≠ 0 } )
23 neirr ⊢ ¬ 0 ≠ 0
24 23 a1i ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ¬ 0 ≠ 0 )
25 24 ralrimivw ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ∀ 𝑣 ∈ 𝑉 ¬ 0 ≠ 0 )
26 rabeq0 ⊢ ( { 𝑣 ∈ 𝑉 ∣ 0 ≠ 0 } = ∅ ↔ ∀ 𝑣 ∈ 𝑉 ¬ 0 ≠ 0 )
27 25 26 sylibr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → { 𝑣 ∈ 𝑉 ∣ 0 ≠ 0 } = ∅ )
28 0fin ⊢ ∅ ∈ Fin
29 28 a1i ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ∅ ∈ Fin )
30 27 29 eqeltrd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → { 𝑣 ∈ 𝑉 ∣ 0 ≠ 0 } ∈ Fin )
31 22 30 eqeltrd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 supp 0 ) ∈ Fin )
32 5 funmpt2 ⊢ Fun 𝐹
33 32 a1i ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → Fun 𝐹 )
34 funisfsupp ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 0 ∈ V ) → ( 𝐹 finSupp 0 ↔ ( 𝐹 supp 0 ) ∈ Fin ) )
35 33 14 20 34 syl3anc ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 finSupp 0 ↔ ( 𝐹 supp 0 ) ∈ Fin ) )
36 31 35 mpbird ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝐹 finSupp 0 )
37 1 2 3 4 5 lincvalsc0 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = 𝑍 )
38 14 36 37 3jca ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ∧ ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = 𝑍 ) )