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		0fin	⊢ ∅ ∈ 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 𝑍 )