mhpmulcl - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mhpmulcl		Structured version Visualization version GIF version

Theorem mhpmulcl 21621

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

**Hypotheses**
Ref	Expression
mhpmulcl.h	⊢ 𝐻 = (𝐼 mHomP 𝑅)
mhpmulcl.y	⊢ 𝑌 = (𝐼 mPoly 𝑅)
mhpmulcl.t	⊢ · = (._r‘𝑌)
mhpmulcl.i	⊢ (𝜑 → 𝐼 ∈ 𝑉)
mhpmulcl.r	⊢ (𝜑 → 𝑅 ∈ Ring)
mhpmulcl.m	⊢ (𝜑 → 𝑀 ∈ ℕ₀)
mhpmulcl.n	⊢ (𝜑 → 𝑁 ∈ ℕ₀)
mhpmulcl.p	⊢ (𝜑 → 𝑃 ∈ (𝐻‘𝑀))
mhpmulcl.q	⊢ (𝜑 → 𝑄 ∈ (𝐻‘𝑁))

**Assertion**
Ref	Expression
mhpmulcl	⊢ (𝜑 → (𝑃 · 𝑄) ∈ (𝐻‘(𝑀 + 𝑁)))

Proof of Theorem mhpmulcl Dummy variables 𝑏 𝑑 𝑒 𝑖 𝑥 𝑐 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mhpmulcl.y	. . . . . . . 8 ⊢ 𝑌 = (𝐼 mPoly 𝑅)
2		eqid 2731	. . . . . . . 8 ⊢ (Base‘𝑌) = (Base‘𝑌)
3		eqid 2731	. . . . . . . 8 ⊢ (._r‘𝑅) = (._r‘𝑅)
4		mhpmulcl.t	. . . . . . . 8 ⊢ · = (._r‘𝑌)
5		eqid 2731	. . . . . . . 8 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}
6		mhpmulcl.h	. . . . . . . . 9 ⊢ 𝐻 = (𝐼 mHomP 𝑅)
7		mhpmulcl.i	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
8		mhpmulcl.r	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ Ring)
9		mhpmulcl.m	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
10		mhpmulcl.p	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ (𝐻‘𝑀))
11	6, 1, 2, 7, 8, 9, 10	mhpmpl 21616	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ (Base‘𝑌))
12		mhpmulcl.n	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
13		mhpmulcl.q	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (𝐻‘𝑁))
14	6, 1, 2, 7, 8, 12, 13	mhpmpl 21616	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ (Base‘𝑌))
15	1, 2, 3, 4, 5, 11, 14	mplmul 21497	. . . . . . 7 ⊢ (𝜑 → (𝑃 · 𝑄) = (𝑑 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ↦ (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒)))))))
16	15	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → (𝑃 · 𝑄) = (𝑑 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ↦ (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒)))))))
17		breq2 5145	. . . . . . . . . 10 ⊢ (𝑑 = 𝑥 → (𝑐 ∘_r ≤ 𝑑 ↔ 𝑐 ∘_r ≤ 𝑥))
18	17	rabbidv 3439	. . . . . . . . 9 ⊢ (𝑑 = 𝑥 → {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
19		fvoveq1 7416	. . . . . . . . . 10 ⊢ (𝑑 = 𝑥 → (𝑄‘(𝑑 ∘_f − 𝑒)) = (𝑄‘(𝑥 ∘_f − 𝑒)))
20	19	oveq2d 7409	. . . . . . . . 9 ⊢ (𝑑 = 𝑥 → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒))) = ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))
21	18, 20	mpteq12dv 5232	. . . . . . . 8 ⊢ (𝑑 = 𝑥 → (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒)))) = (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒)))))
22	21	oveq2d 7409	. . . . . . 7 ⊢ (𝑑 = 𝑥 → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒))))) = (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))))
23	22	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑑 = 𝑥) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒))))) = (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))))
24		simpr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
25		ovexd 7428	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) ∈ V)
26	16, 23, 24, 25	fvmptd 6991	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → ((𝑃 · 𝑄)‘𝑥) = (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))))
27	26	neeq1d 2999	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → (((𝑃 · 𝑄)‘𝑥) ≠ (0_g‘𝑅) ↔ (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) ≠ (0_g‘𝑅)))
28		simp-4l 781	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝜑)
29		oveq2 7401	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑒 → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒))
30	29	eqeq1d 2733	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑒 → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀 ↔ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) = 𝑀))
31	30	necon3bbid 2977	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑒 → (¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀 ↔ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀))
32		simplr 767	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
33		elrabi 3673	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} → 𝑒 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
34	32, 33	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑒 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
35		simpr 485	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀)
36	31, 34, 35	elrabd 3681	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀})
37		notrab 4307	. . . . . . . . . . . . . 14 ⊢ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀}) = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀}
38	36, 37	eleqtrrdi 2843	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑒 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀}))
39		eqid 2731	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑅) = (Base‘𝑅)
40	1, 39, 2, 5, 11	mplelf 21486	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑅))
41		eqid 2731	. . . . . . . . . . . . . . 15 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
42	6, 41, 5, 7, 8, 9, 10	mhpdeg 21617	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 supp (0_g‘𝑅)) ⊆ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀})
43		ovex 7426	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ↑_m 𝐼) ∈ V
44	43	rabex 5325	. . . . . . . . . . . . . . 15 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∈ V
45	44	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∈ V)
46		fvexd 6893	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝑅) ∈ V)
47	40, 42, 45, 46	suppssr 8163	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑒 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀})) → (𝑃‘𝑒) = (0_g‘𝑅))
48	28, 38, 47	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → (𝑃‘𝑒) = (0_g‘𝑅))
49	48	oveq1d 7408	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = ((0_g‘𝑅)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))
50	8	ad4antr 730	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑅 ∈ Ring)
51	14	ad4antr 730	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑄 ∈ (Base‘𝑌))
52	1, 39, 2, 5, 51	mplelf 21486	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑄:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑅))
53		simp-4r 782	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
54		eqid 2731	. . . . . . . . . . . . . . . 16 ⊢ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}
55	5, 54	psrbagconcl 21418	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒) ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
56	53, 32, 55	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → (𝑥 ∘_f − 𝑒) ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
57		elrabi 3673	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∘_f − 𝑒) ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} → (𝑥 ∘_f − 𝑒) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
58	56, 57	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → (𝑥 ∘_f − 𝑒) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
59	52, 58	ffvelcdmd 7072	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → (𝑄‘(𝑥 ∘_f − 𝑒)) ∈ (Base‘𝑅))
60	39, 3, 41	ringlz 20064	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ (𝑄‘(𝑥 ∘_f − 𝑒)) ∈ (Base‘𝑅)) → ((0_g‘𝑅)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = (0_g‘𝑅))
61	50, 59, 60	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → ((0_g‘𝑅)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = (0_g‘𝑅))
62	49, 61	eqtrd 2771	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = (0_g‘𝑅))
63		simp-4l 781	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝜑)
64		oveq2 7401	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑥 ∘_f − 𝑒) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)))
65	64	eqeq1d 2733	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑥 ∘_f − 𝑒) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁 ↔ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) = 𝑁))
66	65	necon3bbid 2977	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (𝑥 ∘_f − 𝑒) → (¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁 ↔ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁))
67		simp-4r 782	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
68		simplr 767	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
69	67, 68, 55	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → (𝑥 ∘_f − 𝑒) ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
70	69, 57	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → (𝑥 ∘_f − 𝑒) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
71		simpr 485	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁)
72	66, 70, 71	elrabd 3681	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → (𝑥 ∘_f − 𝑒) ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁})
73		notrab 4307	. . . . . . . . . . . . . 14 ⊢ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁}) = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁}
74	72, 73	eleqtrrdi 2843	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → (𝑥 ∘_f − 𝑒) ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁}))
75	1, 39, 2, 5, 14	mplelf 21486	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑄:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑅))
76	6, 41, 5, 7, 8, 12, 13	mhpdeg 21617	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑄 supp (0_g‘𝑅)) ⊆ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁})
77	75, 76, 45, 46	suppssr 8163	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∘_f − 𝑒) ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁})) → (𝑄‘(𝑥 ∘_f − 𝑒)) = (0_g‘𝑅))
78	63, 74, 77	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → (𝑄‘(𝑥 ∘_f − 𝑒)) = (0_g‘𝑅))
79	78	oveq2d 7409	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = ((𝑃‘𝑒)(._r‘𝑅)(0_g‘𝑅)))
80	8	ad4antr 730	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝑅 ∈ Ring)
81	11	ad4antr 730	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝑃 ∈ (Base‘𝑌))
82	1, 39, 2, 5, 81	mplelf 21486	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝑃:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑅))
83	33	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
84	83	adantr 481	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝑒 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
85	82, 84	ffvelcdmd 7072	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → (𝑃‘𝑒) ∈ (Base‘𝑅))
86	39, 3, 41	ringrz 20065	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ (𝑃‘𝑒) ∈ (Base‘𝑅)) → ((𝑃‘𝑒)(._r‘𝑅)(0_g‘𝑅)) = (0_g‘𝑅))
87	80, 85, 86	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → ((𝑃‘𝑒)(._r‘𝑅)(0_g‘𝑅)) = (0_g‘𝑅))
88	79, 87	eqtrd 2771	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = (0_g‘𝑅))
89		nn0subm 20934	. . . . . . . . . . . . . . . 16 ⊢ ℕ₀ ∈ (SubMnd‘ℂ_fld)
90		eqid 2731	. . . . . . . . . . . . . . . . 17 ⊢ (ℂ_fld ↾_s ℕ₀) = (ℂ_fld ↾_s ℕ₀)
91	90	submbas 18671	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ∈ (SubMnd‘ℂ_fld) → ℕ₀ = (Base‘(ℂ_fld ↾_s ℕ₀)))
92	89, 91	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ℕ₀ = (Base‘(ℂ_fld ↾_s ℕ₀))
93		cnfld0 20903	. . . . . . . . . . . . . . . . 17 ⊢ 0 = (0_g‘ℂ_fld)
94	90, 93	subm0 18672	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ∈ (SubMnd‘ℂ_fld) → 0 = (0_g‘(ℂ_fld ↾_s ℕ₀)))
95	89, 94	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 0 = (0_g‘(ℂ_fld ↾_s ℕ₀))
96		nn0ex 12460	. . . . . . . . . . . . . . . 16 ⊢ ℕ₀ ∈ V
97		cnfldadd 20883	. . . . . . . . . . . . . . . . 17 ⊢ + = (+_g‘ℂ_fld)
98	90, 97	ressplusg 17217	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ∈ V → + = (+_g‘(ℂ_fld ↾_s ℕ₀)))
99	96, 98	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ + = (+_g‘(ℂ_fld ↾_s ℕ₀))
100		cnring 20901	. . . . . . . . . . . . . . . . . 18 ⊢ ℂ_fld ∈ Ring
101		ringcmn 20056	. . . . . . . . . . . . . . . . . 18 ⊢ (ℂ_fld ∈ Ring → ℂ_fld ∈ CMnd)
102	100, 101	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ℂ_fld ∈ CMnd
103	90	submcmn 19666	. . . . . . . . . . . . . . . . 17 ⊢ ((ℂ_fld ∈ CMnd ∧ ℕ₀ ∈ (SubMnd‘ℂ_fld)) → (ℂ_fld ↾_s ℕ₀) ∈ CMnd)
104	102, 89, 103	mp2an 690	. . . . . . . . . . . . . . . 16 ⊢ (ℂ_fld ↾_s ℕ₀) ∈ CMnd
105	104	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (ℂ_fld ↾_s ℕ₀) ∈ CMnd)
106	7	ad3antrrr 728	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝐼 ∈ 𝑉)
107	5	psrbagf 21402	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} → 𝑒:𝐼⟶ℕ₀)
108	83, 107	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒:𝐼⟶ℕ₀)
109		simpllr 774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
110	5	psrbagf 21402	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} → 𝑥:𝐼⟶ℕ₀)
111	109, 110	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑥:𝐼⟶ℕ₀)
112	111	ffnd 6705	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑥 Fn 𝐼)
113	108	ffnd 6705	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 Fn 𝐼)
114		inidm 4214	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∩ 𝐼) = 𝐼
115		eqidd 2732	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑥‘𝑖) = (𝑥‘𝑖))
116		eqidd 2732	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑒‘𝑖) = (𝑒‘𝑖))
117	112, 113, 106, 106, 114, 115, 116	offval 7662	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒) = (𝑖 ∈ 𝐼 ↦ ((𝑥‘𝑖) − (𝑒‘𝑖))))
118		simpl 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}))
119		simplr 767	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
120		breq1 5144	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = 𝑒 → (𝑐 ∘_r ≤ 𝑥 ↔ 𝑒 ∘_r ≤ 𝑥))
121	120	elrab 3679	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↔ (𝑒 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∧ 𝑒 ∘_r ≤ 𝑥))
122	121	simprbi 497	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} → 𝑒 ∘_r ≤ 𝑥)
123	119, 122	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → 𝑒 ∘_r ≤ 𝑥)
124		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → 𝑖 ∈ 𝐼)
125	113, 112, 106, 106, 114, 116, 115	ofrval 7665	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑒 ∘_r ≤ 𝑥 ∧ 𝑖 ∈ 𝐼) → (𝑒‘𝑖) ≤ (𝑥‘𝑖))
126	118, 123, 124, 125	syl3anc 1371	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑒‘𝑖) ≤ (𝑥‘𝑖))
127	108	ffvelcdmda 7071	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑒‘𝑖) ∈ ℕ₀)
128	111	ffvelcdmda 7071	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑥‘𝑖) ∈ ℕ₀)
129		nn0sub 12504	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒‘𝑖) ∈ ℕ₀ ∧ (𝑥‘𝑖) ∈ ℕ₀) → ((𝑒‘𝑖) ≤ (𝑥‘𝑖) ↔ ((𝑥‘𝑖) − (𝑒‘𝑖)) ∈ ℕ₀))
130	127, 128, 129	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → ((𝑒‘𝑖) ≤ (𝑥‘𝑖) ↔ ((𝑥‘𝑖) − (𝑒‘𝑖)) ∈ ℕ₀))
131	126, 130	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → ((𝑥‘𝑖) − (𝑒‘𝑖)) ∈ ℕ₀)
132	117, 131	fmpt3d 7100	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒):𝐼⟶ℕ₀)
133	108	ffund 6708	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → Fun 𝑒)
134		c0ex 11190	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ V
135	106, 134	jctir 521	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝐼 ∈ 𝑉 ∧ 0 ∈ V))
136		fsuppeq 8142	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑒:𝐼⟶ℕ₀ → (𝑒 supp 0) = (^◡𝑒 “ (ℕ₀ ∖ {0}))))
137	135, 108, 136	sylc 65	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 supp 0) = (^◡𝑒 “ (ℕ₀ ∖ {0})))
138		dfn2 12467	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ = (ℕ₀ ∖ {0})
139	138	imaeq2i 6047	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝑒 “ ℕ) = (^◡𝑒 “ (ℕ₀ ∖ {0}))
140	137, 139	eqtr4di 2789	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 supp 0) = (^◡𝑒 “ ℕ))
141	5	psrbag 21401	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ 𝑉 → (𝑒 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ↔ (𝑒:𝐼⟶ℕ₀ ∧ (^◡𝑒 “ ℕ) ∈ Fin)))
142	106, 141	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ↔ (𝑒:𝐼⟶ℕ₀ ∧ (^◡𝑒 “ ℕ) ∈ Fin)))
143	83, 142	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒:𝐼⟶ℕ₀ ∧ (^◡𝑒 “ ℕ) ∈ Fin))
144	143	simprd 496	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (^◡𝑒 “ ℕ) ∈ Fin)
145	140, 144	eqeltrd 2832	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 supp 0) ∈ Fin)
146	83	elexd 3493	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 ∈ V)
147		isfsupp 9348	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 ∈ V ∧ 0 ∈ V) → (𝑒 finSupp 0 ↔ (Fun 𝑒 ∧ (𝑒 supp 0) ∈ Fin)))
148	146, 134, 147	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 finSupp 0 ↔ (Fun 𝑒 ∧ (𝑒 supp 0) ∈ Fin)))
149	133, 145, 148	mpbir2and 711	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 finSupp 0)
150	112, 113, 106, 106	offun 7667	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → Fun (𝑥 ∘_f − 𝑒))
151	5	psrbagfsupp 21404	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} → 𝑥 finSupp 0)
152	109, 151	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑥 finSupp 0)
153	152, 149	fsuppunfi 9366	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑥 supp 0) ∪ (𝑒 supp 0)) ∈ Fin)
154		0nn0 12469	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℕ₀
155	154	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 0 ∈ ℕ₀)
156		0m0e0 12314	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 − 0) = 0
157	156	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (0 − 0) = 0)
158	106, 155, 111, 108, 157	suppofssd 8170	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑥 ∘_f − 𝑒) supp 0) ⊆ ((𝑥 supp 0) ∪ (𝑒 supp 0)))
159	153, 158	ssfid 9250	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑥 ∘_f − 𝑒) supp 0) ∈ Fin)
160		ovexd 7428	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒) ∈ V)
161		isfsupp 9348	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∘_f − 𝑒) ∈ V ∧ 0 ∈ V) → ((𝑥 ∘_f − 𝑒) finSupp 0 ↔ (Fun (𝑥 ∘_f − 𝑒) ∧ ((𝑥 ∘_f − 𝑒) supp 0) ∈ Fin)))
162	160, 134, 161	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑥 ∘_f − 𝑒) finSupp 0 ↔ (Fun (𝑥 ∘_f − 𝑒) ∧ ((𝑥 ∘_f − 𝑒) supp 0) ∈ Fin)))
163	150, 159, 162	mpbir2and 711	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒) finSupp 0)
164	92, 95, 99, 105, 106, 108, 132, 149, 163	gsumadd 19750	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑒 ∘_f + (𝑥 ∘_f − 𝑒))) = (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) + ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒))))
165	108	ffvelcdmda 7071	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑒‘𝑏) ∈ ℕ₀)
166	165	nn0cnd 12516	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑒‘𝑏) ∈ ℂ)
167	111	ffvelcdmda 7071	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑥‘𝑏) ∈ ℕ₀)
168	167	nn0cnd 12516	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑥‘𝑏) ∈ ℂ)
169	166, 168	pncan3d 11556	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → ((𝑒‘𝑏) + ((𝑥‘𝑏) − (𝑒‘𝑏))) = (𝑥‘𝑏))
170	169	mpteq2dva 5241	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑏 ∈ 𝐼 ↦ ((𝑒‘𝑏) + ((𝑥‘𝑏) − (𝑒‘𝑏)))) = (𝑏 ∈ 𝐼 ↦ (𝑥‘𝑏)))
171		fvexd 6893	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑒‘𝑏) ∈ V)
172		ovexd 7428	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → ((𝑥‘𝑏) − (𝑒‘𝑏)) ∈ V)
173	108	feqmptd 6946	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 = (𝑏 ∈ 𝐼 ↦ (𝑒‘𝑏)))
174	111	feqmptd 6946	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑥 = (𝑏 ∈ 𝐼 ↦ (𝑥‘𝑏)))
175	106, 167, 165, 174, 173	offval2 7673	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒) = (𝑏 ∈ 𝐼 ↦ ((𝑥‘𝑏) − (𝑒‘𝑏))))
176	106, 171, 172, 173, 175	offval2 7673	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 ∘_f + (𝑥 ∘_f − 𝑒)) = (𝑏 ∈ 𝐼 ↦ ((𝑒‘𝑏) + ((𝑥‘𝑏) − (𝑒‘𝑏)))))
177	170, 176, 174	3eqtr4d 2781	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 ∘_f + (𝑥 ∘_f − 𝑒)) = 𝑥)
178	177	oveq2d 7409	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑒 ∘_f + (𝑥 ∘_f − 𝑒))) = ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥))
179	164, 178	eqtr3d 2773	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) + ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒))) = ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥))
180		simplr 767	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁))
181	179, 180	eqnetrd 3007	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) + ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒))) ≠ (𝑀 + 𝑁))
182		oveq12 7402	. . . . . . . . . . . . . 14 ⊢ ((((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) = 𝑀 ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) = 𝑁) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) + ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒))) = (𝑀 + 𝑁))
183	182	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) = 𝑀 ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) = 𝑁) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) + ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒))) = (𝑀 + 𝑁)))
184	183	necon3ad 2952	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) + ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒))) ≠ (𝑀 + 𝑁) → ¬ (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) = 𝑀 ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) = 𝑁)))
185	181, 184	mpd 15	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ¬ (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) = 𝑀 ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) = 𝑁))
186		neorian 3036	. . . . . . . . . . 11 ⊢ ((((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀 ∨ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) ↔ ¬ (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) = 𝑀 ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) = 𝑁))
187	185, 186	sylibr 233	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀 ∨ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁))
188	62, 88, 187	mpjaodan 957	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = (0_g‘𝑅))
189	188	mpteq2dva 5241	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒)))) = (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ (0_g‘𝑅)))
190	189	oveq2d 7409	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) = (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ (0_g‘𝑅))))
191		ringmnd 20024	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
192	8, 191	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ Mnd)
193	192	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → 𝑅 ∈ Mnd)
194	44	rabex 5325	. . . . . . . 8 ⊢ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ∈ V
195	41	gsumz 18692	. . . . . . . 8 ⊢ ((𝑅 ∈ Mnd ∧ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ∈ V) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ (0_g‘𝑅))) = (0_g‘𝑅))
196	193, 194, 195	sylancl 586	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ (0_g‘𝑅))) = (0_g‘𝑅))
197	190, 196	eqtrd 2771	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) = (0_g‘𝑅))
198	197	ex 413	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) = (0_g‘𝑅)))
199	198	necon1d 2961	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → ((𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) ≠ (0_g‘𝑅) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) = (𝑀 + 𝑁)))
200	27, 199	sylbid 239	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → (((𝑃 · 𝑄)‘𝑥) ≠ (0_g‘𝑅) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) = (𝑀 + 𝑁)))
201	200	ralrimiva 3145	. 2 ⊢ (𝜑 → ∀𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} (((𝑃 · 𝑄)‘𝑥) ≠ (0_g‘𝑅) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) = (𝑀 + 𝑁)))
202	9, 12	nn0addcld 12518	. . 3 ⊢ (𝜑 → (𝑀 + 𝑁) ∈ ℕ₀)
203	1	mplring 21506	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring)
204	7, 8, 203	syl2anc 584	. . . 4 ⊢ (𝜑 → 𝑌 ∈ Ring)
205	2, 4	ringcl 20031	. . . 4 ⊢ ((𝑌 ∈ Ring ∧ 𝑃 ∈ (Base‘𝑌) ∧ 𝑄 ∈ (Base‘𝑌)) → (𝑃 · 𝑄) ∈ (Base‘𝑌))
206	204, 11, 14, 205	syl3anc 1371	. . 3 ⊢ (𝜑 → (𝑃 · 𝑄) ∈ (Base‘𝑌))
207	6, 1, 2, 41, 5, 7, 8, 202, 206	ismhp3 21615	. 2 ⊢ (𝜑 → ((𝑃 · 𝑄) ∈ (𝐻‘(𝑀 + 𝑁)) ↔ ∀𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} (((𝑃 · 𝑄)‘𝑥) ≠ (0_g‘𝑅) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) = (𝑀 + 𝑁))))
208	201, 207	mpbird 256	1 ⊢ (𝜑 → (𝑃 · 𝑄) ∈ (𝐻‘(𝑀 + 𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 = wceq 1541 ∈ wcel 2106 ≠ wne 2939 ∀wral 3060 {crab 3431 Vcvv 3473 ∖ cdif 3941 ∪ cun 3942 {csn 4622 class class class wbr 5141 ↦ cmpt 5224 ^◡ccnv 5668 “ cima 5672 Fun wfun 6526 ⟶wf 6528 ‘cfv 6532 (class class class)co 7393 ∘_f cof 7651 ∘_r cofr 7652 supp csupp 8128 ↑_m cmap 8803 Fincfn 8922 finSupp cfsupp 9344 0cc0 11092 + caddc 11095 ≤ cle 11231 − cmin 11426 ℕcn 12194 ℕ₀cn0 12454 Basecbs 17126 ↾_s cress 17155 +_gcplusg 17179 ._rcmulr 17180 0_gc0g 17367 Σ_g cgsu 17368 Mndcmnd 18602 SubMndcsubmnd 18646 CMndccmn 19612 Ringcrg 20014 ℂ_fldccnfld 20878 mPoly cmpl 21390 mHomP cmhp 21601

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-rep 5278 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7708 ax-cnex 11148 ax-resscn 11149 ax-1cn 11150 ax-icn 11151 ax-addcl 11152 ax-addrcl 11153 ax-mulcl 11154 ax-mulrcl 11155 ax-mulcom 11156 ax-addass 11157 ax-mulass 11158 ax-distr 11159 ax-i2m1 11160 ax-1ne0 11161 ax-1rid 11162 ax-rnegex 11163 ax-rrecex 11164 ax-cnre 11165 ax-pre-lttri 11166 ax-pre-lttrn 11167 ax-pre-ltadd 11168 ax-pre-mulgt0 11169 ax-addf 11171 ax-mulf 11172

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4523 df-pw 4598 df-sn 4623 df-pr 4625 df-tp 4627 df-op 4629 df-uni 4902 df-int 4944 df-iun 4992 df-iin 4993 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5567 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-se 5625 df-we 5626 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-pred 6289 df-ord 6356 df-on 6357 df-lim 6358 df-suc 6359 df-iota 6484 df-fun 6534 df-fn 6535 df-f 6536 df-f1 6537 df-fo 6538 df-f1o 6539 df-fv 6540 df-isom 6541 df-riota 7349 df-ov 7396 df-oprab 7397 df-mpo 7398 df-of 7653 df-ofr 7654 df-om 7839 df-1st 7957 df-2nd 7958 df-supp 8129 df-frecs 8248 df-wrecs 8279 df-recs 8353 df-rdg 8392 df-1o 8448 df-er 8686 df-map 8805 df-pm 8806 df-ixp 8875 df-en 8923 df-dom 8924 df-sdom 8925 df-fin 8926 df-fsupp 9345 df-sup 9419 df-oi 9487 df-card 9916 df-pnf 11232 df-mnf 11233 df-xr 11234 df-ltxr 11235 df-le 11236 df-sub 11428 df-neg 11429 df-nn 12195 df-2 12257 df-3 12258 df-4 12259 df-5 12260 df-6 12261 df-7 12262 df-8 12263 df-9 12264 df-n0 12455 df-z 12541 df-dec 12660 df-uz 12805 df-fz 13467 df-fzo 13610 df-seq 13949 df-hash 14273 df-struct 17062 df-sets 17079 df-slot 17097 df-ndx 17109 df-base 17127 df-ress 17156 df-plusg 17192 df-mulr 17193 df-starv 17194 df-sca 17195 df-vsca 17196 df-ip 17197 df-tset 17198 df-ple 17199 df-ds 17201 df-unif 17202 df-hom 17203 df-cco 17204 df-0g 17369 df-gsum 17370 df-prds 17375 df-pws 17377 df-mre 17512 df-mrc 17513 df-acs 17515 df-mgm 18543 df-sgrp 18592 df-mnd 18603 df-mhm 18647 df-submnd 18648 df-grp 18797 df-minusg 18798 df-mulg 18923 df-subg 18975 df-ghm 19056 df-cntz 19147 df-cmn 19614 df-abl 19615 df-mgp 19947 df-ur 19964 df-ring 20016 df-cring 20017 df-subrg 20310 df-cnfld 20879 df-psr 21393 df-mpl 21395 df-mhp 21605

This theorem is referenced by: mhppwdeg 21622

W3C validator