Metamath Proof Explorer

Theorem ressupprn

Description: The range of a function restricted to its support. (Contributed by Thierry Arnoux, 25-Jun-2024)

Ref Expression
Assertion ressupprn ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( ran 𝐹 ∖ { 0 } ) )

Proof

Step Hyp Ref Expression
1 funfn ⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
2 1 biimpi ⊢ ( Fun 𝐹 → 𝐹 Fn dom 𝐹 )
3 2 3ad2ant1 ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → 𝐹 Fn dom 𝐹 )
4 dmexg ⊢ ( 𝐹 ∈ 𝑉 → dom 𝐹 ∈ V )
5 4 3ad2ant2 ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → dom 𝐹 ∈ V )
6 simp3 ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → 0 ∈ 𝑊 )
7 elsuppfn ⊢ ( ( 𝐹 Fn dom 𝐹 ∧ dom 𝐹 ∈ V ∧ 0 ∈ 𝑊 ) → ( 𝑥 ∈ ( 𝐹 supp 0 ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ) )
8 3 5 6 7 syl3anc ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → ( 𝑥 ∈ ( 𝐹 supp 0 ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ) )
9 8 anbi1d ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → ( ( 𝑥 ∈ ( 𝐹 supp 0 ) ∧ ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = 𝑦 ) ↔ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ∧ ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = 𝑦 ) ) )
10 anass ⊢ ( ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ∧ ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = 𝑦 ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∧ ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = 𝑦 ) ) )
11 10 a1i ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → ( ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ∧ ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = 𝑦 ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∧ ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = 𝑦 ) ) ) )
12 8 biimprd ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) → 𝑥 ∈ ( 𝐹 supp 0 ) ) )
13 12 impl ⊢ ( ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) → 𝑥 ∈ ( 𝐹 supp 0 ) )
14 13 fvresd ⊢ ( ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) → ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
15 14 eqeq1d ⊢ ( ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) → ( ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
16 15 pm5.32da ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∧ ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) )
17 ancom ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) )
18 simpr ⊢ ( ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( 𝐹 ‘ 𝑥 ) = 𝑦 )
19 18 neeq1d ⊢ ( ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ↔ 𝑦 ≠ 0 ) )
20 19 pm5.32da ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 ≠ 0 ) ) )
21 17 20 syl5bb ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 ≠ 0 ) ) )
22 16 21 bitrd ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∧ ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 ≠ 0 ) ) )
23 22 pm5.32da ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → ( ( 𝑥 ∈ dom 𝐹 ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∧ ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = 𝑦 ) ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 ≠ 0 ) ) ) )
24 9 11 23 3bitrd ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → ( ( 𝑥 ∈ ( 𝐹 supp 0 ) ∧ ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = 𝑦 ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 ≠ 0 ) ) ) )
25 24 rexbidv2 ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → ( ∃ 𝑥 ∈ ( 𝐹 supp 0 ) ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = 𝑦 ↔ ∃ 𝑥 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 ≠ 0 ) ) )
26 suppssdm ⊢ ( 𝐹 supp 0 ) ⊆ dom 𝐹
27 fnssres ⊢ ( ( 𝐹 Fn dom 𝐹 ∧ ( 𝐹 supp 0 ) ⊆ dom 𝐹 ) → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) Fn ( 𝐹 supp 0 ) )
28 3 26 27 sylancl ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) Fn ( 𝐹 supp 0 ) )
29 fvelrnb ⊢ ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) Fn ( 𝐹 supp 0 ) → ( 𝑦 ∈ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↔ ∃ 𝑥 ∈ ( 𝐹 supp 0 ) ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = 𝑦 ) )
30 28 29 syl ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → ( 𝑦 ∈ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↔ ∃ 𝑥 ∈ ( 𝐹 supp 0 ) ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = 𝑦 ) )
31 fvelrnb ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ dom 𝐹 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
32 31 anbi1d ⊢ ( 𝐹 Fn dom 𝐹 → ( ( 𝑦 ∈ ran 𝐹 ∧ 𝑦 ≠ 0 ) ↔ ( ∃ 𝑥 ∈ dom 𝐹 ( 𝐹 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 ≠ 0 ) ) )
33 eldifsn ⊢ ( 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ↔ ( 𝑦 ∈ ran 𝐹 ∧ 𝑦 ≠ 0 ) )
34 r19.41v ⊢ ( ∃ 𝑥 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 ≠ 0 ) ↔ ( ∃ 𝑥 ∈ dom 𝐹 ( 𝐹 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 ≠ 0 ) )
35 32 33 34 3bitr4g ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ↔ ∃ 𝑥 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 ≠ 0 ) ) )
36 3 35 syl ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → ( 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ↔ ∃ 𝑥 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 ≠ 0 ) ) )
37 25 30 36 3bitr4d ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → ( 𝑦 ∈ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↔ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) )
38 37 eqrdv ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( ran 𝐹 ∖ { 0 } ) )