Metamath Proof Explorer

Theorem suppmptcfin

Description: The support of a mapping with value 0 except of one is finite. (Contributed by AV, 27-Apr-2019)

Ref Expression
Hypotheses suppmptcfin.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
suppmptcfin.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
suppmptcfin.0 ⊢ 0 = ( 0g ‘ 𝑅 )
suppmptcfin.1 ⊢ 1 = ( 1r ‘ 𝑅 )
suppmptcfin.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑋 , 1 , 0 ) )
Assertion suppmptcfin ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 supp 0 ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 suppmptcfin.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 suppmptcfin.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
3 suppmptcfin.0 ⊢ 0 = ( 0g ‘ 𝑅 )
4 suppmptcfin.1 ⊢ 1 = ( 1r ‘ 𝑅 )
5 suppmptcfin.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑋 , 1 , 0 ) )
6 eqeq1 ⊢ ( 𝑥 = 𝑣 → ( 𝑥 = 𝑋 ↔ 𝑣 = 𝑋 ) )
7 6 ifbid ⊢ ( 𝑥 = 𝑣 → if ( 𝑥 = 𝑋 , 1 , 0 ) = if ( 𝑣 = 𝑋 , 1 , 0 ) )
8 7 cbvmptv ⊢ ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑋 , 1 , 0 ) ) = ( 𝑣 ∈ 𝑉 ↦ if ( 𝑣 = 𝑋 , 1 , 0 ) )
9 5 8 eqtri ⊢ 𝐹 = ( 𝑣 ∈ 𝑉 ↦ if ( 𝑣 = 𝑋 , 1 , 0 ) )
10 simp2 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 𝑉 ∈ 𝒫 𝐵 )
11 3 fvexi ⊢ 0 ∈ V
12 11 a1i ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 0 ∈ V )
13 4 fvexi ⊢ 1 ∈ V
14 13 a1i ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) → 1 ∈ V )
15 11 a1i ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) → 0 ∈ V )
16 14 15 ifcld ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) → if ( 𝑣 = 𝑋 , 1 , 0 ) ∈ V )
17 9 10 12 16 mptsuppd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 supp 0 ) = { 𝑣 ∈ 𝑉 ∣ if ( 𝑣 = 𝑋 , 1 , 0 ) ≠ 0 } )
18 snfi ⊢ { 𝑋 } ∈ Fin
19 2a1 ⊢ ( 𝑣 = 𝑋 → ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) → ( if ( 𝑣 = 𝑋 , 1 , 0 ) ≠ 0 → 𝑣 = 𝑋 ) ) )
20 iffalse ⊢ ( ¬ 𝑣 = 𝑋 → if ( 𝑣 = 𝑋 , 1 , 0 ) = 0 )
21 20 adantr ⊢ ( ( ¬ 𝑣 = 𝑋 ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) ) → if ( 𝑣 = 𝑋 , 1 , 0 ) = 0 )
22 21 neeq1d ⊢ ( ( ¬ 𝑣 = 𝑋 ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) ) → ( if ( 𝑣 = 𝑋 , 1 , 0 ) ≠ 0 ↔ 0 ≠ 0 ) )
23 eqid ⊢ 0 = 0
24 eqneqall ⊢ ( 0 = 0 → ( 0 ≠ 0 → 𝑣 = 𝑋 ) )
25 23 24 ax-mp ⊢ ( 0 ≠ 0 → 𝑣 = 𝑋 )
26 22 25 biimtrdi ⊢ ( ( ¬ 𝑣 = 𝑋 ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) ) → ( if ( 𝑣 = 𝑋 , 1 , 0 ) ≠ 0 → 𝑣 = 𝑋 ) )
27 26 ex ⊢ ( ¬ 𝑣 = 𝑋 → ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) → ( if ( 𝑣 = 𝑋 , 1 , 0 ) ≠ 0 → 𝑣 = 𝑋 ) ) )
28 19 27 pm2.61i ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) → ( if ( 𝑣 = 𝑋 , 1 , 0 ) ≠ 0 → 𝑣 = 𝑋 ) )
29 28 ralrimiva ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ∀ 𝑣 ∈ 𝑉 ( if ( 𝑣 = 𝑋 , 1 , 0 ) ≠ 0 → 𝑣 = 𝑋 ) )
30 rabsssn ⊢ ( { 𝑣 ∈ 𝑉 ∣ if ( 𝑣 = 𝑋 , 1 , 0 ) ≠ 0 } ⊆ { 𝑋 } ↔ ∀ 𝑣 ∈ 𝑉 ( if ( 𝑣 = 𝑋 , 1 , 0 ) ≠ 0 → 𝑣 = 𝑋 ) )
31 29 30 sylibr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → { 𝑣 ∈ 𝑉 ∣ if ( 𝑣 = 𝑋 , 1 , 0 ) ≠ 0 } ⊆ { 𝑋 } )
32 ssfi ⊢ ( ( { 𝑋 } ∈ Fin ∧ { 𝑣 ∈ 𝑉 ∣ if ( 𝑣 = 𝑋 , 1 , 0 ) ≠ 0 } ⊆ { 𝑋 } ) → { 𝑣 ∈ 𝑉 ∣ if ( 𝑣 = 𝑋 , 1 , 0 ) ≠ 0 } ∈ Fin )
33 18 31 32 sylancr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → { 𝑣 ∈ 𝑉 ∣ if ( 𝑣 = 𝑋 , 1 , 0 ) ≠ 0 } ∈ Fin )
34 17 33 eqeltrd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 supp 0 ) ∈ Fin )