Metamath Proof Explorer

Theorem mhpmulcl

Description: A product of homogeneous polynomials is a homogeneous polynomial whose degree is the sum of the degrees of the factors. Compare mdegmulle2 (which shows less-than-or-equal instead of equal). (Contributed by SN, 22-Jul-2024) Remove closure hypotheses. (Revised by SN, 4-Sep-2025)

Ref Expression
Hypotheses mhpmulcl.h ⊢ H = I mHomP R
mhpmulcl.y ⊢ Y = I mPoly R
mhpmulcl.t ⊢ · ˙ = ⋅ Y
mhpmulcl.r ⊢ φ → R ∈ Ring
mhpmulcl.p ⊢ φ → P ∈ H ⁡ M
mhpmulcl.q ⊢ φ → Q ∈ H ⁡ N
Assertion mhpmulcl ⊢ φ → P · ˙ Q ∈ H ⁡ M + N

Proof

Step Hyp Ref Expression
1 mhpmulcl.h ⊢ H = I mHomP R
2 mhpmulcl.y ⊢ Y = I mPoly R
3 mhpmulcl.t ⊢ · ˙ = ⋅ Y
4 mhpmulcl.r ⊢ φ → R ∈ Ring
5 mhpmulcl.p ⊢ φ → P ∈ H ⁡ M
6 mhpmulcl.q ⊢ φ → Q ∈ H ⁡ N
7 breq2 ⊢ d = x → c ≤ f d ↔ c ≤ f x
8 7 rabbidv ⊢ d = x → c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f d = c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x
9 fvoveq1 ⊢ d = x → Q ⁡ d − f e = Q ⁡ x − f e
10 9 oveq2d ⊢ d = x → P ⁡ e ⋅ R Q ⁡ d − f e = P ⁡ e ⋅ R Q ⁡ x − f e
11 8 10 mpteq12dv ⊢ d = x → e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f d ⟼ P ⁡ e ⋅ R Q ⁡ d − f e = e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ⟼ P ⁡ e ⋅ R Q ⁡ x − f e
12 11 oveq2d ⊢ d = x → ∑ R e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f d P ⁡ e ⋅ R Q ⁡ d − f e = ∑ R e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x P ⁡ e ⋅ R Q ⁡ x − f e
13 eqid ⊢ Base Y = Base Y
14 eqid ⊢ ⋅ R = ⋅ R
15 eqid ⊢ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
16 1 2 13 5 mhpmpl ⊢ φ → P ∈ Base Y
17 1 2 13 6 mhpmpl ⊢ φ → Q ∈ Base Y
18 2 13 14 3 15 16 17 mplmul ⊢ φ → P · ˙ Q = d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ ∑ R e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f d P ⁡ e ⋅ R Q ⁡ d − f e
19 18 adantr ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → P · ˙ Q = d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ ∑ R e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f d P ⁡ e ⋅ R Q ⁡ d − f e
20 simpr ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
21 ovexd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → ∑ R e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x P ⁡ e ⋅ R Q ⁡ x − f e ∈ V
22 12 19 20 21 fvmptd4 ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → P · ˙ Q ⁡ x = ∑ R e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x P ⁡ e ⋅ R Q ⁡ x − f e
23 22 neeq1d ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → P · ˙ Q ⁡ x ≠ 0 R ↔ ∑ R e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x P ⁡ e ⋅ R Q ⁡ x − f e ≠ 0 R
24 simp-4l ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 e ≠ M → φ
25 oveq2 ⊢ c = e → ∑ ℂ fld ↾ 𝑠 ℕ 0 c = ∑ ℂ fld ↾ 𝑠 ℕ 0 e
26 25 eqeq1d ⊢ c = e → ∑ ℂ fld ↾ 𝑠 ℕ 0 c = M ↔ ∑ ℂ fld ↾ 𝑠 ℕ 0 e = M
27 26 necon3bbid ⊢ c = e → ¬ ∑ ℂ fld ↾ 𝑠 ℕ 0 c = M ↔ ∑ ℂ fld ↾ 𝑠 ℕ 0 e ≠ M
28 elrabi ⊢ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → e ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
29 28 ad2antlr ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 e ≠ M → e ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
30 simpr ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 e ≠ M → ∑ ℂ fld ↾ 𝑠 ℕ 0 e ≠ M
31 27 29 30 elrabd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 e ≠ M → e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | ¬ ∑ ℂ fld ↾ 𝑠 ℕ 0 c = M
32 notrab ⊢ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∖ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | ∑ ℂ fld ↾ 𝑠 ℕ 0 c = M = c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | ¬ ∑ ℂ fld ↾ 𝑠 ℕ 0 c = M
33 31 32 eleqtrrdi ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 e ≠ M → e ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∖ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | ∑ ℂ fld ↾ 𝑠 ℕ 0 c = M
34 eqid ⊢ Base R = Base R
35 2 34 13 15 16 mplelf ⊢ φ → P : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ Base R
36 eqid ⊢ 0 R = 0 R
37 1 36 15 5 mhpdeg ⊢ φ → P supp 0 R ⊆ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | ∑ ℂ fld ↾ 𝑠 ℕ 0 c = M
38 fvexd ⊢ φ → 0 R ∈ V
39 35 37 5 38 suppssrg ⊢ φ ∧ e ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∖ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | ∑ ℂ fld ↾ 𝑠 ℕ 0 c = M → P ⁡ e = 0 R
40 24 33 39 syl2anc ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 e ≠ M → P ⁡ e = 0 R
41 40 oveq1d ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 e ≠ M → P ⁡ e ⋅ R Q ⁡ x − f e = 0 R ⋅ R Q ⁡ x − f e
42 4 ad4antr ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 e ≠ M → R ∈ Ring
43 17 ad4antr ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 e ≠ M → Q ∈ Base Y
44 2 34 13 15 43 mplelf ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 e ≠ M → Q : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ Base R
45 eqid ⊢ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x = c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x
46 15 45 psrbagconcl ⊢ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → x − f e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x
47 46 ad5ant24 ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 e ≠ M → x − f e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x
48 elrabi ⊢ x − f e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → x − f e ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
49 47 48 syl ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 e ≠ M → x − f e ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
50 44 49 ffvelcdmd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 e ≠ M → Q ⁡ x − f e ∈ Base R
51 34 14 36 42 50 ringlzd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 e ≠ M → 0 R ⋅ R Q ⁡ x − f e = 0 R
52 41 51 eqtrd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 e ≠ M → P ⁡ e ⋅ R Q ⁡ x − f e = 0 R
53 simp-4l ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ N → φ
54 oveq2 ⊢ c = x − f e → ∑ ℂ fld ↾ 𝑠 ℕ 0 c = ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e
55 54 eqeq1d ⊢ c = x − f e → ∑ ℂ fld ↾ 𝑠 ℕ 0 c = N ↔ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e = N
56 55 necon3bbid ⊢ c = x − f e → ¬ ∑ ℂ fld ↾ 𝑠 ℕ 0 c = N ↔ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ N
57 46 ad5ant24 ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ N → x − f e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x
58 57 48 syl ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ N → x − f e ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
59 simpr ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ N → ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ N
60 56 58 59 elrabd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ N → x − f e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | ¬ ∑ ℂ fld ↾ 𝑠 ℕ 0 c = N
61 notrab ⊢ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∖ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | ∑ ℂ fld ↾ 𝑠 ℕ 0 c = N = c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | ¬ ∑ ℂ fld ↾ 𝑠 ℕ 0 c = N
62 60 61 eleqtrrdi ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ N → x − f e ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∖ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | ∑ ℂ fld ↾ 𝑠 ℕ 0 c = N
63 2 34 13 15 17 mplelf ⊢ φ → Q : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ Base R
64 1 36 15 6 mhpdeg ⊢ φ → Q supp 0 R ⊆ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | ∑ ℂ fld ↾ 𝑠 ℕ 0 c = N
65 63 64 6 38 suppssrg ⊢ φ ∧ x − f e ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∖ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | ∑ ℂ fld ↾ 𝑠 ℕ 0 c = N → Q ⁡ x − f e = 0 R
66 53 62 65 syl2anc ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ N → Q ⁡ x − f e = 0 R
67 66 oveq2d ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ N → P ⁡ e ⋅ R Q ⁡ x − f e = P ⁡ e ⋅ R 0 R
68 4 ad4antr ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ N → R ∈ Ring
69 16 ad4antr ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ N → P ∈ Base Y
70 2 34 13 15 69 mplelf ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ N → P : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ Base R
71 28 ad2antlr ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ N → e ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
72 70 71 ffvelcdmd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ N → P ⁡ e ∈ Base R
73 34 14 36 68 72 ringrzd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ N → P ⁡ e ⋅ R 0 R = 0 R
74 67 73 eqtrd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ N → P ⁡ e ⋅ R Q ⁡ x − f e = 0 R
75 nn0subm ⊢ ℕ 0 ∈ SubMnd ⁡ ℂ fld
76 eqid ⊢ ℂ fld ↾ 𝑠 ℕ 0 = ℂ fld ↾ 𝑠 ℕ 0
77 76 submbas ⊢ ℕ 0 ∈ SubMnd ⁡ ℂ fld → ℕ 0 = Base ℂ fld ↾ 𝑠 ℕ 0
78 75 77 ax-mp ⊢ ℕ 0 = Base ℂ fld ↾ 𝑠 ℕ 0
79 cnfld0 ⊢ 0 = 0 ℂ fld
80 76 79 subm0 ⊢ ℕ 0 ∈ SubMnd ⁡ ℂ fld → 0 = 0 ℂ fld ↾ 𝑠 ℕ 0
81 75 80 ax-mp ⊢ 0 = 0 ℂ fld ↾ 𝑠 ℕ 0
82 nn0ex ⊢ ℕ 0 ∈ V
83 cnfldadd ⊢ + = + ℂ fld
84 76 83 ressplusg ⊢ ℕ 0 ∈ V → + = + ℂ fld ↾ 𝑠 ℕ 0
85 82 84 ax-mp ⊢ + = + ℂ fld ↾ 𝑠 ℕ 0
86 cnring ⊢ ℂ fld ∈ Ring
87 ringcmn ⊢ ℂ fld ∈ Ring → ℂ fld ∈ CMnd
88 86 87 ax-mp ⊢ ℂ fld ∈ CMnd
89 76 submcmn ⊢ ℂ fld ∈ CMnd ∧ ℕ 0 ∈ SubMnd ⁡ ℂ fld → ℂ fld ↾ 𝑠 ℕ 0 ∈ CMnd
90 88 75 89 mp2an ⊢ ℂ fld ↾ 𝑠 ℕ 0 ∈ CMnd
91 90 a1i ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → ℂ fld ↾ 𝑠 ℕ 0 ∈ CMnd
92 reldmmhp ⊢ Rel ⁡ dom ⁡ mHomP
93 92 1 5 elfvov1 ⊢ φ → I ∈ V
94 93 ad3antrrr ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → I ∈ V
95 28 adantl ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → e ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
96 15 psrbagf ⊢ e ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → e : I ⟶ ℕ 0
97 95 96 syl ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → e : I ⟶ ℕ 0
98 15 psrbagf ⊢ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → x : I ⟶ ℕ 0
99 98 ad3antlr ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → x : I ⟶ ℕ 0
100 99 ffnd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → x Fn I
101 97 ffnd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → e Fn I
102 inidm ⊢ I ∩ I = I
103 eqidd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ i ∈ I → x ⁡ i = x ⁡ i
104 eqidd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ i ∈ I → e ⁡ i = e ⁡ i
105 100 101 94 94 102 103 104 offval ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → x − f e = i ∈ I ⟼ x ⁡ i − e ⁡ i
106 simpl ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ i ∈ I → φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x
107 breq1 ⊢ c = e → c ≤ f x ↔ e ≤ f x
108 107 elrab ⊢ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ↔ e ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ e ≤ f x
109 108 simprbi ⊢ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → e ≤ f x
110 109 ad2antlr ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ i ∈ I → e ≤ f x
111 simpr ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ i ∈ I → i ∈ I
112 101 100 94 94 102 104 103 ofrval ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ e ≤ f x ∧ i ∈ I → e ⁡ i ≤ x ⁡ i
113 106 110 111 112 syl3anc ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ i ∈ I → e ⁡ i ≤ x ⁡ i
114 97 ffvelcdmda ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ i ∈ I → e ⁡ i ∈ ℕ 0
115 99 ffvelcdmda ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ i ∈ I → x ⁡ i ∈ ℕ 0
116 nn0sub ⊢ e ⁡ i ∈ ℕ 0 ∧ x ⁡ i ∈ ℕ 0 → e ⁡ i ≤ x ⁡ i ↔ x ⁡ i − e ⁡ i ∈ ℕ 0
117 114 115 116 syl2anc ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ i ∈ I → e ⁡ i ≤ x ⁡ i ↔ x ⁡ i − e ⁡ i ∈ ℕ 0
118 113 117 mpbid ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ i ∈ I → x ⁡ i − e ⁡ i ∈ ℕ 0
119 105 118 fmpt3d ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → x − f e : I ⟶ ℕ 0
120 97 ffund ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → Fun ⁡ e
121 c0ex ⊢ 0 ∈ V
122 94 121 jctir ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → I ∈ V ∧ 0 ∈ V
123 fsuppeq ⊢ I ∈ V ∧ 0 ∈ V → e : I ⟶ ℕ 0 → e supp 0 = e -1 ℕ 0 ∖ 0
124 122 97 123 sylc ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → e supp 0 = e -1 ℕ 0 ∖ 0
125 dfn2 ⊢ ℕ = ℕ 0 ∖ 0
126 125 imaeq2i ⊢ e -1 ℕ = e -1 ℕ 0 ∖ 0
127 124 126 eqtr4di ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → e supp 0 = e -1 ℕ
128 15 psrbag ⊢ I ∈ V → e ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ↔ e : I ⟶ ℕ 0 ∧ e -1 ℕ ∈ Fin
129 94 128 syl ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → e ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ↔ e : I ⟶ ℕ 0 ∧ e -1 ℕ ∈ Fin
130 95 129 mpbid ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → e : I ⟶ ℕ 0 ∧ e -1 ℕ ∈ Fin
131 130 simprd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → e -1 ℕ ∈ Fin
132 127 131 eqeltrd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → e supp 0 ∈ Fin
133 95 elexd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → e ∈ V
134 isfsupp ⊢ e ∈ V ∧ 0 ∈ V → finSupp 0 ⁡ e ↔ Fun ⁡ e ∧ e supp 0 ∈ Fin
135 133 121 134 sylancl ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → finSupp 0 ⁡ e ↔ Fun ⁡ e ∧ e supp 0 ∈ Fin
136 120 132 135 mpbir2and ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → finSupp 0 ⁡ e
137 ovexd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → x − f e ∈ V
138 0nn0 ⊢ 0 ∈ ℕ 0
139 138 a1i ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → 0 ∈ ℕ 0
140 100 101 94 94 offun ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → Fun ⁡ x − f e
141 15 psrbagfsupp ⊢ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → finSupp 0 ⁡ x
142 141 ad3antlr ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → finSupp 0 ⁡ x
143 142 136 fsuppunfi ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → supp 0 ⁡ x ∪ supp 0 ⁡ e ∈ Fin
144 0m0e0 ⊢ 0 − 0 = 0
145 144 a1i ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → 0 − 0 = 0
146 94 139 99 97 145 suppofssd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → x − f e supp 0 ⊆ supp 0 ⁡ x ∪ supp 0 ⁡ e
147 143 146 ssfid ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → x − f e supp 0 ∈ Fin
148 137 139 140 147 isfsuppd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → finSupp 0 ⁡ x − f e
149 78 81 85 91 94 97 119 136 148 gsumadd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → ∑ ℂ fld ↾ 𝑠 ℕ 0 e + f x − f e = ∑ ℂ fld ↾ 𝑠 ℕ 0 e + ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e
150 97 ffvelcdmda ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ b ∈ I → e ⁡ b ∈ ℕ 0
151 150 nn0cnd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ b ∈ I → e ⁡ b ∈ ℂ
152 99 ffvelcdmda ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ b ∈ I → x ⁡ b ∈ ℕ 0
153 152 nn0cnd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ b ∈ I → x ⁡ b ∈ ℂ
154 151 153 pncan3d ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ b ∈ I → e ⁡ b + x ⁡ b - e ⁡ b = x ⁡ b
155 154 mpteq2dva ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → b ∈ I ⟼ e ⁡ b + x ⁡ b - e ⁡ b = b ∈ I ⟼ x ⁡ b
156 fvexd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ b ∈ I → e ⁡ b ∈ V
157 ovexd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∧ b ∈ I → x ⁡ b − e ⁡ b ∈ V
158 97 feqmptd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → e = b ∈ I ⟼ e ⁡ b
159 99 feqmptd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → x = b ∈ I ⟼ x ⁡ b
160 94 152 150 159 158 offval2 ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → x − f e = b ∈ I ⟼ x ⁡ b − e ⁡ b
161 94 156 157 158 160 offval2 ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → e + f x − f e = b ∈ I ⟼ e ⁡ b + x ⁡ b - e ⁡ b
162 155 161 159 3eqtr4d ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → e + f x − f e = x
163 162 oveq2d ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → ∑ ℂ fld ↾ 𝑠 ℕ 0 e + f x − f e = ∑ ℂ fld ↾ 𝑠 ℕ 0 x
164 149 163 eqtr3d ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → ∑ ℂ fld ↾ 𝑠 ℕ 0 e + ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e = ∑ ℂ fld ↾ 𝑠 ℕ 0 x
165 simplr ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N
166 164 165 eqnetrd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → ∑ ℂ fld ↾ 𝑠 ℕ 0 e + ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ M + N
167 oveq12 ⊢ ∑ ℂ fld ↾ 𝑠 ℕ 0 e = M ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e = N → ∑ ℂ fld ↾ 𝑠 ℕ 0 e + ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e = M + N
168 167 a1i ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → ∑ ℂ fld ↾ 𝑠 ℕ 0 e = M ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e = N → ∑ ℂ fld ↾ 𝑠 ℕ 0 e + ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e = M + N
169 168 necon3ad ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → ∑ ℂ fld ↾ 𝑠 ℕ 0 e + ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ M + N → ¬ ∑ ℂ fld ↾ 𝑠 ℕ 0 e = M ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e = N
170 166 169 mpd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → ¬ ∑ ℂ fld ↾ 𝑠 ℕ 0 e = M ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e = N
171 neorian ⊢ ∑ ℂ fld ↾ 𝑠 ℕ 0 e ≠ M ∨ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ N ↔ ¬ ∑ ℂ fld ↾ 𝑠 ℕ 0 e = M ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e = N
172 170 171 sylibr ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → ∑ ℂ fld ↾ 𝑠 ℕ 0 e ≠ M ∨ ∑ ℂ fld ↾ 𝑠 ℕ 0 x − f e ≠ N
173 52 74 172 mpjaodan ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N ∧ e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x → P ⁡ e ⋅ R Q ⁡ x − f e = 0 R
174 173 mpteq2dva ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N → e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ⟼ P ⁡ e ⋅ R Q ⁡ x − f e = e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ⟼ 0 R
175 174 oveq2d ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N → ∑ R e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x P ⁡ e ⋅ R Q ⁡ x − f e = ∑ R e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x 0 R
176 ringmnd ⊢ R ∈ Ring → R ∈ Mnd
177 4 176 syl ⊢ φ → R ∈ Mnd
178 177 ad2antrr ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N → R ∈ Mnd
179 ovex ⊢ ℕ 0 I ∈ V
180 179 rabex ⊢ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∈ V
181 180 rabex ⊢ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∈ V
182 36 gsumz ⊢ R ∈ Mnd ∧ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x ∈ V → ∑ R e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x 0 R = 0 R
183 178 181 182 sylancl ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N → ∑ R e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x 0 R = 0 R
184 175 183 eqtrd ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N → ∑ R e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x P ⁡ e ⋅ R Q ⁡ x − f e = 0 R
185 184 ex ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → ∑ ℂ fld ↾ 𝑠 ℕ 0 x ≠ M + N → ∑ R e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x P ⁡ e ⋅ R Q ⁡ x − f e = 0 R
186 185 necon1d ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → ∑ R e ∈ c ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | c ≤ f x P ⁡ e ⋅ R Q ⁡ x − f e ≠ 0 R → ∑ ℂ fld ↾ 𝑠 ℕ 0 x = M + N
187 23 186 sylbid ⊢ φ ∧ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → P · ˙ Q ⁡ x ≠ 0 R → ∑ ℂ fld ↾ 𝑠 ℕ 0 x = M + N
188 187 ralrimiva ⊢ φ → ∀ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin P · ˙ Q ⁡ x ≠ 0 R → ∑ ℂ fld ↾ 𝑠 ℕ 0 x = M + N
189 1 5 mhprcl ⊢ φ → M ∈ ℕ 0
190 1 6 mhprcl ⊢ φ → N ∈ ℕ 0
191 189 190 nn0addcld ⊢ φ → M + N ∈ ℕ 0
192 2 93 4 mplringd ⊢ φ → Y ∈ Ring
193 13 3 192 16 17 ringcld ⊢ φ → P · ˙ Q ∈ Base Y
194 1 2 13 36 15 191 193 ismhp3 ⊢ φ → P · ˙ Q ∈ H ⁡ M + N ↔ ∀ x ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin P · ˙ Q ⁡ x ≠ 0 R → ∑ ℂ fld ↾ 𝑠 ℕ 0 x = M + N
195 188 194 mpbird ⊢ φ → P · ˙ Q ∈ H ⁡ M + N