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 21683

Description: A product of homogeneous polynomials is a homogeneous polynomial whose degree is the sum of the degrees of the factors. Compare mdegmulle2 25588 (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 2732	. . . . . . . 8 ⊢ (Base‘𝑌) = (Base‘𝑌)
3		eqid 2732	. . . . . . . 8 ⊢ (._r‘𝑅) = (._r‘𝑅)
4		mhpmulcl.t	. . . . . . . 8 ⊢ · = (._r‘𝑌)
5		eqid 2732	. . . . . . . 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 21678	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ (Base‘𝑌))
12		mhpmulcl.n	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
13		mhpmulcl.q	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (𝐻‘𝑁))
14	6, 1, 2, 7, 8, 12, 13	mhpmpl 21678	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ (Base‘𝑌))
15	1, 2, 3, 4, 5, 11, 14	mplmul 21561	. . . . . . 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 5151	. . . . . . . . . 10 ⊢ (𝑑 = 𝑥 → (𝑐 ∘_r ≤ 𝑑 ↔ 𝑐 ∘_r ≤ 𝑥))
18	17	rabbidv 3440	. . . . . . . . 9 ⊢ (𝑑 = 𝑥 → {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥})
19		fvoveq1 7428	. . . . . . . . . 10 ⊢ (𝑑 = 𝑥 → (𝑄‘(𝑑 ∘_f − 𝑒)) = (𝑄‘(𝑥 ∘_f − 𝑒)))
20	19	oveq2d 7421	. . . . . . . . 9 ⊢ (𝑑 = 𝑥 → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒))) = ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))
21	18, 20	mpteq12dv 5238	. . . . . . . 8 ⊢ (𝑑 = 𝑥 → (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑑} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑑 ∘_f − 𝑒)))) = (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒)))))
22	21	oveq2d 7421	. . . . . . 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 7440	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) ∈ V)
26	16, 23, 24, 25	fvmptd 7002	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) → ((𝑃 · 𝑄)‘𝑥) = (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))))
27	26	neeq1d 3000	. . . 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 7413	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑒 → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒))
30	29	eqeq1d 2734	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑒 → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀 ↔ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) = 𝑀))
31	30	necon3bbid 2978	. . . . . . . . . . . . . . 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 3676	. . . . . . . . . . . . . . . 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 3684	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀})
37		notrab 4310	. . . . . . . . . . . . . 14 ⊢ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀}) = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀}
38	36, 37	eleqtrrdi 2844	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → 𝑒 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀}))
39		eqid 2732	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑅) = (Base‘𝑅)
40	1, 39, 2, 5, 11	mplelf 21548	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑅))
41		eqid 2732	. . . . . . . . . . . . . . 15 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
42	6, 41, 5, 7, 8, 9, 10	mhpdeg 21679	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 supp (0_g‘𝑅)) ⊆ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑀})
43		ovex 7438	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ↑_m 𝐼) ∈ V
44	43	rabex 5331	. . . . . . . . . . . . . . 15 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∈ V
45	44	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∈ V)
46		fvexd 6903	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝑅) ∈ V)
47	40, 42, 45, 46	suppssr 8177	. . . . . . . . . . . . 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 7420	. . . . . . . . . . 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 21548	. . . . . . . . . . . . 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 2732	. . . . . . . . . . . . . . . 16 ⊢ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}
55	5, 54	psrbagconcl 21478	. . . . . . . . . . . . . . 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 3676	. . . . . . . . . . . . . 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 7084	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) ≠ 𝑀) → (𝑄‘(𝑥 ∘_f − 𝑒)) ∈ (Base‘𝑅))
60	39, 3, 41	ringlz 20100	. . . . . . . . . . . 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 2772	. . . . . . . . . 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 7413	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑥 ∘_f − 𝑒) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)))
65	64	eqeq1d 2734	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑥 ∘_f − 𝑒) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁 ↔ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) = 𝑁))
66	65	necon3bbid 2978	. . . . . . . . . . . . . . 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 3684	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → (𝑥 ∘_f − 𝑒) ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁})
73		notrab 4310	. . . . . . . . . . . . . 14 ⊢ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∖ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁}) = {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ¬ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁}
74	72, 73	eleqtrrdi 2844	. . . . . . . . . . . . 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 21548	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑄:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑅))
76	6, 41, 5, 7, 8, 12, 13	mhpdeg 21679	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑄 supp (0_g‘𝑅)) ⊆ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑐) = 𝑁})
77	75, 76, 45, 46	suppssr 8177	. . . . . . . . . . . . 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 7421	. . . . . . . . . . 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 21548	. . . . . . . . . . . . 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 7084	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → (𝑃‘𝑒) ∈ (Base‘𝑅))
86	39, 3, 41	ringrz 20101	. . . . . . . . . . . 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 2772	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒)) ≠ 𝑁) → ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))) = (0_g‘𝑅))
89		nn0subm 20992	. . . . . . . . . . . . . . . 16 ⊢ ℕ₀ ∈ (SubMnd‘ℂ_fld)
90		eqid 2732	. . . . . . . . . . . . . . . . 17 ⊢ (ℂ_fld ↾_s ℕ₀) = (ℂ_fld ↾_s ℕ₀)
91	90	submbas 18691	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ∈ (SubMnd‘ℂ_fld) → ℕ₀ = (Base‘(ℂ_fld ↾_s ℕ₀)))
92	89, 91	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ℕ₀ = (Base‘(ℂ_fld ↾_s ℕ₀))
93		cnfld0 20961	. . . . . . . . . . . . . . . . 17 ⊢ 0 = (0_g‘ℂ_fld)
94	90, 93	subm0 18692	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ∈ (SubMnd‘ℂ_fld) → 0 = (0_g‘(ℂ_fld ↾_s ℕ₀)))
95	89, 94	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 0 = (0_g‘(ℂ_fld ↾_s ℕ₀))
96		nn0ex 12474	. . . . . . . . . . . . . . . 16 ⊢ ℕ₀ ∈ V
97		cnfldadd 20941	. . . . . . . . . . . . . . . . 17 ⊢ + = (+_g‘ℂ_fld)
98	90, 97	ressplusg 17231	. . . . . . . . . . . . . . . 16 ⊢ (ℕ₀ ∈ V → + = (+_g‘(ℂ_fld ↾_s ℕ₀)))
99	96, 98	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ + = (+_g‘(ℂ_fld ↾_s ℕ₀))
100		cnring 20959	. . . . . . . . . . . . . . . . . 18 ⊢ ℂ_fld ∈ Ring
101		ringcmn 20092	. . . . . . . . . . . . . . . . . 18 ⊢ (ℂ_fld ∈ Ring → ℂ_fld ∈ CMnd)
102	100, 101	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ℂ_fld ∈ CMnd
103	90	submcmn 19700	. . . . . . . . . . . . . . . . 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 21462	. . . . . . . . . . . . . . . 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 21462	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} → 𝑥:𝐼⟶ℕ₀)
111	109, 110	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑥:𝐼⟶ℕ₀)
112	111	ffnd 6715	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑥 Fn 𝐼)
113	108	ffnd 6715	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 Fn 𝐼)
114		inidm 4217	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∩ 𝐼) = 𝐼
115		eqidd 2733	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑥‘𝑖) = (𝑥‘𝑖))
116		eqidd 2733	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑒‘𝑖) = (𝑒‘𝑖))
117	112, 113, 106, 106, 114, 115, 116	offval 7675	. . . . . . . . . . . . . . . 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 5150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = 𝑒 → (𝑐 ∘_r ≤ 𝑥 ↔ 𝑒 ∘_r ≤ 𝑥))
121	120	elrab 3682	. . . . . . . . . . . . . . . . . . . 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 7678	. . . . . . . . . . . . . . . . . 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 7083	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑒‘𝑖) ∈ ℕ₀)
128	111	ffvelcdmda 7083	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑖 ∈ 𝐼) → (𝑥‘𝑖) ∈ ℕ₀)
129		nn0sub 12518	. . . . . . . . . . . . . . . . . 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 7112	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒):𝐼⟶ℕ₀)
133	108	ffund 6718	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → Fun 𝑒)
134		c0ex 11204	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ V
135	106, 134	jctir 521	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝐼 ∈ 𝑉 ∧ 0 ∈ V))
136		fsuppeq 8156	. . . . . . . . . . . . . . . . . . 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 12481	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ = (ℕ₀ ∖ {0})
139	138	imaeq2i 6055	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝑒 “ ℕ) = (^◡𝑒 “ (ℕ₀ ∖ {0}))
140	137, 139	eqtr4di 2790	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 supp 0) = (^◡𝑒 “ ℕ))
141	5	psrbag 21461	. . . . . . . . . . . . . . . . . . . 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 2833	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 supp 0) ∈ Fin)
146	83	elexd 3494	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 ∈ V)
147		isfsupp 9361	. . . . . . . . . . . . . . . . 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 7680	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → Fun (𝑥 ∘_f − 𝑒))
151	5	psrbagfsupp 21464	. . . . . . . . . . . . . . . . . . 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 9379	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑥 supp 0) ∪ (𝑒 supp 0)) ∈ Fin)
154		0nn0 12483	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℕ₀
155	154	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 0 ∈ ℕ₀)
156		0m0e0 12328	. . . . . . . . . . . . . . . . . . 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 8184	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑥 ∘_f − 𝑒) supp 0) ⊆ ((𝑥 supp 0) ∪ (𝑒 supp 0)))
159	153, 158	ssfid 9263	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((𝑥 ∘_f − 𝑒) supp 0) ∈ Fin)
160		ovexd 7440	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒) ∈ V)
161		isfsupp 9361	. . . . . . . . . . . . . . . . 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 19785	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑒 ∘_f + (𝑥 ∘_f − 𝑒))) = (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) + ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒))))
165	108	ffvelcdmda 7083	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑒‘𝑏) ∈ ℕ₀)
166	165	nn0cnd 12530	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑒‘𝑏) ∈ ℂ)
167	111	ffvelcdmda 7083	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑥‘𝑏) ∈ ℕ₀)
168	167	nn0cnd 12530	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑥‘𝑏) ∈ ℂ)
169	166, 168	pncan3d 11570	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → ((𝑒‘𝑏) + ((𝑥‘𝑏) − (𝑒‘𝑏))) = (𝑥‘𝑏))
170	169	mpteq2dva 5247	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑏 ∈ 𝐼 ↦ ((𝑒‘𝑏) + ((𝑥‘𝑏) − (𝑒‘𝑏)))) = (𝑏 ∈ 𝐼 ↦ (𝑥‘𝑏)))
171		fvexd 6903	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → (𝑒‘𝑏) ∈ V)
172		ovexd 7440	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) ∧ 𝑏 ∈ 𝐼) → ((𝑥‘𝑏) − (𝑒‘𝑏)) ∈ V)
173	108	feqmptd 6957	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑒 = (𝑏 ∈ 𝐼 ↦ (𝑒‘𝑏)))
174	111	feqmptd 6957	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → 𝑥 = (𝑏 ∈ 𝐼 ↦ (𝑥‘𝑏)))
175	106, 167, 165, 174, 173	offval2 7686	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑒) = (𝑏 ∈ 𝐼 ↦ ((𝑥‘𝑏) − (𝑒‘𝑏))))
176	106, 171, 172, 173, 175	offval2 7686	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 ∘_f + (𝑥 ∘_f − 𝑒)) = (𝑏 ∈ 𝐼 ↦ ((𝑒‘𝑏) + ((𝑥‘𝑏) − (𝑒‘𝑏)))))
177	170, 176, 174	3eqtr4d 2782	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (𝑒 ∘_f + (𝑥 ∘_f − 𝑒)) = 𝑥)
178	177	oveq2d 7421	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑒 ∘_f + (𝑥 ∘_f − 𝑒))) = ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥))
179	164, 178	eqtr3d 2774	. . . . . . . . . . . . 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 3008	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥}) → (((ℂ_fld ↾_s ℕ₀) Σ_g 𝑒) + ((ℂ_fld ↾_s ℕ₀) Σ_g (𝑥 ∘_f − 𝑒))) ≠ (𝑀 + 𝑁))
182		oveq12 7414	. . . . . . . . . . . . . 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 2953	. . . . . . . . . . . 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 3037	. . . . . . . . . . 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 5247	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒)))) = (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ (0_g‘𝑅)))
190	189	oveq2d 7421	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ ((𝑃‘𝑒)(._r‘𝑅)(𝑄‘(𝑥 ∘_f − 𝑒))))) = (𝑅 Σ_g (𝑒 ∈ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ↦ (0_g‘𝑅))))
191		ringmnd 20059	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
192	8, 191	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ Mnd)
193	192	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}) ∧ ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) ≠ (𝑀 + 𝑁)) → 𝑅 ∈ Mnd)
194	44	rabex 5331	. . . . . . . 8 ⊢ {𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} ∣ 𝑐 ∘_r ≤ 𝑥} ∈ V
195	41	gsumz 18713	. . . . . . . 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 2772	. . . . . 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 2962	. . . 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 3146	. 2 ⊢ (𝜑 → ∀𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin} (((𝑃 · 𝑄)‘𝑥) ≠ (0_g‘𝑅) → ((ℂ_fld ↾_s ℕ₀) Σ_g 𝑥) = (𝑀 + 𝑁)))
202	9, 12	nn0addcld 12532	. . 3 ⊢ (𝜑 → (𝑀 + 𝑁) ∈ ℕ₀)
203	1	mplring 21569	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring)
204	7, 8, 203	syl2anc 584	. . . 4 ⊢ (𝜑 → 𝑌 ∈ Ring)
205	2, 4	ringcl 20066	. . . 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 21677	. 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 2940 ∀wral 3061 {crab 3432 Vcvv 3474 ∖ cdif 3944 ∪ cun 3945 {csn 4627 class class class wbr 5147 ↦ cmpt 5230 ^◡ccnv 5674 “ cima 5678 Fun wfun 6534 ⟶wf 6536 ‘cfv 6540 (class class class)co 7405 ∘_f cof 7664 ∘_r cofr 7665 supp csupp 8142 ↑_m cmap 8816 Fincfn 8935 finSupp cfsupp 9357 0cc0 11106 + caddc 11109 ≤ cle 11245 − cmin 11440 ℕcn 12208 ℕ₀cn0 12468 Basecbs 17140 ↾_s cress 17169 +_gcplusg 17193 ._rcmulr 17194 0_gc0g 17381 Σ_g cgsu 17382 Mndcmnd 18621 SubMndcsubmnd 18666 CMndccmn 19642 Ringcrg 20049 ℂ_fldccnfld 20936 mPoly cmpl 21450 mHomP cmhp 21663

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 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-addf 11185 ax-mulf 11186

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 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-tp 4632 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-iin 4999 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-of 7666 df-ofr 7667 df-om 7852 df-1st 7971 df-2nd 7972 df-supp 8143 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-1o 8462 df-er 8699 df-map 8818 df-pm 8819 df-ixp 8888 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-fsupp 9358 df-sup 9433 df-oi 9501 df-card 9930 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-nn 12209 df-2 12271 df-3 12272 df-4 12273 df-5 12274 df-6 12275 df-7 12276 df-8 12277 df-9 12278 df-n0 12469 df-z 12555 df-dec 12674 df-uz 12819 df-fz 13481 df-fzo 13624 df-seq 13963 df-hash 14287 df-struct 17076 df-sets 17093 df-slot 17111 df-ndx 17123 df-base 17141 df-ress 17170 df-plusg 17206 df-mulr 17207 df-starv 17208 df-sca 17209 df-vsca 17210 df-ip 17211 df-tset 17212 df-ple 17213 df-ds 17215 df-unif 17216 df-hom 17217 df-cco 17218 df-0g 17383 df-gsum 17384 df-prds 17389 df-pws 17391 df-mre 17526 df-mrc 17527 df-acs 17529 df-mgm 18557 df-sgrp 18606 df-mnd 18622 df-mhm 18667 df-submnd 18668 df-grp 18818 df-minusg 18819 df-mulg 18945 df-subg 18997 df-ghm 19084 df-cntz 19175 df-cmn 19644 df-abl 19645 df-mgp 19982 df-ur 19999 df-ring 20051 df-cring 20052 df-subrg 20353 df-cnfld 20937 df-psr 21453 df-mpl 21455 df-mhp 21667

This theorem is referenced by: mhppwdeg 21684

W3C validator