Metamath Proof Explorer

Theorem mdegmullem

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

Ref Expression
Hypotheses mdegaddle.y ⊢ Y = I mPoly R
mdegaddle.d ⊢ D = I mDeg R
mdegaddle.i ⊢ φ → I ∈ V
mdegaddle.r ⊢ φ → R ∈ Ring
mdegmulle2.b ⊢ B = Base Y
mdegmulle2.t ⊢ · ˙ = ⋅ Y
mdegmulle2.f ⊢ φ → F ∈ B
mdegmulle2.g ⊢ φ → G ∈ B
mdegmulle2.j1 ⊢ φ → J ∈ ℕ 0
mdegmulle2.k1 ⊢ φ → K ∈ ℕ 0
mdegmulle2.j2 ⊢ φ → D ⁡ F ≤ J
mdegmulle2.k2 ⊢ φ → D ⁡ G ≤ K
mdegmullem.a ⊢ A = a ∈ ℕ 0 I | a -1 ℕ ∈ Fin
mdegmullem.h ⊢ H = b ∈ A ⟼ ∑ ℂ fld b
Assertion mdegmullem ⊢ φ → D ⁡ F · ˙ G ≤ J + K

Proof

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