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

Metamath Proof Explorer

Theorem psrbasfsupp

Description: Rewrite a finite support for nonnegative integers : For functions mapping a set I to the nonnegative integers, having finite support can also be written as having a finite preimage of the positive integers. The latter expression is used for example in psrbas , but with the former expression, theorems about finite support can be used more directly. (Contributed by Thierry Arnoux, 10-Jan-2026)

Ref Expression
Hypothesis psrbasfsupp.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ 𝑓 finSupp 0 }
Assertion psrbasfsupp 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }

Proof

Step Hyp Ref Expression
1 psrbasfsupp.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ 𝑓 finSupp 0 }
2 0nn0 ⊢ 0 ∈ ℕ0
3 isfsupp ⊢ ( ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∧ 0 ∈ ℕ0 ) → ( 𝑓 finSupp 0 ↔ ( Fun 𝑓 ∧ ( 𝑓 supp 0 ) ∈ Fin ) ) )
4 2 3 mpan2 ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( 𝑓 finSupp 0 ↔ ( Fun 𝑓 ∧ ( 𝑓 supp 0 ) ∈ Fin ) ) )
5 elmapfun ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → Fun 𝑓 )
6 5 biantrurd ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( ( 𝑓 supp 0 ) ∈ Fin ↔ ( Fun 𝑓 ∧ ( 𝑓 supp 0 ) ∈ Fin ) ) )
7 dfn2 ⊢ ℕ = ( ℕ0 ∖ { 0 } )
8 7 ineq2i ⊢ ( ran 𝑓 ∩ ℕ ) = ( ran 𝑓 ∩ ( ℕ0 ∖ { 0 } ) )
9 incom ⊢ ( ran 𝑓 ∩ ℕ ) = ( ℕ ∩ ran 𝑓 )
10 indif2 ⊢ ( ran 𝑓 ∩ ( ℕ0 ∖ { 0 } ) ) = ( ( ran 𝑓 ∩ ℕ0 ) ∖ { 0 } )
11 8 9 10 3eqtr3i ⊢ ( ℕ ∩ ran 𝑓 ) = ( ( ran 𝑓 ∩ ℕ0 ) ∖ { 0 } )
12 elmapi ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → 𝑓 : 𝐼 ⟶ ℕ0 )
13 12 frnd ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ran 𝑓 ⊆ ℕ0 )
14 dfss2 ⊢ ( ran 𝑓 ⊆ ℕ0 ↔ ( ran 𝑓 ∩ ℕ0 ) = ran 𝑓 )
15 13 14 sylib ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( ran 𝑓 ∩ ℕ0 ) = ran 𝑓 )
16 15 difeq1d ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( ( ran 𝑓 ∩ ℕ0 ) ∖ { 0 } ) = ( ran 𝑓 ∖ { 0 } ) )
17 11 16 eqtrid ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( ℕ ∩ ran 𝑓 ) = ( ran 𝑓 ∖ { 0 } ) )
18 17 imaeq2d ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( ◡ 𝑓 “ ( ℕ ∩ ran 𝑓 ) ) = ( ◡ 𝑓 “ ( ran 𝑓 ∖ { 0 } ) ) )
19 fimacnvinrn ⊢ ( Fun 𝑓 → ( ◡ 𝑓 “ ℕ ) = ( ◡ 𝑓 “ ( ℕ ∩ ran 𝑓 ) ) )
20 5 19 syl ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( ◡ 𝑓 “ ℕ ) = ( ◡ 𝑓 “ ( ℕ ∩ ran 𝑓 ) ) )
21 id ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) )
22 2 a1i ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → 0 ∈ ℕ0 )
23 supppreima ⊢ ( ( Fun 𝑓 ∧ 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∧ 0 ∈ ℕ0 ) → ( 𝑓 supp 0 ) = ( ◡ 𝑓 “ ( ran 𝑓 ∖ { 0 } ) ) )
24 5 21 22 23 syl3anc ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( 𝑓 supp 0 ) = ( ◡ 𝑓 “ ( ran 𝑓 ∖ { 0 } ) ) )
25 18 20 24 3eqtr4rd ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( 𝑓 supp 0 ) = ( ◡ 𝑓 “ ℕ ) )
26 25 eleq1d ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( ( 𝑓 supp 0 ) ∈ Fin ↔ ( ◡ 𝑓 “ ℕ ) ∈ Fin ) )
27 4 6 26 3bitr2d ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( 𝑓 finSupp 0 ↔ ( ◡ 𝑓 “ ℕ ) ∈ Fin ) )
28 27 rabbiia ⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ 𝑓 finSupp 0 } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
29 1 28 eqtri ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }