Metamath Proof Explorer

Theorem rnplynfin

Description: The range of a nonconstant polynomial is not a finite set. (Contributed by SN, 30-Aug-2026)

Ref Expression
Hypotheses rnplynfin.f ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
rnplynfin.1 ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ≠ 0 )
Assertion rnplynfin ( 𝜑 → ¬ ran 𝐹 ∈ Fin )

Proof

Step Hyp Ref Expression
1 rnplynfin.f ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
2 rnplynfin.1 ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ≠ 0 )
3 plyf ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
4 1 3 syl ⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ )
5 4 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ℂ )
6 plyssc ⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
7 6 1 sselid ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℂ ) )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
9 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
10 plyconst ⊢ ( ( ℂ ⊆ ℂ ∧ 𝑥 ∈ ℂ ) → ( ℂ × { 𝑥 } ) ∈ ( Poly ‘ ℂ ) )
11 9 10 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ℂ × { 𝑥 } ) ∈ ( Poly ‘ ℂ ) )
12 plysubcl ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ ( ℂ × { 𝑥 } ) ∈ ( Poly ‘ ℂ ) ) → ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ∈ ( Poly ‘ ℂ ) )
13 8 11 12 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ∈ ( Poly ‘ ℂ ) )
14 2 neneqd ⊢ ( 𝜑 → ¬ ( deg ‘ 𝐹 ) = 0 )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ¬ ( deg ‘ 𝐹 ) = 0 )
16 0dgr ⊢ ( 𝑥 ∈ ℂ → ( deg ‘ ( ℂ × { 𝑥 } ) ) = 0 )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( deg ‘ ( ℂ × { 𝑥 } ) ) = 0 )
18 fveqeq2 ⊢ ( 𝐹 = ( ℂ × { 𝑥 } ) → ( ( deg ‘ 𝐹 ) = 0 ↔ ( deg ‘ ( ℂ × { 𝑥 } ) ) = 0 ) )
19 17 18 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝐹 = ( ℂ × { 𝑥 } ) → ( deg ‘ 𝐹 ) = 0 ) )
20 15 19 mtod ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ¬ 𝐹 = ( ℂ × { 𝑥 } ) )
21 vex ⊢ 𝑥 ∈ V
22 21 fconst2 ⊢ ( 𝐹 : ℂ ⟶ { 𝑥 } ↔ 𝐹 = ( ℂ × { 𝑥 } ) )
23 20 22 sylnibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ¬ 𝐹 : ℂ ⟶ { 𝑥 } )
24 4 ffnd ⊢ ( 𝜑 → 𝐹 Fn ℂ )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐹 Fn ℂ )
26 25 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℂ ( 𝐹 ‘ 𝑦 ) = 𝑥 ) → 𝐹 Fn ℂ )
27 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℂ ( 𝐹 ‘ 𝑦 ) = 𝑥 ) → ∀ 𝑦 ∈ ℂ ( 𝐹 ‘ 𝑦 ) = 𝑥 )
28 fconstfv ⊢ ( 𝐹 : ℂ ⟶ { 𝑥 } ↔ ( 𝐹 Fn ℂ ∧ ∀ 𝑦 ∈ ℂ ( 𝐹 ‘ 𝑦 ) = 𝑥 ) )
29 26 27 28 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℂ ( 𝐹 ‘ 𝑦 ) = 𝑥 ) → 𝐹 : ℂ ⟶ { 𝑥 } )
30 23 29 mtand ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ¬ ∀ 𝑦 ∈ ℂ ( 𝐹 ‘ 𝑦 ) = 𝑥 )
31 rexnal ⊢ ( ∃ 𝑦 ∈ ℂ ¬ ( 𝐹 ‘ 𝑦 ) = 𝑥 ↔ ¬ ∀ 𝑦 ∈ ℂ ( 𝐹 ‘ 𝑦 ) = 𝑥 )
32 30 31 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ∃ 𝑦 ∈ ℂ ¬ ( 𝐹 ‘ 𝑦 ) = 𝑥 )
33 cnex ⊢ ℂ ∈ V
34 33 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ℂ ∈ V )
35 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
36 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
37 34 35 25 36 ofc2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑦 ) − 𝑥 ) )
38 37 neeq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( ( ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ‘ 𝑦 ) ≠ 0 ↔ ( ( 𝐹 ‘ 𝑦 ) − 𝑥 ) ≠ 0 ) )
39 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
40 39 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
41 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → 𝑥 ∈ ℂ )
42 40 41 subeq0ad ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( ( ( 𝐹 ‘ 𝑦 ) − 𝑥 ) = 0 ↔ ( 𝐹 ‘ 𝑦 ) = 𝑥 ) )
43 42 necon3bid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( ( ( 𝐹 ‘ 𝑦 ) − 𝑥 ) ≠ 0 ↔ ( 𝐹 ‘ 𝑦 ) ≠ 𝑥 ) )
44 df-ne ⊢ ( ( 𝐹 ‘ 𝑦 ) ≠ 𝑥 ↔ ¬ ( 𝐹 ‘ 𝑦 ) = 𝑥 )
45 44 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( ( 𝐹 ‘ 𝑦 ) ≠ 𝑥 ↔ ¬ ( 𝐹 ‘ 𝑦 ) = 𝑥 ) )
46 38 43 45 3bitrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( ( ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ‘ 𝑦 ) ≠ 0 ↔ ¬ ( 𝐹 ‘ 𝑦 ) = 𝑥 ) )
47 46 rexbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ∃ 𝑦 ∈ ℂ ( ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ‘ 𝑦 ) ≠ 0 ↔ ∃ 𝑦 ∈ ℂ ¬ ( 𝐹 ‘ 𝑦 ) = 𝑥 ) )
48 32 47 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ∃ 𝑦 ∈ ℂ ( ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ‘ 𝑦 ) ≠ 0 )
49 ne0p ⊢ ( ( 𝑦 ∈ ℂ ∧ ( ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ‘ 𝑦 ) ≠ 0 ) → ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ≠ 0𝑝 )
50 49 rexlimiva ⊢ ( ∃ 𝑦 ∈ ℂ ( ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ‘ 𝑦 ) ≠ 0 → ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ≠ 0𝑝 )
51 48 50 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ≠ 0𝑝 )
52 eqid ⊢ ( ◡ ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) “ { 0 } ) = ( ◡ ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) “ { 0 } )
53 52 fta1 ⊢ ( ( ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ∈ ( Poly ‘ ℂ ) ∧ ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ≠ 0𝑝 ) → ( ( ◡ ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) “ { 0 } ) ) ≤ ( deg ‘ ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ) ) )
54 13 51 53 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ◡ ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) “ { 0 } ) ) ≤ ( deg ‘ ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ) ) )
55 54 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ◡ ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) “ { 0 } ) ∈ Fin )
56 55 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℂ ( ◡ ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) “ { 0 } ) ∈ Fin )
57 fnconstg ⊢ ( 𝑥 ∈ ℂ → ( ℂ × { 𝑥 } ) Fn ℂ )
58 57 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ℂ × { 𝑥 } ) Fn ℂ )
59 inidm ⊢ ( ℂ ∩ ℂ ) = ℂ
60 21 fvconst2 ⊢ ( 𝑦 ∈ ℂ → ( ( ℂ × { 𝑥 } ) ‘ 𝑦 ) = 𝑥 )
61 60 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( ( ℂ × { 𝑥 } ) ‘ 𝑦 ) = 𝑥 )
62 25 58 34 34 59 36 61 ofval ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑦 ) − 𝑥 ) )
63 62 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( ( ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ‘ 𝑦 ) = 0 ↔ ( ( 𝐹 ‘ 𝑦 ) − 𝑥 ) = 0 ) )
64 63 42 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( ( ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ‘ 𝑦 ) = 0 ↔ ( 𝐹 ‘ 𝑦 ) = 𝑥 ) )
65 64 pm5.32da ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝑦 ∈ ℂ ∧ ( ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ‘ 𝑦 ) = 0 ) ↔ ( 𝑦 ∈ ℂ ∧ ( 𝐹 ‘ 𝑦 ) = 𝑥 ) ) )
66 25 58 34 34 59 offn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) Fn ℂ )
67 fniniseg ⊢ ( ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) Fn ℂ → ( 𝑦 ∈ ( ◡ ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) “ { 0 } ) ↔ ( 𝑦 ∈ ℂ ∧ ( ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ‘ 𝑦 ) = 0 ) ) )
68 66 67 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑦 ∈ ( ◡ ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) “ { 0 } ) ↔ ( 𝑦 ∈ ℂ ∧ ( ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) ‘ 𝑦 ) = 0 ) ) )
69 fniniseg ⊢ ( 𝐹 Fn ℂ → ( 𝑦 ∈ ( ◡ 𝐹 “ { 𝑥 } ) ↔ ( 𝑦 ∈ ℂ ∧ ( 𝐹 ‘ 𝑦 ) = 𝑥 ) ) )
70 25 69 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑦 ∈ ( ◡ 𝐹 “ { 𝑥 } ) ↔ ( 𝑦 ∈ ℂ ∧ ( 𝐹 ‘ 𝑦 ) = 𝑥 ) ) )
71 65 68 70 3bitr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑦 ∈ ( ◡ ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) “ { 0 } ) ↔ 𝑦 ∈ ( ◡ 𝐹 “ { 𝑥 } ) ) )
72 71 eqrdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ◡ ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) “ { 0 } ) = ( ◡ 𝐹 “ { 𝑥 } ) )
73 72 eleq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ◡ ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) “ { 0 } ) ∈ Fin ↔ ( ◡ 𝐹 “ { 𝑥 } ) ∈ Fin ) )
74 73 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℂ ( ◡ ( 𝐹 ∘f − ( ℂ × { 𝑥 } ) ) “ { 0 } ) ∈ Fin ↔ ∀ 𝑥 ∈ ℂ ( ◡ 𝐹 “ { 𝑥 } ) ∈ Fin ) )
75 56 74 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℂ ( ◡ 𝐹 “ { 𝑥 } ) ∈ Fin )
76 ssralv ⊢ ( ran 𝐹 ⊆ ℂ → ( ∀ 𝑥 ∈ ℂ ( ◡ 𝐹 “ { 𝑥 } ) ∈ Fin → ∀ 𝑥 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑥 } ) ∈ Fin ) )
77 5 75 76 sylc ⊢ ( 𝜑 → ∀ 𝑥 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑥 } ) ∈ Fin )
78 4 fdmd ⊢ ( 𝜑 → dom 𝐹 = ℂ )
79 nnnfi ⊢ ¬ ℕ ∈ Fin
80 nnsscn ⊢ ℕ ⊆ ℂ
81 ssfi ⊢ ( ( ℂ ∈ Fin ∧ ℕ ⊆ ℂ ) → ℕ ∈ Fin )
82 80 81 mpan2 ⊢ ( ℂ ∈ Fin → ℕ ∈ Fin )
83 79 82 mto ⊢ ¬ ℂ ∈ Fin
84 83 a1i ⊢ ( 𝜑 → ¬ ℂ ∈ Fin )
85 78 84 eqneltrd ⊢ ( 𝜑 → ¬ dom 𝐹 ∈ Fin )
86 85 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑥 } ) ∈ Fin ) → ¬ dom 𝐹 ∈ Fin )
87 4 ffund ⊢ ( 𝜑 → Fun 𝐹 )
88 iunpreima ⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ∪ 𝑥 ∈ ran 𝐹 { 𝑥 } ) = ∪ 𝑥 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑥 } ) )
89 87 88 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ ∪ 𝑥 ∈ ran 𝐹 { 𝑥 } ) = ∪ 𝑥 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑥 } ) )
90 iunid ⊢ ∪ 𝑥 ∈ ran 𝐹 { 𝑥 } = ran 𝐹
91 90 imaeq2i ⊢ ( ◡ 𝐹 “ ∪ 𝑥 ∈ ran 𝐹 { 𝑥 } ) = ( ◡ 𝐹 “ ran 𝐹 )
92 cnvimarndm ⊢ ( ◡ 𝐹 “ ran 𝐹 ) = dom 𝐹
93 91 92 eqtri ⊢ ( ◡ 𝐹 “ ∪ 𝑥 ∈ ran 𝐹 { 𝑥 } ) = dom 𝐹
94 89 93 eqtr3di ⊢ ( 𝜑 → ∪ 𝑥 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑥 } ) = dom 𝐹 )
95 94 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑥 } ) ∈ Fin ) ∧ ran 𝐹 ∈ Fin ) → ∪ 𝑥 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑥 } ) = dom 𝐹 )
96 simpr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑥 } ) ∈ Fin ) ∧ ran 𝐹 ∈ Fin ) → ran 𝐹 ∈ Fin )
97 simplr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑥 } ) ∈ Fin ) ∧ ran 𝐹 ∈ Fin ) → ∀ 𝑥 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑥 } ) ∈ Fin )
98 iunfi ⊢ ( ( ran 𝐹 ∈ Fin ∧ ∀ 𝑥 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑥 } ) ∈ Fin ) → ∪ 𝑥 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑥 } ) ∈ Fin )
99 96 97 98 syl2anc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑥 } ) ∈ Fin ) ∧ ran 𝐹 ∈ Fin ) → ∪ 𝑥 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑥 } ) ∈ Fin )
100 95 99 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑥 } ) ∈ Fin ) ∧ ran 𝐹 ∈ Fin ) → dom 𝐹 ∈ Fin )
101 86 100 mtand ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑥 } ) ∈ Fin ) → ¬ ran 𝐹 ∈ Fin )
102 77 101 mpdan ⊢ ( 𝜑 → ¬ ran 𝐹 ∈ Fin )