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 20897

Description: A product of homogeneous polynomials is a homogeneous polynomial whose degree is the sum of the degrees of the factors. Compare mdegmulle2 24784 (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 2758	. . . . . . . 8 ⊢ (Base‘𝑌) = (Base‘𝑌)
3		eqid 2758	. . . . . . . 8 ⊢ (._r‘𝑅) = (._r‘𝑅)
4		mhpmulcl.t	. . . . . . . 8 ⊢ · = (._r‘𝑌)
5		eqid 2758	. . . . . . . 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 20892	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ (Base‘𝑌))
12		mhpmulcl.n	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
13		mhpmulcl.q	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (𝐻‘𝑁))
14	6, 1, 2, 7, 8, 12, 13	mhpmpl 20892	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ (Base‘𝑌))
15	1, 2, 3, 4, 5, 11, 14	mplmul 20779	. . . . . . 7 ⊢ (𝜑 → (𝑃 · 𝑄) = (𝑑 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ↦ (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒)))))))
16	15	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → (𝑃 · 𝑄) = (𝑑 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ↦ (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒)))))))
17		breq2 5039	. . . . . . . . . 10 ⊢ (𝑑 = 𝑥 → (𝑐 ∘_r ≤ 𝑑 ↔ 𝑐 ∘_r ≤ 𝑥))
18	17	rabbidv 3392	. . . . . . . . 9 ⊢ (𝑑 = 𝑥 → {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
19		fvoveq1 7178	. . . . . . . . . 10 ⊢ (𝑑 = 𝑥 → (𝑄‘(𝑑 ∘_f − 𝑒)) = (𝑄‘(𝑥 ∘_f − 𝑒)))
20	19	oveq2d 7171	. . . . . . . . 9 ⊢ (𝑑 = 𝑥 → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒))) = ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))
21	18, 20	mpteq12dv 5120	. . . . . . . 8 ⊢ (𝑑 = 𝑥 → (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒)))) = (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒)))))
22	21	oveq2d 7171	. . . . . . 7 ⊢ (𝑑 = 𝑥 → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒))))) = (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))))
23	22	adantl 485	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑑 = 𝑥) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒))))) = (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))))
24		simpr 488	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
25		ovexd 7190	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) ∈ V)
26	16, 23, 24, 25	fvmptd 6770	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → ((𝑃 · 𝑄)‘𝑥) = (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))))
27	26	neeq1d 3010	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → (((𝑃 · 𝑄)‘𝑥) ≠ (0_g‘𝑅) ↔ (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) ≠ (0_g‘𝑅)))
28		simp-4l 782	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝜑)
29		oveq2 7163	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑒 → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒))
30	29	eqeq1d 2760	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑒 → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀 ↔ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) = 𝑀))
31	30	necon3bbid 2988	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑒 → (¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀 ↔ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀))
32		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
33		elrabi 3598	. . . . . . . . . . . . . . . 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 488	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀)
36	31, 34, 35	elrabd 3606	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀})
37		notrab 4216	. . . . . . . . . . . . . 14 ⊢ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀}) = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀}
38	36, 37	eleqtrrdi 2863	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑒 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀}))
39		eqid 2758	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑅) = (Base‘𝑅)
40	1, 39, 2, 5, 11	mplelf 20768	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑅))
41		eqid 2758	. . . . . . . . . . . . . . 15 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
42	6, 41, 5, 7, 8, 9, 10	mhpdeg 20893	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 supp (0_g‘𝑅)) ⊆ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀})
43		ovex 7188	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ↑_m 𝐼) ∈ V
44	43	rabex 5205	. . . . . . . . . . . . . . 15 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∈ V
45	44	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∈ V)
46		fvexd 6677	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝑅) ∈ V)
47	40, 42, 45, 46	suppssr 7875	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑒 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀})) → (𝑃‘𝑒) = (0_g‘𝑅))
48	28, 38, 47	syl2anc 587	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → (𝑃‘𝑒) = (0_g‘𝑅))
49	48	oveq1d 7170	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = ((0_g‘𝑅)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))
50	8	ad4antr 731	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑅 ∈ Ring)
51	14	ad4antr 731	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑄 ∈ (Base‘𝑌))
52	1, 39, 2, 5, 51	mplelf 20768	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑄:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑅))
53		simp-4r 783	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
54		eqid 2758	. . . . . . . . . . . . . . . 16 ⊢ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}
55	5, 54	psrbagconcl 20701	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒) ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
56	53, 32, 55	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → (𝑥 ∘_f − 𝑒) ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
57		elrabi 3598	. . . . . . . . . . . . . 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	ffvelrnd 6848	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → (𝑄‘(𝑥 ∘_f − 𝑒)) ∈ (Base‘𝑅))
60	39, 3, 41	ringlz 19413	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ (𝑄‘(𝑥 ∘_f − 𝑒)) ∈ (Base‘𝑅)) → ((0_g‘𝑅)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = (0_g‘𝑅))
61	50, 59, 60	syl2anc 587	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → ((0_g‘𝑅)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = (0_g‘𝑅))
62	49, 61	eqtrd 2793	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = (0_g‘𝑅))
63		simp-4l 782	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝜑)
64		oveq2 7163	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑥 ∘_f − 𝑒) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)))
65	64	eqeq1d 2760	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑥 ∘_f − 𝑒) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁 ↔ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) = 𝑁))
66	65	necon3bbid 2988	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (𝑥 ∘_f − 𝑒) → (¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁 ↔ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁))
67		simp-4r 783	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
68		simplr 768	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
69	67, 68, 55	syl2anc 587	. . . . . . . . . . . . . . . 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 488	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁)
72	66, 70, 71	elrabd 3606	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → (𝑥 ∘_f − 𝑒) ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁})
73		notrab 4216	. . . . . . . . . . . . . 14 ⊢ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁}) = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁}
74	72, 73	eleqtrrdi 2863	. . . . . . . . . . . . 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 20768	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑄:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑅))
76	6, 41, 5, 7, 8, 12, 13	mhpdeg 20893	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑄 supp (0_g‘𝑅)) ⊆ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁})
77	75, 76, 45, 46	suppssr 7875	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∘_f − 𝑒) ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁})) → (𝑄‘(𝑥 ∘_f − 𝑒)) = (0_g‘𝑅))
78	63, 74, 77	syl2anc 587	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → (𝑄‘(𝑥 ∘_f − 𝑒)) = (0_g‘𝑅))
79	78	oveq2d 7171	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = ((𝑃‘𝑒)(._r‘𝑅)(0_g‘𝑅)))
80	8	ad4antr 731	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝑅 ∈ Ring)
81	11	ad4antr 731	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝑃 ∈ (Base‘𝑌))
82	1, 39, 2, 5, 81	mplelf 20768	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝑃:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑅))
83	33	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
84	83	adantr 484	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝑒 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
85	82, 84	ffvelrnd 6848	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → (𝑃‘𝑒) ∈ (Base‘𝑅))
86	39, 3, 41	ringrz 19414	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ (𝑃‘𝑒) ∈ (Base‘𝑅)) → ((𝑃‘𝑒)(._r‘𝑅)(0_g‘𝑅)) = (0_g‘𝑅))
87	80, 85, 86	syl2anc 587	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → ((𝑃‘𝑒)(._r‘𝑅)(0_g‘𝑅)) = (0_g‘𝑅))
88	79, 87	eqtrd 2793	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = (0_g‘𝑅))
89		nn0subm 20226	. . . . . . . . . . . . . . . 16 ⊢ ℕ₀ ∈ (SubMnd‘ℂ_fld)
90		eqid 2758	. . . . . . . . . . . . . . . . 17 ⊢ (ℂ_fld ↾_s ℕ₀) = (ℂ_fld ↾_s ℕ₀)
91	90	submbas 18050	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ∈ (SubMnd‘ℂ_fld) → ℕ₀ = (Base‘(ℂ_fld ↾_s ℕ₀)))
92	89, 91	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ℕ₀ = (Base‘(ℂ_fld ↾_s ℕ₀))
93		cnfld0 20195	. . . . . . . . . . . . . . . . 17 ⊢ 0 = (0_g‘ℂ_fld)
94	90, 93	subm0 18051	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ∈ (SubMnd‘ℂ_fld) → 0 = (0_g‘(ℂ_fld ↾_s ℕ₀)))
95	89, 94	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 0 = (0_g‘(ℂ_fld ↾_s ℕ₀))
96		nn0ex 11945	. . . . . . . . . . . . . . . 16 ⊢ ℕ₀ ∈ V
97		cnfldadd 20176	. . . . . . . . . . . . . . . . 17 ⊢ + = (+_g‘ℂ_fld)
98	90, 97	ressplusg 16675	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ∈ V → + = (+_g‘(ℂ_fld ↾_s ℕ₀)))
99	96, 98	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ + = (+_g‘(ℂ_fld ↾_s ℕ₀))
100		cnring 20193	. . . . . . . . . . . . . . . . . 18 ⊢ ℂ_fld ∈ Ring
101		ringcmn 19407	. . . . . . . . . . . . . . . . . 18 ⊢ (ℂ_fld ∈ Ring → ℂ_fld ∈ CMnd)
102	100, 101	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ℂ_fld ∈ CMnd
103	90	submcmn 19031	. . . . . . . . . . . . . . . . 17 ⊢ ((ℂ_fld ∈ CMnd ∧ ℕ₀ ∈ (SubMnd‘ℂ_fld)) → (ℂ_fld ↾_s ℕ₀) ∈ CMnd)
104	102, 89, 103	mp2an 691	. . . . . . . . . . . . . . . 16 ⊢ (ℂ_fld ↾_s ℕ₀) ∈ CMnd
105	104	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (ℂ_fld ↾_s ℕ₀) ∈ CMnd)
106	7	ad3antrrr 729	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝐼 ∈ 𝑉)
107	5	psrbagf 20685	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} → 𝑒:𝐼⟶ℕ₀)
108	83, 107	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒:𝐼⟶ℕ₀)
109		simpllr 775	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
110	5	psrbagf 20685	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} → 𝑥:𝐼⟶ℕ₀)
111	109, 110	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑥:𝐼⟶ℕ₀)
112	111	ffnd 6503	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑥 Fn 𝐼)
113	108	ffnd 6503	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 Fn 𝐼)
114		inidm 4125	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∩ 𝐼) = 𝐼
115		eqidd 2759	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑥‘𝑖) = (𝑥‘𝑖))
116		eqidd 2759	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑒‘𝑖) = (𝑒‘𝑖))
117	112, 113, 106, 106, 114, 115, 116	offval 7418	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒) = (𝑖 ∈ 𝐼 ↦ ((𝑥‘𝑖) − (𝑒‘𝑖))))
118		simpl 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}))
119		simplr 768	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
120		breq1 5038	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = 𝑒 → (𝑐 ∘_r ≤ 𝑥 ↔ 𝑒 ∘_r ≤ 𝑥))
121	120	elrab 3604	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↔ (𝑒 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∧ 𝑒 ∘_r ≤ 𝑥))
122	121	simprbi 500	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} → 𝑒 ∘_r ≤ 𝑥)
123	119, 122	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → 𝑒 ∘_r ≤ 𝑥)
124		simpr 488	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → 𝑖 ∈ 𝐼)
125	113, 112, 106, 106, 114, 116, 115	ofrval 7421	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑒 ∘_r ≤ 𝑥 ∧ 𝑖 ∈ 𝐼) → (𝑒‘𝑖) ≤ (𝑥‘𝑖))
126	118, 123, 124, 125	syl3anc 1368	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑒‘𝑖) ≤ (𝑥‘𝑖))
127	108	ffvelrnda 6847	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑒‘𝑖) ∈ ℕ₀)
128	111	ffvelrnda 6847	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑥‘𝑖) ∈ ℕ₀)
129		nn0sub 11989	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒‘𝑖) ∈ ℕ₀ ∧ (𝑥‘𝑖) ∈ ℕ₀) → ((𝑒‘𝑖) ≤ (𝑥‘𝑖) ↔ ((𝑥‘𝑖) − (𝑒‘𝑖)) ∈ ℕ₀))
130	127, 128, 129	syl2anc 587	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → ((𝑒‘𝑖) ≤ (𝑥‘𝑖) ↔ ((𝑥‘𝑖) − (𝑒‘𝑖)) ∈ ℕ₀))
131	126, 130	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → ((𝑥‘𝑖) − (𝑒‘𝑖)) ∈ ℕ₀)
132	117, 131	fmpt3d 6876	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒):𝐼⟶ℕ₀)
133	108	ffund 6506	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → Fun 𝑒)
134		c0ex 10678	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ V
135	106, 134	jctir 524	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝐼 ∈ 𝑉 ∧ 0 ∈ V))
136		frnsuppeq 7854	. . . . . . . . . . . . . . . . . . 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 11952	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ = (ℕ₀ ∖ {0})
139	138	imaeq2i 5903	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝑒 “ ℕ) = (^◡𝑒 “ (ℕ₀ ∖ {0}))
140	137, 139	eqtr4di 2811	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 supp 0) = (^◡𝑒 “ ℕ))
141	5	psrbag 20684	. . . . . . . . . . . . . . . . . . . 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 235	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒:𝐼⟶ℕ₀ ∧ (^◡𝑒 “ ℕ) ∈ Fin))
144	143	simprd 499	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (^◡𝑒 “ ℕ) ∈ Fin)
145	140, 144	eqeltrd 2852	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 supp 0) ∈ Fin)
146	83	elexd 3430	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 ∈ V)
147		isfsupp 8875	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 ∈ V ∧ 0 ∈ V) → (𝑒 finSupp 0 ↔ (Fun 𝑒 ∧ (𝑒 supp 0) ∈ Fin)))
148	146, 134, 147	sylancl 589	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 finSupp 0 ↔ (Fun 𝑒 ∧ (𝑒 supp 0) ∈ Fin)))
149	133, 145, 148	mpbir2and 712	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 finSupp 0)
150	112, 113, 106, 106	offun 7423	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → Fun (𝑥 ∘_f − 𝑒))
151	5	psrbagfsupp 20687	. . . . . . . . . . . . . . . . . . 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 8891	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑥 supp 0) ∪ (𝑒 supp 0)) ∈ Fin)
154		0nn0 11954	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℕ₀
155	154	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 0 ∈ ℕ₀)
156		0m0e0 11799	. . . . . . . . . . . . . . . . . . 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 7882	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑥 ∘_f − 𝑒) supp 0) ⊆ ((𝑥 supp 0) ∪ (𝑒 supp 0)))
159	153, 158	ssfid 8783	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑥 ∘_f − 𝑒) supp 0) ∈ Fin)
160		ovexd 7190	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒) ∈ V)
161		isfsupp 8875	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∘_f − 𝑒) ∈ V ∧ 0 ∈ V) → ((𝑥 ∘_f − 𝑒) finSupp 0 ↔ (Fun (𝑥 ∘_f − 𝑒) ∧ ((𝑥 ∘_f − 𝑒) supp 0) ∈ Fin)))
162	160, 134, 161	sylancl 589	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑥 ∘_f − 𝑒) finSupp 0 ↔ (Fun (𝑥 ∘_f − 𝑒) ∧ ((𝑥 ∘_f − 𝑒) supp 0) ∈ Fin)))
163	150, 159, 162	mpbir2and 712	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒) finSupp 0)
164	92, 95, 99, 105, 106, 108, 132, 149, 163	gsumadd 19116	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑒 ∘_f + (𝑥 ∘_f − 𝑒))) = (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) + ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒))))
165	108	ffvelrnda 6847	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑒‘𝑏) ∈ ℕ₀)
166	165	nn0cnd 12001	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑒‘𝑏) ∈ ℂ)
167	111	ffvelrnda 6847	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑥‘𝑏) ∈ ℕ₀)
168	167	nn0cnd 12001	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑥‘𝑏) ∈ ℂ)
169	166, 168	pncan3d 11043	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → ((𝑒‘𝑏) + ((𝑥‘𝑏) − (𝑒‘𝑏))) = (𝑥‘𝑏))
170	169	mpteq2dva 5130	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑏 ∈ 𝐼 ↦ ((𝑒‘𝑏) + ((𝑥‘𝑏) − (𝑒‘𝑏)))) = (𝑏 ∈ 𝐼 ↦ (𝑥‘𝑏)))
171		fvexd 6677	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑒‘𝑏) ∈ V)
172		ovexd 7190	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → ((𝑥‘𝑏) − (𝑒‘𝑏)) ∈ V)
173	108	feqmptd 6725	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 = (𝑏 ∈ 𝐼 ↦ (𝑒‘𝑏)))
174	111	feqmptd 6725	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑥 = (𝑏 ∈ 𝐼 ↦ (𝑥‘𝑏)))
175	106, 167, 165, 174, 173	offval2 7429	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒) = (𝑏 ∈ 𝐼 ↦ ((𝑥‘𝑏) − (𝑒‘𝑏))))
176	106, 171, 172, 173, 175	offval2 7429	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 ∘_f + (𝑥 ∘_f − 𝑒)) = (𝑏 ∈ 𝐼 ↦ ((𝑒‘𝑏) + ((𝑥‘𝑏) − (𝑒‘𝑏)))))
177	170, 176, 174	3eqtr4d 2803	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 ∘_f + (𝑥 ∘_f − 𝑒)) = 𝑥)
178	177	oveq2d 7171	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑒 ∘_f + (𝑥 ∘_f − 𝑒))) = ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥))
179	164, 178	eqtr3d 2795	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) + ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒))) = ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥))
180		simplr 768	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁))
181	179, 180	eqnetrd 3018	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) + ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒))) ≠ (𝑀 + 𝑁))
182		oveq12 7164	. . . . . . . . . . . . . 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 2964	. . . . . . . . . . . 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 3045	. . . . . . . . . . 11 ⊢ ((((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀 ∨ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) ↔ ¬ (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) = 𝑀 ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) = 𝑁))
187	185, 186	sylibr 237	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀 ∨ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁))
188	62, 88, 187	mpjaodan 956	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = (0_g‘𝑅))
189	188	mpteq2dva 5130	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒)))) = (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ (0_g‘𝑅)))
190	189	oveq2d 7171	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) = (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ (0_g‘𝑅))))
191		ringmnd 19380	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
192	8, 191	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ Mnd)
193	192	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → 𝑅 ∈ Mnd)
194	44	rabex 5205	. . . . . . . 8 ⊢ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ∈ V
195	41	gsumz 18071	. . . . . . . 8 ⊢ ((𝑅 ∈ Mnd ∧ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ∈ V) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ (0_g‘𝑅))) = (0_g‘𝑅))
196	193, 194, 195	sylancl 589	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ (0_g‘𝑅))) = (0_g‘𝑅))
197	190, 196	eqtrd 2793	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) = (0_g‘𝑅))
198	197	ex 416	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) = (0_g‘𝑅)))
199	198	necon1d 2973	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → ((𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) ≠ (0_g‘𝑅) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) = (𝑀 + 𝑁)))
200	27, 199	sylbid 243	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → (((𝑃 · 𝑄)‘𝑥) ≠ (0_g‘𝑅) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) = (𝑀 + 𝑁)))
201	200	ralrimiva 3113	. 2 ⊢ (𝜑 → ∀𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} (((𝑃 · 𝑄)‘𝑥) ≠ (0_g‘𝑅) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) = (𝑀 + 𝑁)))
202	9, 12	nn0addcld 12003	. . 3 ⊢ (𝜑 → (𝑀 + 𝑁) ∈ ℕ₀)
203	1	mplring 20788	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring)
204	7, 8, 203	syl2anc 587	. . . 4 ⊢ (𝜑 → 𝑌 ∈ Ring)
205	2, 4	ringcl 19387	. . . 4 ⊢ ((𝑌 ∈ Ring ∧ 𝑃 ∈ (Base‘𝑌) ∧ 𝑄 ∈ (Base‘𝑌)) → (𝑃 · 𝑄) ∈ (Base‘𝑌))
206	204, 11, 14, 205	syl3anc 1368	. . 3 ⊢ (𝜑 → (𝑃 · 𝑄) ∈ (Base‘𝑌))
207	6, 1, 2, 41, 5, 7, 8, 202, 206	ismhp3 20891	. 2 ⊢ (𝜑 → ((𝑃 · 𝑄) ∈ (𝐻‘(𝑀 + 𝑁)) ↔ ∀𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} (((𝑃 · 𝑄)‘𝑥) ≠ (0_g‘𝑅) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) = (𝑀 + 𝑁))))
208	201, 207	mpbird 260	1 ⊢ (𝜑 → (𝑃 · 𝑄) ∈ (𝐻‘(𝑀 + 𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 844 = wceq 1538 ∈ wcel 2111 ≠ wne 2951 ∀wral 3070 {crab 3074 Vcvv 3409 ∖ cdif 3857 ∪ cun 3858 {csn 4525 class class class wbr 5035 ↦ cmpt 5115 ^◡ccnv 5526 “ cima 5530 Fun wfun 6333 ⟶wf 6335 ‘cfv 6339 (class class class)co 7155 ∘_f cof 7408 ∘_r cofr 7409 supp csupp 7840 ↑_m cmap 8421 Fincfn 8532 finSupp cfsupp 8871 0cc0 10580 + caddc 10583 ≤ cle 10719 − cmin 10913 ℕcn 11679 ℕ₀cn0 11939 Basecbs 16546 ↾_s cress 16547 +_gcplusg 16628 ._rcmulr 16629 0_gc0g 16776 Σ_g cgsu 16777 Mndcmnd 17982 SubMndcsubmnd 18026 CMndccmn 18978 Ringcrg 19370 ℂ_fldccnfld 20171 mPoly cmpl 20673 mHomP cmhp 20877

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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5159 ax-sep 5172 ax-nul 5179 ax-pow 5237 ax-pr 5301 ax-un 7464 ax-cnex 10636 ax-resscn 10637 ax-1cn 10638 ax-icn 10639 ax-addcl 10640 ax-addrcl 10641 ax-mulcl 10642 ax-mulrcl 10643 ax-mulcom 10644 ax-addass 10645 ax-mulass 10646 ax-distr 10647 ax-i2m1 10648 ax-1ne0 10649 ax-1rid 10650 ax-rnegex 10651 ax-rrecex 10652 ax-cnre 10653 ax-pre-lttri 10654 ax-pre-lttrn 10655 ax-pre-ltadd 10656 ax-pre-mulgt0 10657 ax-addf 10659 ax-mulf 10660

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3699 df-csb 3808 df-dif 3863 df-un 3865 df-in 3867 df-ss 3877 df-pss 3879 df-nul 4228 df-if 4424 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4802 df-int 4842 df-iun 4888 df-iin 4889 df-br 5036 df-opab 5098 df-mpt 5116 df-tr 5142 df-id 5433 df-eprel 5438 df-po 5446 df-so 5447 df-fr 5486 df-se 5487 df-we 5488 df-xp 5533 df-rel 5534 df-cnv 5535 df-co 5536 df-dm 5537 df-rn 5538 df-res 5539 df-ima 5540 df-pred 6130 df-ord 6176 df-on 6177 df-lim 6178 df-suc 6179 df-iota 6298 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 df-fv 6347 df-isom 6348 df-riota 7113 df-ov 7158 df-oprab 7159 df-mpo 7160 df-of 7410 df-ofr 7411 df-om 7585 df-1st 7698 df-2nd 7699 df-supp 7841 df-wrecs 7962 df-recs 8023 df-rdg 8061 df-1o 8117 df-er 8304 df-map 8423 df-pm 8424 df-ixp 8485 df-en 8533 df-dom 8534 df-sdom 8535 df-fin 8536 df-fsupp 8872 df-oi 9012 df-card 9406 df-pnf 10720 df-mnf 10721 df-xr 10722 df-ltxr 10723 df-le 10724 df-sub 10915 df-neg 10916 df-nn 11680 df-2 11742 df-3 11743 df-4 11744 df-5 11745 df-6 11746 df-7 11747 df-8 11748 df-9 11749 df-n0 11940 df-z 12026 df-dec 12143 df-uz 12288 df-fz 12945 df-fzo 13088 df-seq 13424 df-hash 13746 df-struct 16548 df-ndx 16549 df-slot 16550 df-base 16552 df-sets 16553 df-ress 16554 df-plusg 16641 df-mulr 16642 df-starv 16643 df-sca 16644 df-vsca 16645 df-tset 16647 df-ple 16648 df-ds 16650 df-unif 16651 df-0g 16778 df-gsum 16779 df-mre 16920 df-mrc 16921 df-acs 16923 df-mgm 17923 df-sgrp 17972 df-mnd 17983 df-mhm 18027 df-submnd 18028 df-grp 18177 df-minusg 18178 df-mulg 18297 df-subg 18348 df-ghm 18428 df-cntz 18519 df-cmn 18980 df-abl 18981 df-mgp 19313 df-ur 19325 df-ring 19372 df-cring 19373 df-subrg 19606 df-cnfld 20172 df-psr 20676 df-mpl 20678 df-mhp 20881

This theorem is referenced by: mhppwdeg 20898

W3C validator