Metamath Proof Explorer


Theorem mdegle0

Description: A polynomial has nonpositive degree iff it is a constant. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses mdegaddle.y 𝑌 = ( 𝐼 mPoly 𝑅 )
mdegaddle.d 𝐷 = ( 𝐼 mDeg 𝑅 )
mdegaddle.i ( 𝜑𝐼𝑉 )
mdegaddle.r ( 𝜑𝑅 ∈ Ring )
mdegle0.b 𝐵 = ( Base ‘ 𝑌 )
mdegle0.a 𝐴 = ( algSc ‘ 𝑌 )
mdegle0.f ( 𝜑𝐹𝐵 )
Assertion mdegle0 ( 𝜑 → ( ( 𝐷𝐹 ) ≤ 0 ↔ 𝐹 = ( 𝐴 ‘ ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mdegaddle.y 𝑌 = ( 𝐼 mPoly 𝑅 )
2 mdegaddle.d 𝐷 = ( 𝐼 mDeg 𝑅 )
3 mdegaddle.i ( 𝜑𝐼𝑉 )
4 mdegaddle.r ( 𝜑𝑅 ∈ Ring )
5 mdegle0.b 𝐵 = ( Base ‘ 𝑌 )
6 mdegle0.a 𝐴 = ( algSc ‘ 𝑌 )
7 mdegle0.f ( 𝜑𝐹𝐵 )
8 0xr 0 ∈ ℝ*
9 eqid ( 0g𝑅 ) = ( 0g𝑅 )
10 eqid { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } = { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin }
11 eqid ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) = ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) )
12 2 1 5 9 10 11 mdegleb ( ( 𝐹𝐵 ∧ 0 ∈ ℝ* ) → ( ( 𝐷𝐹 ) ≤ 0 ↔ ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ( 0 < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) → ( 𝐹𝑥 ) = ( 0g𝑅 ) ) ) )
13 7 8 12 sylancl ( 𝜑 → ( ( 𝐷𝐹 ) ≤ 0 ↔ ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ( 0 < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) → ( 𝐹𝑥 ) = ( 0g𝑅 ) ) ) )
14 10 11 tdeglem1 ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) : { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ⟶ ℕ0
15 14 a1i ( 𝜑 → ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) : { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ⟶ ℕ0 )
16 15 ffvelrnda ( ( 𝜑𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ∈ ℕ0 )
17 nn0re ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ∈ ℕ0 → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ∈ ℝ )
18 nn0ge0 ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ∈ ℕ0 → 0 ≤ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) )
19 17 18 jca ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ∈ ℕ0 → ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ) )
20 ne0gt0 ( ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ) → ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ≠ 0 ↔ 0 < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ) )
21 16 19 20 3syl ( ( 𝜑𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ) → ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ≠ 0 ↔ 0 < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ) )
22 10 11 tdeglem4 ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } → ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 𝐼 × { 0 } ) ) )
23 22 adantl ( ( 𝜑𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ) → ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 𝐼 × { 0 } ) ) )
24 23 necon3abid ( ( 𝜑𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ) → ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ≠ 0 ↔ ¬ 𝑥 = ( 𝐼 × { 0 } ) ) )
25 21 24 bitr3d ( ( 𝜑𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ) → ( 0 < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ↔ ¬ 𝑥 = ( 𝐼 × { 0 } ) ) )
26 25 imbi1d ( ( 𝜑𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 0 < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) → ( 𝐹𝑥 ) = ( 0g𝑅 ) ) ↔ ( ¬ 𝑥 = ( 𝐼 × { 0 } ) → ( 𝐹𝑥 ) = ( 0g𝑅 ) ) ) )
27 eqeq2 ( ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g𝑅 ) ) → ( ( 𝐹𝑥 ) = ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) ↔ ( 𝐹𝑥 ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g𝑅 ) ) ) )
28 27 bibi1d ( ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g𝑅 ) ) → ( ( ( 𝐹𝑥 ) = ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) ↔ ( ¬ 𝑥 = ( 𝐼 × { 0 } ) → ( 𝐹𝑥 ) = ( 0g𝑅 ) ) ) ↔ ( ( 𝐹𝑥 ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g𝑅 ) ) ↔ ( ¬ 𝑥 = ( 𝐼 × { 0 } ) → ( 𝐹𝑥 ) = ( 0g𝑅 ) ) ) ) )
29 eqeq2 ( ( 0g𝑅 ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g𝑅 ) ) → ( ( 𝐹𝑥 ) = ( 0g𝑅 ) ↔ ( 𝐹𝑥 ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g𝑅 ) ) ) )
30 29 bibi1d ( ( 0g𝑅 ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g𝑅 ) ) → ( ( ( 𝐹𝑥 ) = ( 0g𝑅 ) ↔ ( ¬ 𝑥 = ( 𝐼 × { 0 } ) → ( 𝐹𝑥 ) = ( 0g𝑅 ) ) ) ↔ ( ( 𝐹𝑥 ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g𝑅 ) ) ↔ ( ¬ 𝑥 = ( 𝐼 × { 0 } ) → ( 𝐹𝑥 ) = ( 0g𝑅 ) ) ) ) )
31 fveq2 ( 𝑥 = ( 𝐼 × { 0 } ) → ( 𝐹𝑥 ) = ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) )
32 pm2.24 ( 𝑥 = ( 𝐼 × { 0 } ) → ( ¬ 𝑥 = ( 𝐼 × { 0 } ) → ( 𝐹𝑥 ) = ( 0g𝑅 ) ) )
33 31 32 2thd ( 𝑥 = ( 𝐼 × { 0 } ) → ( ( 𝐹𝑥 ) = ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) ↔ ( ¬ 𝑥 = ( 𝐼 × { 0 } ) → ( 𝐹𝑥 ) = ( 0g𝑅 ) ) ) )
34 33 adantl ( ( 𝜑𝑥 = ( 𝐼 × { 0 } ) ) → ( ( 𝐹𝑥 ) = ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) ↔ ( ¬ 𝑥 = ( 𝐼 × { 0 } ) → ( 𝐹𝑥 ) = ( 0g𝑅 ) ) ) )
35 biimt ( ¬ 𝑥 = ( 𝐼 × { 0 } ) → ( ( 𝐹𝑥 ) = ( 0g𝑅 ) ↔ ( ¬ 𝑥 = ( 𝐼 × { 0 } ) → ( 𝐹𝑥 ) = ( 0g𝑅 ) ) ) )
36 35 adantl ( ( 𝜑 ∧ ¬ 𝑥 = ( 𝐼 × { 0 } ) ) → ( ( 𝐹𝑥 ) = ( 0g𝑅 ) ↔ ( ¬ 𝑥 = ( 𝐼 × { 0 } ) → ( 𝐹𝑥 ) = ( 0g𝑅 ) ) ) )
37 28 30 34 36 ifbothda ( 𝜑 → ( ( 𝐹𝑥 ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g𝑅 ) ) ↔ ( ¬ 𝑥 = ( 𝐼 × { 0 } ) → ( 𝐹𝑥 ) = ( 0g𝑅 ) ) ) )
38 37 adantr ( ( 𝜑𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 𝐹𝑥 ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g𝑅 ) ) ↔ ( ¬ 𝑥 = ( 𝐼 × { 0 } ) → ( 𝐹𝑥 ) = ( 0g𝑅 ) ) ) )
39 26 38 bitr4d ( ( 𝜑𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 0 < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) → ( 𝐹𝑥 ) = ( 0g𝑅 ) ) ↔ ( 𝐹𝑥 ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g𝑅 ) ) ) )
40 39 ralbidva ( 𝜑 → ( ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ( 0 < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) → ( 𝐹𝑥 ) = ( 0g𝑅 ) ) ↔ ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ( 𝐹𝑥 ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g𝑅 ) ) ) )
41 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
42 1 41 5 10 7 mplelf ( 𝜑𝐹 : { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
43 42 feqmptd ( 𝜑𝐹 = ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( 𝐹𝑥 ) ) )
44 10 psrbag0 ( 𝐼𝑉 → ( 𝐼 × { 0 } ) ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } )
45 3 44 syl ( 𝜑 → ( 𝐼 × { 0 } ) ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } )
46 42 45 ffvelrnd ( 𝜑 → ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) ∈ ( Base ‘ 𝑅 ) )
47 1 10 9 41 6 3 4 46 mplascl ( 𝜑 → ( 𝐴 ‘ ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) ) = ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g𝑅 ) ) ) )
48 43 47 eqeq12d ( 𝜑 → ( 𝐹 = ( 𝐴 ‘ ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) ) ↔ ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( 𝐹𝑥 ) ) = ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g𝑅 ) ) ) ) )
49 fvex ( 𝐹𝑥 ) ∈ V
50 49 rgenw 𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ( 𝐹𝑥 ) ∈ V
51 mpteqb ( ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ( 𝐹𝑥 ) ∈ V → ( ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( 𝐹𝑥 ) ) = ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g𝑅 ) ) ) ↔ ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ( 𝐹𝑥 ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g𝑅 ) ) ) )
52 50 51 mp1i ( 𝜑 → ( ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( 𝐹𝑥 ) ) = ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g𝑅 ) ) ) ↔ ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ( 𝐹𝑥 ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g𝑅 ) ) ) )
53 48 52 bitrd ( 𝜑 → ( 𝐹 = ( 𝐴 ‘ ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) ) ↔ ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ( 𝐹𝑥 ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g𝑅 ) ) ) )
54 40 53 bitr4d ( 𝜑 → ( ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ( 0 < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) → ( 𝐹𝑥 ) = ( 0g𝑅 ) ) ↔ 𝐹 = ( 𝐴 ‘ ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) ) ) )
55 13 54 bitrd ( 𝜑 → ( ( 𝐷𝐹 ) ≤ 0 ↔ 𝐹 = ( 𝐴 ‘ ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) ) ) )