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 21539

Description: A product of homogeneous polynomials is a homogeneous polynomial whose degree is the sum of the degrees of the factors. Compare mdegmulle2 25444 (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 2736	. . . . . . . 8 ⊢ (Base‘𝑌) = (Base‘𝑌)
3		eqid 2736	. . . . . . . 8 ⊢ (._r‘𝑅) = (._r‘𝑅)
4		mhpmulcl.t	. . . . . . . 8 ⊢ · = (._r‘𝑌)
5		eqid 2736	. . . . . . . 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 21534	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ (Base‘𝑌))
12		mhpmulcl.n	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
13		mhpmulcl.q	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (𝐻‘𝑁))
14	6, 1, 2, 7, 8, 12, 13	mhpmpl 21534	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ (Base‘𝑌))
15	1, 2, 3, 4, 5, 11, 14	mplmul 21415	. . . . . . 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 5109	. . . . . . . . . 10 ⊢ (𝑑 = 𝑥 → (𝑐 ∘_r ≤ 𝑑 ↔ 𝑐 ∘_r ≤ 𝑥))
18	17	rabbidv 3415	. . . . . . . . 9 ⊢ (𝑑 = 𝑥 → {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
19		fvoveq1 7380	. . . . . . . . . 10 ⊢ (𝑑 = 𝑥 → (𝑄‘(𝑑 ∘_f − 𝑒)) = (𝑄‘(𝑥 ∘_f − 𝑒)))
20	19	oveq2d 7373	. . . . . . . . 9 ⊢ (𝑑 = 𝑥 → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒))) = ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))
21	18, 20	mpteq12dv 5196	. . . . . . . 8 ⊢ (𝑑 = 𝑥 → (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒)))) = (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒)))))
22	21	oveq2d 7373	. . . . . . 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 7392	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) ∈ V)
26	16, 23, 24, 25	fvmptd 6955	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → ((𝑃 · 𝑄)‘𝑥) = (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))))
27	26	neeq1d 3003	. . . 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 7365	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑒 → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒))
30	29	eqeq1d 2738	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑒 → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀 ↔ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) = 𝑀))
31	30	necon3bbid 2981	. . . . . . . . . . . . . . 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 3639	. . . . . . . . . . . . . . . 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 3647	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀})
37		notrab 4271	. . . . . . . . . . . . . 14 ⊢ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀}) = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀}
38	36, 37	eleqtrrdi 2849	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑒 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀}))
39		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑅) = (Base‘𝑅)
40	1, 39, 2, 5, 11	mplelf 21404	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑅))
41		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
42	6, 41, 5, 7, 8, 9, 10	mhpdeg 21535	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 supp (0_g‘𝑅)) ⊆ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀})
43		ovex 7390	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ↑_m 𝐼) ∈ V
44	43	rabex 5289	. . . . . . . . . . . . . . 15 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∈ V
45	44	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∈ V)
46		fvexd 6857	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝑅) ∈ V)
47	40, 42, 45, 46	suppssr 8127	. . . . . . . . . . . . 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 7372	. . . . . . . . . . 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 21404	. . . . . . . . . . . . 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 2736	. . . . . . . . . . . . . . . 16 ⊢ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}
55	5, 54	psrbagconcl 21336	. . . . . . . . . . . . . . 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 3639	. . . . . . . . . . . . . 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 7036	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → (𝑄‘(𝑥 ∘_f − 𝑒)) ∈ (Base‘𝑅))
60	39, 3, 41	ringlz 20011	. . . . . . . . . . . 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 2776	. . . . . . . . . 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 7365	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑥 ∘_f − 𝑒) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)))
65	64	eqeq1d 2738	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑥 ∘_f − 𝑒) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁 ↔ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) = 𝑁))
66	65	necon3bbid 2981	. . . . . . . . . . . . . . 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 3647	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → (𝑥 ∘_f − 𝑒) ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁})
73		notrab 4271	. . . . . . . . . . . . . 14 ⊢ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁}) = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁}
74	72, 73	eleqtrrdi 2849	. . . . . . . . . . . . 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 21404	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑄:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑅))
76	6, 41, 5, 7, 8, 12, 13	mhpdeg 21535	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑄 supp (0_g‘𝑅)) ⊆ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁})
77	75, 76, 45, 46	suppssr 8127	. . . . . . . . . . . . 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 7373	. . . . . . . . . . 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 21404	. . . . . . . . . . . . 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 7036	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → (𝑃‘𝑒) ∈ (Base‘𝑅))
86	39, 3, 41	ringrz 20012	. . . . . . . . . . . 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 2776	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = (0_g‘𝑅))
89		nn0subm 20852	. . . . . . . . . . . . . . . 16 ⊢ ℕ₀ ∈ (SubMnd‘ℂ_fld)
90		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (ℂ_fld ↾_s ℕ₀) = (ℂ_fld ↾_s ℕ₀)
91	90	submbas 18625	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ∈ (SubMnd‘ℂ_fld) → ℕ₀ = (Base‘(ℂ_fld ↾_s ℕ₀)))
92	89, 91	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ℕ₀ = (Base‘(ℂ_fld ↾_s ℕ₀))
93		cnfld0 20821	. . . . . . . . . . . . . . . . 17 ⊢ 0 = (0_g‘ℂ_fld)
94	90, 93	subm0 18626	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ∈ (SubMnd‘ℂ_fld) → 0 = (0_g‘(ℂ_fld ↾_s ℕ₀)))
95	89, 94	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 0 = (0_g‘(ℂ_fld ↾_s ℕ₀))
96		nn0ex 12419	. . . . . . . . . . . . . . . 16 ⊢ ℕ₀ ∈ V
97		cnfldadd 20801	. . . . . . . . . . . . . . . . 17 ⊢ + = (+_g‘ℂ_fld)
98	90, 97	ressplusg 17171	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ∈ V → + = (+_g‘(ℂ_fld ↾_s ℕ₀)))
99	96, 98	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ + = (+_g‘(ℂ_fld ↾_s ℕ₀))
100		cnring 20819	. . . . . . . . . . . . . . . . . 18 ⊢ ℂ_fld ∈ Ring
101		ringcmn 20003	. . . . . . . . . . . . . . . . . 18 ⊢ (ℂ_fld ∈ Ring → ℂ_fld ∈ CMnd)
102	100, 101	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ℂ_fld ∈ CMnd
103	90	submcmn 19616	. . . . . . . . . . . . . . . . 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 21320	. . . . . . . . . . . . . . . 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 21320	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} → 𝑥:𝐼⟶ℕ₀)
111	109, 110	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑥:𝐼⟶ℕ₀)
112	111	ffnd 6669	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑥 Fn 𝐼)
113	108	ffnd 6669	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 Fn 𝐼)
114		inidm 4178	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∩ 𝐼) = 𝐼
115		eqidd 2737	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑥‘𝑖) = (𝑥‘𝑖))
116		eqidd 2737	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑒‘𝑖) = (𝑒‘𝑖))
117	112, 113, 106, 106, 114, 115, 116	offval 7626	. . . . . . . . . . . . . . . 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 5108	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = 𝑒 → (𝑐 ∘_r ≤ 𝑥 ↔ 𝑒 ∘_r ≤ 𝑥))
121	120	elrab 3645	. . . . . . . . . . . . . . . . . . . 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 7629	. . . . . . . . . . . . . . . . . 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 7035	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑒‘𝑖) ∈ ℕ₀)
128	111	ffvelcdmda 7035	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑥‘𝑖) ∈ ℕ₀)
129		nn0sub 12463	. . . . . . . . . . . . . . . . . 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 7064	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒):𝐼⟶ℕ₀)
133	108	ffund 6672	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → Fun 𝑒)
134		c0ex 11149	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ V
135	106, 134	jctir 521	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝐼 ∈ 𝑉 ∧ 0 ∈ V))
136		fsuppeq 8106	. . . . . . . . . . . . . . . . . . 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 12426	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ = (ℕ₀ ∖ {0})
139	138	imaeq2i 6011	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝑒 “ ℕ) = (^◡𝑒 “ (ℕ₀ ∖ {0}))
140	137, 139	eqtr4di 2794	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 supp 0) = (^◡𝑒 “ ℕ))
141	5	psrbag 21319	. . . . . . . . . . . . . . . . . . . 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 2838	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 supp 0) ∈ Fin)
146	83	elexd 3465	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 ∈ V)
147		isfsupp 9309	. . . . . . . . . . . . . . . . 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 7631	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → Fun (𝑥 ∘_f − 𝑒))
151	5	psrbagfsupp 21322	. . . . . . . . . . . . . . . . . . 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 9325	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑥 supp 0) ∪ (𝑒 supp 0)) ∈ Fin)
154		0nn0 12428	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℕ₀
155	154	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 0 ∈ ℕ₀)
156		0m0e0 12273	. . . . . . . . . . . . . . . . . . 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 8134	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑥 ∘_f − 𝑒) supp 0) ⊆ ((𝑥 supp 0) ∪ (𝑒 supp 0)))
159	153, 158	ssfid 9211	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑥 ∘_f − 𝑒) supp 0) ∈ Fin)
160		ovexd 7392	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒) ∈ V)
161		isfsupp 9309	. . . . . . . . . . . . . . . . 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 19700	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑒 ∘_f + (𝑥 ∘_f − 𝑒))) = (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) + ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒))))
165	108	ffvelcdmda 7035	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑒‘𝑏) ∈ ℕ₀)
166	165	nn0cnd 12475	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑒‘𝑏) ∈ ℂ)
167	111	ffvelcdmda 7035	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑥‘𝑏) ∈ ℕ₀)
168	167	nn0cnd 12475	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑥‘𝑏) ∈ ℂ)
169	166, 168	pncan3d 11515	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → ((𝑒‘𝑏) + ((𝑥‘𝑏) − (𝑒‘𝑏))) = (𝑥‘𝑏))
170	169	mpteq2dva 5205	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑏 ∈ 𝐼 ↦ ((𝑒‘𝑏) + ((𝑥‘𝑏) − (𝑒‘𝑏)))) = (𝑏 ∈ 𝐼 ↦ (𝑥‘𝑏)))
171		fvexd 6857	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑒‘𝑏) ∈ V)
172		ovexd 7392	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → ((𝑥‘𝑏) − (𝑒‘𝑏)) ∈ V)
173	108	feqmptd 6910	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 = (𝑏 ∈ 𝐼 ↦ (𝑒‘𝑏)))
174	111	feqmptd 6910	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑥 = (𝑏 ∈ 𝐼 ↦ (𝑥‘𝑏)))
175	106, 167, 165, 174, 173	offval2 7637	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒) = (𝑏 ∈ 𝐼 ↦ ((𝑥‘𝑏) − (𝑒‘𝑏))))
176	106, 171, 172, 173, 175	offval2 7637	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 ∘_f + (𝑥 ∘_f − 𝑒)) = (𝑏 ∈ 𝐼 ↦ ((𝑒‘𝑏) + ((𝑥‘𝑏) − (𝑒‘𝑏)))))
177	170, 176, 174	3eqtr4d 2786	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 ∘_f + (𝑥 ∘_f − 𝑒)) = 𝑥)
178	177	oveq2d 7373	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑒 ∘_f + (𝑥 ∘_f − 𝑒))) = ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥))
179	164, 178	eqtr3d 2778	. . . . . . . . . . . . 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 3011	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) + ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒))) ≠ (𝑀 + 𝑁))
182		oveq12 7366	. . . . . . . . . . . . . 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 2956	. . . . . . . . . . . 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 3039	. . . . . . . . . . 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 5205	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒)))) = (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ (0_g‘𝑅)))
190	189	oveq2d 7373	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) = (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ (0_g‘𝑅))))
191		ringmnd 19974	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
192	8, 191	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ Mnd)
193	192	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → 𝑅 ∈ Mnd)
194	44	rabex 5289	. . . . . . . 8 ⊢ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ∈ V
195	41	gsumz 18646	. . . . . . . 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 2776	. . . . . 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 2965	. . . 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 3143	. 2 ⊢ (𝜑 → ∀𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} (((𝑃 · 𝑄)‘𝑥) ≠ (0_g‘𝑅) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) = (𝑀 + 𝑁)))
202	9, 12	nn0addcld 12477	. . 3 ⊢ (𝜑 → (𝑀 + 𝑁) ∈ ℕ₀)
203	1	mplring 21424	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring)
204	7, 8, 203	syl2anc 584	. . . 4 ⊢ (𝜑 → 𝑌 ∈ Ring)
205	2, 4	ringcl 19981	. . . 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 21533	. 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 2943 ∀wral 3064 {crab 3407 Vcvv 3445 ∖ cdif 3907 ∪ cun 3908 {csn 4586 class class class wbr 5105 ↦ cmpt 5188 ^◡ccnv 5632 “ cima 5636 Fun wfun 6490 ⟶wf 6492 ‘cfv 6496 (class class class)co 7357 ∘_f cof 7615 ∘_r cofr 7616 supp csupp 8092 ↑_m cmap 8765 Fincfn 8883 finSupp cfsupp 9305 0cc0 11051 + caddc 11054 ≤ cle 11190 − cmin 11385 ℕcn 12153 ℕ₀cn0 12413 Basecbs 17083 ↾_s cress 17112 +_gcplusg 17133 ._rcmulr 17134 0_gc0g 17321 Σ_g cgsu 17322 Mndcmnd 18556 SubMndcsubmnd 18600 CMndccmn 19562 Ringcrg 19964 ℂ_fldccnfld 20796 mPoly cmpl 21308 mHomP cmhp 21519

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 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-addf 11130 ax-mulf 11131

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 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-tp 4591 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-iin 4957 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-se 5589 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-of 7617 df-ofr 7618 df-om 7803 df-1st 7921 df-2nd 7922 df-supp 8093 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-er 8648 df-map 8767 df-pm 8768 df-ixp 8836 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fsupp 9306 df-sup 9378 df-oi 9446 df-card 9875 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-nn 12154 df-2 12216 df-3 12217 df-4 12218 df-5 12219 df-6 12220 df-7 12221 df-8 12222 df-9 12223 df-n0 12414 df-z 12500 df-dec 12619 df-uz 12764 df-fz 13425 df-fzo 13568 df-seq 13907 df-hash 14231 df-struct 17019 df-sets 17036 df-slot 17054 df-ndx 17066 df-base 17084 df-ress 17113 df-plusg 17146 df-mulr 17147 df-starv 17148 df-sca 17149 df-vsca 17150 df-ip 17151 df-tset 17152 df-ple 17153 df-ds 17155 df-unif 17156 df-hom 17157 df-cco 17158 df-0g 17323 df-gsum 17324 df-prds 17329 df-pws 17331 df-mre 17466 df-mrc 17467 df-acs 17469 df-mgm 18497 df-sgrp 18546 df-mnd 18557 df-mhm 18601 df-submnd 18602 df-grp 18751 df-minusg 18752 df-mulg 18873 df-subg 18925 df-ghm 19006 df-cntz 19097 df-cmn 19564 df-abl 19565 df-mgp 19897 df-ur 19914 df-ring 19966 df-cring 19967 df-subrg 20220 df-cnfld 20797 df-psr 21311 df-mpl 21313 df-mhp 21523

This theorem is referenced by: mhppwdeg 21540

W3C validator