Metamath Proof Explorer

Theorem mdegmullem

Description: Lemma for mdegmulle2 . (Contributed by Stefan O'Rear, 26-Mar-2015)

Ref Expression
Hypotheses mdegaddle.y ⊢ 𝑌 = ( 𝐼 mPoly 𝑅 )
mdegaddle.d ⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
mdegaddle.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
mdegaddle.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mdegmulle2.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
mdegmulle2.t ⊢ · = ( .r ‘ 𝑌 )
mdegmulle2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
mdegmulle2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
mdegmulle2.j1 ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
mdegmulle2.k1 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
mdegmulle2.j2 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 𝐽 )
mdegmulle2.k2 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ≤ 𝐾 )
mdegmullem.a ⊢ 𝐴 = { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin }
mdegmullem.h ⊢ 𝐻 = ( 𝑏 ∈ 𝐴 ↦ ( ℂfld Σg 𝑏 ) )
Assertion mdegmullem ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( 𝐽 + 𝐾 ) )

Proof

Step Hyp Ref Expression
1 mdegaddle.y ⊢ 𝑌 = ( 𝐼 mPoly 𝑅 )
2 mdegaddle.d ⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
3 mdegaddle.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4 mdegaddle.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 mdegmulle2.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
6 mdegmulle2.t ⊢ · = ( .r ‘ 𝑌 )
7 mdegmulle2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
8 mdegmulle2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
9 mdegmulle2.j1 ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
10 mdegmulle2.k1 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
11 mdegmulle2.j2 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 𝐽 )
12 mdegmulle2.k2 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ≤ 𝐾 )
13 mdegmullem.a ⊢ 𝐴 = { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin }
14 mdegmullem.h ⊢ 𝐻 = ( 𝑏 ∈ 𝐴 ↦ ( ℂfld Σg 𝑏 ) )
15 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
16 1 5 15 6 13 7 8 mplmul ⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) = ( 𝑐 ∈ 𝐴 ↦ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑐 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑐 ∘f − 𝑑 ) ) ) ) ) ) )
17 16 fveq1d ⊢ ( 𝜑 → ( ( 𝐹 · 𝐺 ) ‘ 𝑥 ) = ( ( 𝑐 ∈ 𝐴 ↦ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑐 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑐 ∘f − 𝑑 ) ) ) ) ) ) ‘ 𝑥 ) )
18 17 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) → ( ( 𝐹 · 𝐺 ) ‘ 𝑥 ) = ( ( 𝑐 ∈ 𝐴 ↦ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑐 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑐 ∘f − 𝑑 ) ) ) ) ) ) ‘ 𝑥 ) )
19 breq2 ⊢ ( 𝑐 = 𝑥 → ( 𝑒 ∘r ≤ 𝑐 ↔ 𝑒 ∘r ≤ 𝑥 ) )
20 19 rabbidv ⊢ ( 𝑐 = 𝑥 → { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑐 } = { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } )
21 fvoveq1 ⊢ ( 𝑐 = 𝑥 → ( 𝐺 ‘ ( 𝑐 ∘f − 𝑑 ) ) = ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) )
22 21 oveq2d ⊢ ( 𝑐 = 𝑥 → ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑐 ∘f − 𝑑 ) ) ) = ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) )
23 20 22 mpteq12dv ⊢ ( 𝑐 = 𝑥 → ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑐 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑐 ∘f − 𝑑 ) ) ) ) = ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ) )
24 23 oveq2d ⊢ ( 𝑐 = 𝑥 → ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑐 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑐 ∘f − 𝑑 ) ) ) ) ) = ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ) ) )
25 eqid ⊢ ( 𝑐 ∈ 𝐴 ↦ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑐 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑐 ∘f − 𝑑 ) ) ) ) ) ) = ( 𝑐 ∈ 𝐴 ↦ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑐 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑐 ∘f − 𝑑 ) ) ) ) ) )
26 ovex ⊢ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ) ) ∈ V
27 24 25 26 fvmpt ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑐 ∈ 𝐴 ↦ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑐 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑐 ∘f − 𝑑 ) ) ) ) ) ) ‘ 𝑥 ) = ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ) ) )
28 27 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) → ( ( 𝑐 ∈ 𝐴 ↦ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑐 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑐 ∘f − 𝑑 ) ) ) ) ) ) ‘ 𝑥 ) = ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ) ) )
29 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
30 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∧ 𝐽 < ( 𝐻 ‘ 𝑑 ) ) ) → 𝐹 ∈ 𝐵 )
31 elrabi ⊢ ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } → 𝑑 ∈ 𝐴 )
32 31 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → 𝑑 ∈ 𝐴 )
33 32 adantrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∧ 𝐽 < ( 𝐻 ‘ 𝑑 ) ) ) → 𝑑 ∈ 𝐴 )
34 2 1 5 mdegxrcl ⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )
35 7 34 syl ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )
36 35 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )
37 nn0ssre ⊢ ℕ0 ⊆ ℝ
38 ressxr ⊢ ℝ ⊆ ℝ*
39 37 38 sstri ⊢ ℕ0 ⊆ ℝ*
40 39 9 sselid ⊢ ( 𝜑 → 𝐽 ∈ ℝ* )
41 40 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → 𝐽 ∈ ℝ* )
42 13 14 tdeglem1 ⊢ 𝐻 : 𝐴 ⟶ ℕ0
43 42 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → 𝐻 : 𝐴 ⟶ ℕ0 )
44 43 32 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐻 ‘ 𝑑 ) ∈ ℕ0 )
45 39 44 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐻 ‘ 𝑑 ) ∈ ℝ* )
46 36 41 45 3jca ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ 𝐽 ∈ ℝ* ∧ ( 𝐻 ‘ 𝑑 ) ∈ ℝ* ) )
47 46 adantrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∧ 𝐽 < ( 𝐻 ‘ 𝑑 ) ) ) → ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ 𝐽 ∈ ℝ* ∧ ( 𝐻 ‘ 𝑑 ) ∈ ℝ* ) )
48 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐷 ‘ 𝐹 ) ≤ 𝐽 )
49 48 anim1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) ∧ 𝐽 < ( 𝐻 ‘ 𝑑 ) ) → ( ( 𝐷 ‘ 𝐹 ) ≤ 𝐽 ∧ 𝐽 < ( 𝐻 ‘ 𝑑 ) ) )
50 49 anasss ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∧ 𝐽 < ( 𝐻 ‘ 𝑑 ) ) ) → ( ( 𝐷 ‘ 𝐹 ) ≤ 𝐽 ∧ 𝐽 < ( 𝐻 ‘ 𝑑 ) ) )
51 xrlelttr ⊢ ( ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ 𝐽 ∈ ℝ* ∧ ( 𝐻 ‘ 𝑑 ) ∈ ℝ* ) → ( ( ( 𝐷 ‘ 𝐹 ) ≤ 𝐽 ∧ 𝐽 < ( 𝐻 ‘ 𝑑 ) ) → ( 𝐷 ‘ 𝐹 ) < ( 𝐻 ‘ 𝑑 ) ) )
52 47 50 51 sylc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∧ 𝐽 < ( 𝐻 ‘ 𝑑 ) ) ) → ( 𝐷 ‘ 𝐹 ) < ( 𝐻 ‘ 𝑑 ) )
53 2 1 5 29 13 14 30 33 52 mdeglt ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∧ 𝐽 < ( 𝐻 ‘ 𝑑 ) ) ) → ( 𝐹 ‘ 𝑑 ) = ( 0g ‘ 𝑅 ) )
54 53 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∧ 𝐽 < ( 𝐻 ‘ 𝑑 ) ) ) → ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) = ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) )
55 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → 𝑅 ∈ Ring )
56 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
57 1 56 5 13 8 mplelf ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ ( Base ‘ 𝑅 ) )
58 57 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → 𝐺 : 𝐴 ⟶ ( Base ‘ 𝑅 ) )
59 ssrab2 ⊢ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ⊆ 𝐴
60 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → 𝑥 ∈ 𝐴 )
61 eqid ⊢ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } = { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 }
62 13 61 psrbagconcl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝑥 ∘f − 𝑑 ) ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } )
63 60 62 sylancom ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝑥 ∘f − 𝑑 ) ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } )
64 59 63 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝑥 ∘f − 𝑑 ) ∈ 𝐴 )
65 58 64 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ∈ ( Base ‘ 𝑅 ) )
66 56 15 29 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) = ( 0g ‘ 𝑅 ) )
67 55 65 66 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) = ( 0g ‘ 𝑅 ) )
68 67 adantrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∧ 𝐽 < ( 𝐻 ‘ 𝑑 ) ) ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) = ( 0g ‘ 𝑅 ) )
69 54 68 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∧ 𝐽 < ( 𝐻 ‘ 𝑑 ) ) ) → ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) = ( 0g ‘ 𝑅 ) )
70 69 anassrs ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) ∧ 𝐽 < ( 𝐻 ‘ 𝑑 ) ) → ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) = ( 0g ‘ 𝑅 ) )
71 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∧ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ) → 𝐺 ∈ 𝐵 )
72 64 adantrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∧ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ) → ( 𝑥 ∘f − 𝑑 ) ∈ 𝐴 )
73 2 1 5 mdegxrcl ⊢ ( 𝐺 ∈ 𝐵 → ( 𝐷 ‘ 𝐺 ) ∈ ℝ* )
74 8 73 syl ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℝ* )
75 74 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐷 ‘ 𝐺 ) ∈ ℝ* )
76 39 10 sselid ⊢ ( 𝜑 → 𝐾 ∈ ℝ* )
77 76 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → 𝐾 ∈ ℝ* )
78 43 64 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ∈ ℕ0 )
79 39 78 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ∈ ℝ* )
80 75 77 79 3jca ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( ( 𝐷 ‘ 𝐺 ) ∈ ℝ* ∧ 𝐾 ∈ ℝ* ∧ ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ∈ ℝ* ) )
81 80 adantrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∧ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ) → ( ( 𝐷 ‘ 𝐺 ) ∈ ℝ* ∧ 𝐾 ∈ ℝ* ∧ ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ∈ ℝ* ) )
82 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐷 ‘ 𝐺 ) ≤ 𝐾 )
83 82 anim1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) ∧ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) → ( ( 𝐷 ‘ 𝐺 ) ≤ 𝐾 ∧ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) )
84 83 anasss ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∧ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ) → ( ( 𝐷 ‘ 𝐺 ) ≤ 𝐾 ∧ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) )
85 xrlelttr ⊢ ( ( ( 𝐷 ‘ 𝐺 ) ∈ ℝ* ∧ 𝐾 ∈ ℝ* ∧ ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ∈ ℝ* ) → ( ( ( 𝐷 ‘ 𝐺 ) ≤ 𝐾 ∧ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) → ( 𝐷 ‘ 𝐺 ) < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) )
86 81 84 85 sylc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∧ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ) → ( 𝐷 ‘ 𝐺 ) < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) )
87 2 1 5 29 13 14 71 72 86 mdeglt ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∧ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ) → ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) = ( 0g ‘ 𝑅 ) )
88 87 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∧ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ) → ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) = ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
89 1 56 5 13 7 mplelf ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( Base ‘ 𝑅 ) )
90 89 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → 𝐹 : 𝐴 ⟶ ( Base ‘ 𝑅 ) )
91 90 32 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐹 ‘ 𝑑 ) ∈ ( Base ‘ 𝑅 ) )
92 56 15 29 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ‘ 𝑑 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
93 55 91 92 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
94 93 adantrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∧ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ) → ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
95 88 94 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∧ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ) → ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) = ( 0g ‘ 𝑅 ) )
96 95 anassrs ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) ∧ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) → ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) = ( 0g ‘ 𝑅 ) )
97 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) )
98 44 nn0red ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐻 ‘ 𝑑 ) ∈ ℝ )
99 78 nn0red ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ∈ ℝ )
100 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → 𝐽 ∈ ℕ0 )
101 100 nn0red ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → 𝐽 ∈ ℝ )
102 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → 𝐾 ∈ ℕ0 )
103 102 nn0red ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → 𝐾 ∈ ℝ )
104 le2add ⊢ ( ( ( ( 𝐻 ‘ 𝑑 ) ∈ ℝ ∧ ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ∈ ℝ ) ∧ ( 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ) ) → ( ( ( 𝐻 ‘ 𝑑 ) ≤ 𝐽 ∧ ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ≤ 𝐾 ) → ( ( 𝐻 ‘ 𝑑 ) + ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ≤ ( 𝐽 + 𝐾 ) ) )
105 98 99 101 103 104 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( ( ( 𝐻 ‘ 𝑑 ) ≤ 𝐽 ∧ ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ≤ 𝐾 ) → ( ( 𝐻 ‘ 𝑑 ) + ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ≤ ( 𝐽 + 𝐾 ) ) )
106 13 14 tdeglem3 ⊢ ( ( 𝑑 ∈ 𝐴 ∧ ( 𝑥 ∘f − 𝑑 ) ∈ 𝐴 ) → ( 𝐻 ‘ ( 𝑑 ∘f + ( 𝑥 ∘f − 𝑑 ) ) ) = ( ( 𝐻 ‘ 𝑑 ) + ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) )
107 32 64 106 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐻 ‘ ( 𝑑 ∘f + ( 𝑥 ∘f − 𝑑 ) ) ) = ( ( 𝐻 ‘ 𝑑 ) + ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) )
108 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → 𝐼 ∈ 𝑉 )
109 13 psrbagf ⊢ ( 𝑑 ∈ 𝐴 → 𝑑 : 𝐼 ⟶ ℕ0 )
110 109 3ad2ant2 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑑 : 𝐼 ⟶ ℕ0 )
111 110 ffvelcdmda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑑 ‘ 𝑏 ) ∈ ℕ0 )
112 111 nn0cnd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑑 ‘ 𝑏 ) ∈ ℂ )
113 13 psrbagf ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 : 𝐼 ⟶ ℕ0 )
114 113 3ad2ant3 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 : 𝐼 ⟶ ℕ0 )
115 114 ffvelcdmda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑏 ) ∈ ℕ0 )
116 115 nn0cnd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑏 ) ∈ ℂ )
117 112 116 pncan3d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐼 ) → ( ( 𝑑 ‘ 𝑏 ) + ( ( 𝑥 ‘ 𝑏 ) − ( 𝑑 ‘ 𝑏 ) ) ) = ( 𝑥 ‘ 𝑏 ) )
118 117 mpteq2dva ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑏 ) + ( ( 𝑥 ‘ 𝑏 ) − ( 𝑑 ‘ 𝑏 ) ) ) ) = ( 𝑏 ∈ 𝐼 ↦ ( 𝑥 ‘ 𝑏 ) ) )
119 simp1 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝐼 ∈ 𝑉 )
120 fvexd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑑 ‘ 𝑏 ) ∈ V )
121 ovexd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑏 ) − ( 𝑑 ‘ 𝑏 ) ) ∈ V )
122 110 feqmptd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑑 = ( 𝑏 ∈ 𝐼 ↦ ( 𝑑 ‘ 𝑏 ) ) )
123 fvexd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑏 ) ∈ V )
124 114 feqmptd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 = ( 𝑏 ∈ 𝐼 ↦ ( 𝑥 ‘ 𝑏 ) ) )
125 119 123 120 124 122 offval2 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∘f − 𝑑 ) = ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑏 ) − ( 𝑑 ‘ 𝑏 ) ) ) )
126 119 120 121 122 125 offval2 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑑 ∘f + ( 𝑥 ∘f − 𝑑 ) ) = ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑏 ) + ( ( 𝑥 ‘ 𝑏 ) − ( 𝑑 ‘ 𝑏 ) ) ) ) )
127 118 126 124 3eqtr4d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑑 ∘f + ( 𝑥 ∘f − 𝑑 ) ) = 𝑥 )
128 108 32 60 127 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝑑 ∘f + ( 𝑥 ∘f − 𝑑 ) ) = 𝑥 )
129 128 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐻 ‘ ( 𝑑 ∘f + ( 𝑥 ∘f − 𝑑 ) ) ) = ( 𝐻 ‘ 𝑥 ) )
130 107 129 eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( ( 𝐻 ‘ 𝑑 ) + ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) = ( 𝐻 ‘ 𝑥 ) )
131 130 breq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( ( ( 𝐻 ‘ 𝑑 ) + ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ≤ ( 𝐽 + 𝐾 ) ↔ ( 𝐻 ‘ 𝑥 ) ≤ ( 𝐽 + 𝐾 ) ) )
132 105 131 sylibd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( ( ( 𝐻 ‘ 𝑑 ) ≤ 𝐽 ∧ ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ≤ 𝐾 ) → ( 𝐻 ‘ 𝑥 ) ≤ ( 𝐽 + 𝐾 ) ) )
133 98 101 lenltd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( ( 𝐻 ‘ 𝑑 ) ≤ 𝐽 ↔ ¬ 𝐽 < ( 𝐻 ‘ 𝑑 ) ) )
134 99 103 lenltd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ≤ 𝐾 ↔ ¬ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) )
135 133 134 anbi12d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( ( ( 𝐻 ‘ 𝑑 ) ≤ 𝐽 ∧ ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ≤ 𝐾 ) ↔ ( ¬ 𝐽 < ( 𝐻 ‘ 𝑑 ) ∧ ¬ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ) )
136 ioran ⊢ ( ¬ ( 𝐽 < ( 𝐻 ‘ 𝑑 ) ∨ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ↔ ( ¬ 𝐽 < ( 𝐻 ‘ 𝑑 ) ∧ ¬ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) )
137 135 136 bitr4di ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( ( ( 𝐻 ‘ 𝑑 ) ≤ 𝐽 ∧ ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ≤ 𝐾 ) ↔ ¬ ( 𝐽 < ( 𝐻 ‘ 𝑑 ) ∨ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ) )
138 43 60 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐻 ‘ 𝑥 ) ∈ ℕ0 )
139 138 nn0red ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐻 ‘ 𝑥 ) ∈ ℝ )
140 9 10 nn0addcld ⊢ ( 𝜑 → ( 𝐽 + 𝐾 ) ∈ ℕ0 )
141 140 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐽 + 𝐾 ) ∈ ℕ0 )
142 141 nn0red ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐽 + 𝐾 ) ∈ ℝ )
143 139 142 lenltd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( ( 𝐻 ‘ 𝑥 ) ≤ ( 𝐽 + 𝐾 ) ↔ ¬ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) )
144 132 137 143 3imtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( ¬ ( 𝐽 < ( 𝐻 ‘ 𝑑 ) ∨ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) → ¬ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) )
145 97 144 mt4d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( 𝐽 < ( 𝐻 ‘ 𝑑 ) ∨ 𝐾 < ( 𝐻 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) )
146 70 96 145 mpjaodan ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ) → ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) = ( 0g ‘ 𝑅 ) )
147 146 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ) = ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ↦ ( 0g ‘ 𝑅 ) ) )
148 147 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ) ) = ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ↦ ( 0g ‘ 𝑅 ) ) ) )
149 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
150 4 149 syl ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
151 150 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) → 𝑅 ∈ Mnd )
152 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
153 13 152 rab2ex ⊢ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∈ V
154 29 gsumz ⊢ ( ( 𝑅 ∈ Mnd ∧ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ∈ V ) → ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
155 151 153 154 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
156 148 155 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ 𝐴 ∣ 𝑒 ∘r ≤ 𝑥 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑥 ∘f − 𝑑 ) ) ) ) ) = ( 0g ‘ 𝑅 ) )
157 18 28 156 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) ) ) → ( ( 𝐹 · 𝐺 ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) )
158 157 expr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) → ( ( 𝐹 · 𝐺 ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) )
159 158 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) → ( ( 𝐹 · 𝐺 ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) )
160 1 3 4 mplringd ⊢ ( 𝜑 → 𝑌 ∈ Ring )
161 5 6 ringcl ⊢ ( ( 𝑌 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 · 𝐺 ) ∈ 𝐵 )
162 160 7 8 161 syl3anc ⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) ∈ 𝐵 )
163 39 140 sselid ⊢ ( 𝜑 → ( 𝐽 + 𝐾 ) ∈ ℝ* )
164 2 1 5 29 13 14 mdegleb ⊢ ( ( ( 𝐹 · 𝐺 ) ∈ 𝐵 ∧ ( 𝐽 + 𝐾 ) ∈ ℝ* ) → ( ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( 𝐽 + 𝐾 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) → ( ( 𝐹 · 𝐺 ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) )
165 162 163 164 syl2anc ⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( 𝐽 + 𝐾 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐽 + 𝐾 ) < ( 𝐻 ‘ 𝑥 ) → ( ( 𝐹 · 𝐺 ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) )
166 159 165 mpbird ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( 𝐽 + 𝐾 ) )