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 ⊢ B × Z supp Z = ∅

Proof

Step Hyp Ref Expression
1 eqidd ⊢ B × Z ∈ V ∧ Z ∈ V → B × Z = B × Z
2 fnconstg ⊢ Z ∈ V → B × Z Fn B
3 2 adantl ⊢ B × Z ∈ V ∧ Z ∈ V → B × Z Fn B
4 snnzg ⊢ Z ∈ V → Z ≠ ∅
5 simpl ⊢ B × Z ∈ V ∧ Z ∈ V → B × Z ∈ V
6 xpexcnv ⊢ Z ≠ ∅ ∧ B × Z ∈ V → B ∈ V
7 4 5 6 syl2an2 ⊢ B × Z ∈ V ∧ Z ∈ V → B ∈ V
8 simpr ⊢ B × Z ∈ V ∧ Z ∈ V → Z ∈ V
9 fnsuppeq0 ⊢ B × Z Fn B ∧ B ∈ V ∧ Z ∈ V → B × Z supp Z = ∅ ↔ B × Z = B × Z
10 3 7 8 9 syl3anc ⊢ B × Z ∈ V ∧ Z ∈ V → B × Z supp Z = ∅ ↔ B × Z = B × Z
11 1 10 mpbird ⊢ B × Z ∈ V ∧ Z ∈ V → B × Z supp Z = ∅
12 supp0prc ⊢ ¬ B × Z ∈ V ∧ Z ∈ V → B × Z supp Z = ∅
13 11 12 pm2.61i ⊢ B × Z supp Z = ∅