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

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 ( ( 𝐵 × { 𝑍 } ) supp 𝑍 ) = ∅

Proof

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