# Metamath Proof Explorer

## Theorem fczsupp0

Description: The support of a constant function with value zero is empty. (Contributed by AV, 30-Jun-2019)

Ref Expression
Assertion fczsupp0 ${⊢}\left({B}×\left\{{Z}\right\}\right)\mathrm{supp}{Z}=\varnothing$

### Proof

Step Hyp Ref Expression
1 eqidd ${⊢}\left({B}×\left\{{Z}\right\}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to {B}×\left\{{Z}\right\}={B}×\left\{{Z}\right\}$
2 fnconstg ${⊢}{Z}\in \mathrm{V}\to \left({B}×\left\{{Z}\right\}\right)Fn{B}$
3 2 adantl ${⊢}\left({B}×\left\{{Z}\right\}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to \left({B}×\left\{{Z}\right\}\right)Fn{B}$
4 snnzg ${⊢}{Z}\in \mathrm{V}\to \left\{{Z}\right\}\ne \varnothing$
5 simpl ${⊢}\left({B}×\left\{{Z}\right\}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to {B}×\left\{{Z}\right\}\in \mathrm{V}$
6 xpexcnv ${⊢}\left(\left\{{Z}\right\}\ne \varnothing \wedge {B}×\left\{{Z}\right\}\in \mathrm{V}\right)\to {B}\in \mathrm{V}$
7 4 5 6 syl2an2 ${⊢}\left({B}×\left\{{Z}\right\}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to {B}\in \mathrm{V}$
8 simpr ${⊢}\left({B}×\left\{{Z}\right\}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to {Z}\in \mathrm{V}$
9 fnsuppeq0 ${⊢}\left(\left({B}×\left\{{Z}\right\}\right)Fn{B}\wedge {B}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to \left(\left({B}×\left\{{Z}\right\}\right)\mathrm{supp}{Z}=\varnothing ↔{B}×\left\{{Z}\right\}={B}×\left\{{Z}\right\}\right)$
10 3 7 8 9 syl3anc ${⊢}\left({B}×\left\{{Z}\right\}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to \left(\left({B}×\left\{{Z}\right\}\right)\mathrm{supp}{Z}=\varnothing ↔{B}×\left\{{Z}\right\}={B}×\left\{{Z}\right\}\right)$
11 1 10 mpbird ${⊢}\left({B}×\left\{{Z}\right\}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to \left({B}×\left\{{Z}\right\}\right)\mathrm{supp}{Z}=\varnothing$
12 supp0prc ${⊢}¬\left({B}×\left\{{Z}\right\}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to \left({B}×\left\{{Z}\right\}\right)\mathrm{supp}{Z}=\varnothing$
13 11 12 pm2.61i ${⊢}\left({B}×\left\{{Z}\right\}\right)\mathrm{supp}{Z}=\varnothing$