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 ⊢ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } = { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin }
11 eqid ⊢ ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) = ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) )
12 2 1 5 9 10 11 mdegleb ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 0 ∈ ℝ* ) → ( ( 𝐷 ‘ 𝐹 ) ≤ 0 ↔ ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ( 0 < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) )
13 7 8 12 sylancl ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) ≤ 0 ↔ ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ( 0 < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) )
14 10 11 tdeglem1 ⊢ ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) : { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ℕ0
15 14 a1i ⊢ ( 𝜑 → ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) : { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ℕ0 )
16 15 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ∈ ℕ0 )
17 nn0re ⊢ ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ∈ ℕ0 → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ∈ ℝ )
18 nn0ge0 ⊢ ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ∈ ℕ0 → 0 ≤ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) )
19 17 18 jca ⊢ ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ∈ ℕ0 → ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ) )
20 ne0gt0 ⊢ ( ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ) → ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ≠ 0 ↔ 0 < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ) )
21 16 19 20 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ≠ 0 ↔ 0 < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ) )
22 10 11 tdeglem4 ⊢ ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } → ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 𝐼 × { 0 } ) ) )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 𝐼 × { 0 } ) ) )
24 23 necon3abid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ≠ 0 ↔ ¬ 𝑥 = ( 𝐼 × { 0 } ) ) )
25 21 24 bitr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 0 < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ↔ ¬ 𝑥 = ( 𝐼 × { 0 } ) ) )
26 25 imbi1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 0 < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ 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 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g ‘ 𝑅 ) ) ↔ ( ¬ 𝑥 = ( 𝐼 × { 0 } ) → ( 𝐹 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) )
39 26 38 bitr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 0 < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ↔ ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g ‘ 𝑅 ) ) ) )
40 39 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ( 0 < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ↔ ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g ‘ 𝑅 ) ) ) )
41 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
42 1 41 5 10 7 mplelf ⊢ ( 𝜑 → 𝐹 : { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
43 42 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( 𝐹 ‘ 𝑥 ) ) )
44 10 psrbag0 ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 × { 0 } ) ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } )
45 3 44 syl ⊢ ( 𝜑 → ( 𝐼 × { 0 } ) ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } )
46 42 45 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) ∈ ( Base ‘ 𝑅 ) )
47 1 10 9 41 6 3 4 46 mplascl ⊢ ( 𝜑 → ( 𝐴 ‘ ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) ) = ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g ‘ 𝑅 ) ) ) )
48 43 47 eqeq12d ⊢ ( 𝜑 → ( 𝐹 = ( 𝐴 ‘ ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) ) ↔ ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g ‘ 𝑅 ) ) ) ) )
49 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
50 49 rgenw ⊢ ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ( 𝐹 ‘ 𝑥 ) ∈ V
51 mpteqb ⊢ ( ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ( 𝐹 ‘ 𝑥 ) ∈ V → ( ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g ‘ 𝑅 ) ) ) ↔ ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g ‘ 𝑅 ) ) ) )
52 50 51 mp1i ⊢ ( 𝜑 → ( ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g ‘ 𝑅 ) ) ) ↔ ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g ‘ 𝑅 ) ) ) )
53 48 52 bitrd ⊢ ( 𝜑 → ( 𝐹 = ( 𝐴 ‘ ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) ) ↔ ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) , ( 0g ‘ 𝑅 ) ) ) )
54 40 53 bitr4d ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ( 0 < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ↔ 𝐹 = ( 𝐴 ‘ ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) ) ) )
55 13 54 bitrd ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) ≤ 0 ↔ 𝐹 = ( 𝐴 ‘ ( 𝐹 ‘ ( 𝐼 × { 0 } ) ) ) ) )