This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fczfsuppd

Description: A constant function with value zero is finitely supported. (Contributed by AV, 30-Jun-2019)

Ref Expression
Hypotheses fczfsuppd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
fczfsuppd.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
Assertion fczfsuppd ( 𝜑 → ( 𝐵 × { 𝑍 } ) finSupp 𝑍 )

Proof

Step Hyp Ref Expression
1 fczfsuppd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
2 fczfsuppd.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
3 fnconstg ⊢ ( 𝑍 ∈ 𝑊 → ( 𝐵 × { 𝑍 } ) Fn 𝐵 )
4 fnfun ⊢ ( ( 𝐵 × { 𝑍 } ) Fn 𝐵 → Fun ( 𝐵 × { 𝑍 } ) )
5 2 3 4 3syl ⊢ ( 𝜑 → Fun ( 𝐵 × { 𝑍 } ) )
6 fczsupp0 ⊢ ( ( 𝐵 × { 𝑍 } ) supp 𝑍 ) = ∅
7 0fi ⊢ ∅ ∈ Fin
8 6 7 eqeltri ⊢ ( ( 𝐵 × { 𝑍 } ) supp 𝑍 ) ∈ Fin
9 8 a1i ⊢ ( 𝜑 → ( ( 𝐵 × { 𝑍 } ) supp 𝑍 ) ∈ Fin )
10 snex ⊢ { 𝑍 } ∈ V
11 xpexg ⊢ ( ( 𝐵 ∈ 𝑉 ∧ { 𝑍 } ∈ V ) → ( 𝐵 × { 𝑍 } ) ∈ V )
12 1 10 11 sylancl ⊢ ( 𝜑 → ( 𝐵 × { 𝑍 } ) ∈ V )
13 isfsupp ⊢ ( ( ( 𝐵 × { 𝑍 } ) ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝐵 × { 𝑍 } ) finSupp 𝑍 ↔ ( Fun ( 𝐵 × { 𝑍 } ) ∧ ( ( 𝐵 × { 𝑍 } ) supp 𝑍 ) ∈ Fin ) ) )
14 12 2 13 syl2anc ⊢ ( 𝜑 → ( ( 𝐵 × { 𝑍 } ) finSupp 𝑍 ↔ ( Fun ( 𝐵 × { 𝑍 } ) ∧ ( ( 𝐵 × { 𝑍 } ) supp 𝑍 ) ∈ Fin ) ) )
15 5 9 14 mpbir2and ⊢ ( 𝜑 → ( 𝐵 × { 𝑍 } ) finSupp 𝑍 )