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 21249

Description: A product of homogeneous polynomials is a homogeneous polynomial whose degree is the sum of the degrees of the factors. Compare mdegmulle2 25149 (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 2738	. . . . . . . 8 ⊢ (Base‘𝑌) = (Base‘𝑌)
3		eqid 2738	. . . . . . . 8 ⊢ (._r‘𝑅) = (._r‘𝑅)
4		mhpmulcl.t	. . . . . . . 8 ⊢ · = (._r‘𝑌)
5		eqid 2738	. . . . . . . 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 21244	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ (Base‘𝑌))
12		mhpmulcl.n	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
13		mhpmulcl.q	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (𝐻‘𝑁))
14	6, 1, 2, 7, 8, 12, 13	mhpmpl 21244	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ (Base‘𝑌))
15	1, 2, 3, 4, 5, 11, 14	mplmul 21125	. . . . . . 7 ⊢ (𝜑 → (𝑃 · 𝑄) = (𝑑 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ↦ (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒)))))))
16	15	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → (𝑃 · 𝑄) = (𝑑 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ↦ (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒)))))))
17		breq2 5074	. . . . . . . . . 10 ⊢ (𝑑 = 𝑥 → (𝑐 ∘_r ≤ 𝑑 ↔ 𝑐 ∘_r ≤ 𝑥))
18	17	rabbidv 3404	. . . . . . . . 9 ⊢ (𝑑 = 𝑥 → {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
19		fvoveq1 7278	. . . . . . . . . 10 ⊢ (𝑑 = 𝑥 → (𝑄‘(𝑑 ∘_f − 𝑒)) = (𝑄‘(𝑥 ∘_f − 𝑒)))
20	19	oveq2d 7271	. . . . . . . . 9 ⊢ (𝑑 = 𝑥 → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒))) = ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))
21	18, 20	mpteq12dv 5161	. . . . . . . 8 ⊢ (𝑑 = 𝑥 → (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒)))) = (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒)))))
22	21	oveq2d 7271	. . . . . . 7 ⊢ (𝑑 = 𝑥 → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒))))) = (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))))
23	22	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑑 = 𝑥) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒))))) = (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))))
24		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
25		ovexd 7290	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) ∈ V)
26	16, 23, 24, 25	fvmptd 6864	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → ((𝑃 · 𝑄)‘𝑥) = (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))))
27	26	neeq1d 3002	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → (((𝑃 · 𝑄)‘𝑥) ≠ (0_g‘𝑅) ↔ (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) ≠ (0_g‘𝑅)))
28		simp-4l 779	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝜑)
29		oveq2 7263	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑒 → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒))
30	29	eqeq1d 2740	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑒 → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀 ↔ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) = 𝑀))
31	30	necon3bbid 2980	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑒 → (¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀 ↔ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀))
32		simplr 765	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
33		elrabi 3611	. . . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀)
36	31, 34, 35	elrabd 3619	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀})
37		notrab 4242	. . . . . . . . . . . . . 14 ⊢ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀}) = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀}
38	36, 37	eleqtrrdi 2850	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑒 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀}))
39		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑅) = (Base‘𝑅)
40	1, 39, 2, 5, 11	mplelf 21114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑅))
41		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
42	6, 41, 5, 7, 8, 9, 10	mhpdeg 21245	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 supp (0_g‘𝑅)) ⊆ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀})
43		ovex 7288	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ↑_m 𝐼) ∈ V
44	43	rabex 5251	. . . . . . . . . . . . . . 15 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∈ V
45	44	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∈ V)
46		fvexd 6771	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝑅) ∈ V)
47	40, 42, 45, 46	suppssr 7983	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑒 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀})) → (𝑃‘𝑒) = (0_g‘𝑅))
48	28, 38, 47	syl2anc 583	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → (𝑃‘𝑒) = (0_g‘𝑅))
49	48	oveq1d 7270	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = ((0_g‘𝑅)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))
50	8	ad4antr 728	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑅 ∈ Ring)
51	14	ad4antr 728	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑄 ∈ (Base‘𝑌))
52	1, 39, 2, 5, 51	mplelf 21114	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑄:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑅))
53		simp-4r 780	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
54		eqid 2738	. . . . . . . . . . . . . . . 16 ⊢ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}
55	5, 54	psrbagconcl 21047	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒) ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
56	53, 32, 55	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → (𝑥 ∘_f − 𝑒) ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
57		elrabi 3611	. . . . . . . . . . . . . 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 6944	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → (𝑄‘(𝑥 ∘_f − 𝑒)) ∈ (Base‘𝑅))
60	39, 3, 41	ringlz 19741	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ (𝑄‘(𝑥 ∘_f − 𝑒)) ∈ (Base‘𝑅)) → ((0_g‘𝑅)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = (0_g‘𝑅))
61	50, 59, 60	syl2anc 583	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → ((0_g‘𝑅)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = (0_g‘𝑅))
62	49, 61	eqtrd 2778	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = (0_g‘𝑅))
63		simp-4l 779	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝜑)
64		oveq2 7263	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑥 ∘_f − 𝑒) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)))
65	64	eqeq1d 2740	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑥 ∘_f − 𝑒) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁 ↔ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) = 𝑁))
66	65	necon3bbid 2980	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (𝑥 ∘_f − 𝑒) → (¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁 ↔ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁))
67		simp-4r 780	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
68		simplr 765	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
69	67, 68, 55	syl2anc 583	. . . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁)
72	66, 70, 71	elrabd 3619	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → (𝑥 ∘_f − 𝑒) ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁})
73		notrab 4242	. . . . . . . . . . . . . 14 ⊢ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁}) = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁}
74	72, 73	eleqtrrdi 2850	. . . . . . . . . . . . 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 21114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑄:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑅))
76	6, 41, 5, 7, 8, 12, 13	mhpdeg 21245	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑄 supp (0_g‘𝑅)) ⊆ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁})
77	75, 76, 45, 46	suppssr 7983	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∘_f − 𝑒) ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁})) → (𝑄‘(𝑥 ∘_f − 𝑒)) = (0_g‘𝑅))
78	63, 74, 77	syl2anc 583	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → (𝑄‘(𝑥 ∘_f − 𝑒)) = (0_g‘𝑅))
79	78	oveq2d 7271	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = ((𝑃‘𝑒)(._r‘𝑅)(0_g‘𝑅)))
80	8	ad4antr 728	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝑅 ∈ Ring)
81	11	ad4antr 728	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝑃 ∈ (Base‘𝑌))
82	1, 39, 2, 5, 81	mplelf 21114	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝑃:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑅))
83	33	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
84	83	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → 𝑒 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
85	82, 84	ffvelrnd 6944	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → (𝑃‘𝑒) ∈ (Base‘𝑅))
86	39, 3, 41	ringrz 19742	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ (𝑃‘𝑒) ∈ (Base‘𝑅)) → ((𝑃‘𝑒)(._r‘𝑅)(0_g‘𝑅)) = (0_g‘𝑅))
87	80, 85, 86	syl2anc 583	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → ((𝑃‘𝑒)(._r‘𝑅)(0_g‘𝑅)) = (0_g‘𝑅))
88	79, 87	eqtrd 2778	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = (0_g‘𝑅))
89		nn0subm 20565	. . . . . . . . . . . . . . . 16 ⊢ ℕ₀ ∈ (SubMnd‘ℂ_fld)
90		eqid 2738	. . . . . . . . . . . . . . . . 17 ⊢ (ℂ_fld ↾_s ℕ₀) = (ℂ_fld ↾_s ℕ₀)
91	90	submbas 18368	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ∈ (SubMnd‘ℂ_fld) → ℕ₀ = (Base‘(ℂ_fld ↾_s ℕ₀)))
92	89, 91	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ℕ₀ = (Base‘(ℂ_fld ↾_s ℕ₀))
93		cnfld0 20534	. . . . . . . . . . . . . . . . 17 ⊢ 0 = (0_g‘ℂ_fld)
94	90, 93	subm0 18369	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ∈ (SubMnd‘ℂ_fld) → 0 = (0_g‘(ℂ_fld ↾_s ℕ₀)))
95	89, 94	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 0 = (0_g‘(ℂ_fld ↾_s ℕ₀))
96		nn0ex 12169	. . . . . . . . . . . . . . . 16 ⊢ ℕ₀ ∈ V
97		cnfldadd 20515	. . . . . . . . . . . . . . . . 17 ⊢ + = (+_g‘ℂ_fld)
98	90, 97	ressplusg 16926	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ∈ V → + = (+_g‘(ℂ_fld ↾_s ℕ₀)))
99	96, 98	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ + = (+_g‘(ℂ_fld ↾_s ℕ₀))
100		cnring 20532	. . . . . . . . . . . . . . . . . 18 ⊢ ℂ_fld ∈ Ring
101		ringcmn 19735	. . . . . . . . . . . . . . . . . 18 ⊢ (ℂ_fld ∈ Ring → ℂ_fld ∈ CMnd)
102	100, 101	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ℂ_fld ∈ CMnd
103	90	submcmn 19354	. . . . . . . . . . . . . . . . 17 ⊢ ((ℂ_fld ∈ CMnd ∧ ℕ₀ ∈ (SubMnd‘ℂ_fld)) → (ℂ_fld ↾_s ℕ₀) ∈ CMnd)
104	102, 89, 103	mp2an 688	. . . . . . . . . . . . . . . 16 ⊢ (ℂ_fld ↾_s ℕ₀) ∈ CMnd
105	104	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (ℂ_fld ↾_s ℕ₀) ∈ CMnd)
106	7	ad3antrrr 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝐼 ∈ 𝑉)
107	5	psrbagf 21031	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} → 𝑒:𝐼⟶ℕ₀)
108	83, 107	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒:𝐼⟶ℕ₀)
109		simpllr 772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin})
110	5	psrbagf 21031	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} → 𝑥:𝐼⟶ℕ₀)
111	109, 110	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑥:𝐼⟶ℕ₀)
112	111	ffnd 6585	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑥 Fn 𝐼)
113	108	ffnd 6585	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 Fn 𝐼)
114		inidm 4149	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∩ 𝐼) = 𝐼
115		eqidd 2739	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑥‘𝑖) = (𝑥‘𝑖))
116		eqidd 2739	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑒‘𝑖) = (𝑒‘𝑖))
117	112, 113, 106, 106, 114, 115, 116	offval 7520	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒) = (𝑖 ∈ 𝐼 ↦ ((𝑥‘𝑖) − (𝑒‘𝑖))))
118		simpl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}))
119		simplr 765	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
120		breq1 5073	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = 𝑒 → (𝑐 ∘_r ≤ 𝑥 ↔ 𝑒 ∘_r ≤ 𝑥))
121	120	elrab 3617	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↔ (𝑒 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∧ 𝑒 ∘_r ≤ 𝑥))
122	121	simprbi 496	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} → 𝑒 ∘_r ≤ 𝑥)
123	119, 122	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → 𝑒 ∘_r ≤ 𝑥)
124		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → 𝑖 ∈ 𝐼)
125	113, 112, 106, 106, 114, 116, 115	ofrval 7523	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑒 ∘_r ≤ 𝑥 ∧ 𝑖 ∈ 𝐼) → (𝑒‘𝑖) ≤ (𝑥‘𝑖))
126	118, 123, 124, 125	syl3anc 1369	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑒‘𝑖) ≤ (𝑥‘𝑖))
127	108	ffvelrnda 6943	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑒‘𝑖) ∈ ℕ₀)
128	111	ffvelrnda 6943	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑥‘𝑖) ∈ ℕ₀)
129		nn0sub 12213	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒‘𝑖) ∈ ℕ₀ ∧ (𝑥‘𝑖) ∈ ℕ₀) → ((𝑒‘𝑖) ≤ (𝑥‘𝑖) ↔ ((𝑥‘𝑖) − (𝑒‘𝑖)) ∈ ℕ₀))
130	127, 128, 129	syl2anc 583	. . . . . . . . . . . . . . . . 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 6972	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒):𝐼⟶ℕ₀)
133	108	ffund 6588	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → Fun 𝑒)
134		c0ex 10900	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ V
135	106, 134	jctir 520	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝐼 ∈ 𝑉 ∧ 0 ∈ V))
136		frnsuppeq 7962	. . . . . . . . . . . . . . . . . . 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 12176	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ = (ℕ₀ ∖ {0})
139	138	imaeq2i 5956	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝑒 “ ℕ) = (^◡𝑒 “ (ℕ₀ ∖ {0}))
140	137, 139	eqtr4di 2797	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 supp 0) = (^◡𝑒 “ ℕ))
141	5	psrbag 21030	. . . . . . . . . . . . . . . . . . . 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 495	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (^◡𝑒 “ ℕ) ∈ Fin)
145	140, 144	eqeltrd 2839	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 supp 0) ∈ Fin)
146	83	elexd 3442	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 ∈ V)
147		isfsupp 9062	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 ∈ V ∧ 0 ∈ V) → (𝑒 finSupp 0 ↔ (Fun 𝑒 ∧ (𝑒 supp 0) ∈ Fin)))
148	146, 134, 147	sylancl 585	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 finSupp 0 ↔ (Fun 𝑒 ∧ (𝑒 supp 0) ∈ Fin)))
149	133, 145, 148	mpbir2and 709	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 finSupp 0)
150	112, 113, 106, 106	offun 7525	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → Fun (𝑥 ∘_f − 𝑒))
151	5	psrbagfsupp 21033	. . . . . . . . . . . . . . . . . . 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 9078	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑥 supp 0) ∪ (𝑒 supp 0)) ∈ Fin)
154		0nn0 12178	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℕ₀
155	154	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 0 ∈ ℕ₀)
156		0m0e0 12023	. . . . . . . . . . . . . . . . . . 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 7990	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑥 ∘_f − 𝑒) supp 0) ⊆ ((𝑥 supp 0) ∪ (𝑒 supp 0)))
159	153, 158	ssfid 8971	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑥 ∘_f − 𝑒) supp 0) ∈ Fin)
160		ovexd 7290	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒) ∈ V)
161		isfsupp 9062	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∘_f − 𝑒) ∈ V ∧ 0 ∈ V) → ((𝑥 ∘_f − 𝑒) finSupp 0 ↔ (Fun (𝑥 ∘_f − 𝑒) ∧ ((𝑥 ∘_f − 𝑒) supp 0) ∈ Fin)))
162	160, 134, 161	sylancl 585	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑥 ∘_f − 𝑒) finSupp 0 ↔ (Fun (𝑥 ∘_f − 𝑒) ∧ ((𝑥 ∘_f − 𝑒) supp 0) ∈ Fin)))
163	150, 159, 162	mpbir2and 709	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒) finSupp 0)
164	92, 95, 99, 105, 106, 108, 132, 149, 163	gsumadd 19439	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑒 ∘_f + (𝑥 ∘_f − 𝑒))) = (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) + ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒))))
165	108	ffvelrnda 6943	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑒‘𝑏) ∈ ℕ₀)
166	165	nn0cnd 12225	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑒‘𝑏) ∈ ℂ)
167	111	ffvelrnda 6943	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑥‘𝑏) ∈ ℕ₀)
168	167	nn0cnd 12225	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑥‘𝑏) ∈ ℂ)
169	166, 168	pncan3d 11265	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → ((𝑒‘𝑏) + ((𝑥‘𝑏) − (𝑒‘𝑏))) = (𝑥‘𝑏))
170	169	mpteq2dva 5170	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑏 ∈ 𝐼 ↦ ((𝑒‘𝑏) + ((𝑥‘𝑏) − (𝑒‘𝑏)))) = (𝑏 ∈ 𝐼 ↦ (𝑥‘𝑏)))
171		fvexd 6771	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑒‘𝑏) ∈ V)
172		ovexd 7290	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → ((𝑥‘𝑏) − (𝑒‘𝑏)) ∈ V)
173	108	feqmptd 6819	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 = (𝑏 ∈ 𝐼 ↦ (𝑒‘𝑏)))
174	111	feqmptd 6819	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑥 = (𝑏 ∈ 𝐼 ↦ (𝑥‘𝑏)))
175	106, 167, 165, 174, 173	offval2 7531	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒) = (𝑏 ∈ 𝐼 ↦ ((𝑥‘𝑏) − (𝑒‘𝑏))))
176	106, 171, 172, 173, 175	offval2 7531	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 ∘_f + (𝑥 ∘_f − 𝑒)) = (𝑏 ∈ 𝐼 ↦ ((𝑒‘𝑏) + ((𝑥‘𝑏) − (𝑒‘𝑏)))))
177	170, 176, 174	3eqtr4d 2788	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 ∘_f + (𝑥 ∘_f − 𝑒)) = 𝑥)
178	177	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑒 ∘_f + (𝑥 ∘_f − 𝑒))) = ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥))
179	164, 178	eqtr3d 2780	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) + ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒))) = ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥))
180		simplr 765	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁))
181	179, 180	eqnetrd 3010	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) + ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒))) ≠ (𝑀 + 𝑁))
182		oveq12 7264	. . . . . . . . . . . . . 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 2955	. . . . . . . . . . . 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 3038	. . . . . . . . . . 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 955	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = (0_g‘𝑅))
189	188	mpteq2dva 5170	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒)))) = (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ (0_g‘𝑅)))
190	189	oveq2d 7271	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) = (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ (0_g‘𝑅))))
191		ringmnd 19708	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
192	8, 191	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ Mnd)
193	192	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → 𝑅 ∈ Mnd)
194	44	rabex 5251	. . . . . . . 8 ⊢ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ∈ V
195	41	gsumz 18389	. . . . . . . 8 ⊢ ((𝑅 ∈ Mnd ∧ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ∈ V) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ (0_g‘𝑅))) = (0_g‘𝑅))
196	193, 194, 195	sylancl 585	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ (0_g‘𝑅))) = (0_g‘𝑅))
197	190, 196	eqtrd 2778	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) = (0_g‘𝑅))
198	197	ex 412	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) = (0_g‘𝑅)))
199	198	necon1d 2964	. . . 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 3107	. 2 ⊢ (𝜑 → ∀𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} (((𝑃 · 𝑄)‘𝑥) ≠ (0_g‘𝑅) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) = (𝑀 + 𝑁)))
202	9, 12	nn0addcld 12227	. . 3 ⊢ (𝜑 → (𝑀 + 𝑁) ∈ ℕ₀)
203	1	mplring 21134	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring)
204	7, 8, 203	syl2anc 583	. . . 4 ⊢ (𝜑 → 𝑌 ∈ Ring)
205	2, 4	ringcl 19715	. . . 4 ⊢ ((𝑌 ∈ Ring ∧ 𝑃 ∈ (Base‘𝑌) ∧ 𝑄 ∈ (Base‘𝑌)) → (𝑃 · 𝑄) ∈ (Base‘𝑌))
206	204, 11, 14, 205	syl3anc 1369	. . 3 ⊢ (𝜑 → (𝑃 · 𝑄) ∈ (Base‘𝑌))
207	6, 1, 2, 41, 5, 7, 8, 202, 206	ismhp3 21243	. 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 395 ∨ wo 843 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 {crab 3067 Vcvv 3422 ∖ cdif 3880 ∪ cun 3881 {csn 4558 class class class wbr 5070 ↦ cmpt 5153 ^◡ccnv 5579 “ cima 5583 Fun wfun 6412 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 ∘_f cof 7509 ∘_r cofr 7510 supp csupp 7948 ↑_m cmap 8573 Fincfn 8691 finSupp cfsupp 9058 0cc0 10802 + caddc 10805 ≤ cle 10941 − cmin 11135 ℕcn 11903 ℕ₀cn0 12163 Basecbs 16840 ↾_s cress 16867 +_gcplusg 16888 ._rcmulr 16889 0_gc0g 17067 Σ_g cgsu 17068 Mndcmnd 18300 SubMndcsubmnd 18344 CMndccmn 19301 Ringcrg 19698 ℂ_fldccnfld 20510 mPoly cmpl 21019 mHomP cmhp 21229

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-addf 10881 ax-mulf 10882

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-iin 4924 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-of 7511 df-ofr 7512 df-om 7688 df-1st 7804 df-2nd 7805 df-supp 7949 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-er 8456 df-map 8575 df-pm 8576 df-ixp 8644 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-fsupp 9059 df-oi 9199 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-7 11971 df-8 11972 df-9 11973 df-n0 12164 df-z 12250 df-dec 12367 df-uz 12512 df-fz 13169 df-fzo 13312 df-seq 13650 df-hash 13973 df-struct 16776 df-sets 16793 df-slot 16811 df-ndx 16823 df-base 16841 df-ress 16868 df-plusg 16901 df-mulr 16902 df-starv 16903 df-sca 16904 df-vsca 16905 df-tset 16907 df-ple 16908 df-ds 16910 df-unif 16911 df-0g 17069 df-gsum 17070 df-mre 17212 df-mrc 17213 df-acs 17215 df-mgm 18241 df-sgrp 18290 df-mnd 18301 df-mhm 18345 df-submnd 18346 df-grp 18495 df-minusg 18496 df-mulg 18616 df-subg 18667 df-ghm 18747 df-cntz 18838 df-cmn 19303 df-abl 19304 df-mgp 19636 df-ur 19653 df-ring 19700 df-cring 19701 df-subrg 19937 df-cnfld 20511 df-psr 21022 df-mpl 21024 df-mhp 21233

This theorem is referenced by: mhppwdeg 21250

W3C validator