Theorem mhpmulcl

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

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

Proof

Step	Hyp	Ref	Expression
1		mhpmulcl.h	⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
2		mhpmulcl.y	⊢ 𝑌 = ( 𝐼 mPoly 𝑅 )
3		mhpmulcl.t	⊢ · = ( .r ‘ 𝑌 )
4		mhpmulcl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
5		mhpmulcl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		mhpmulcl.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
7		mhpmulcl.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
8		mhpmulcl.p	⊢ ( 𝜑 → 𝑃 ∈ ( 𝐻 ‘ 𝑀 ) )
9		mhpmulcl.q	⊢ ( 𝜑 → 𝑄 ∈ ( 𝐻 ‘ 𝑁 ) )
10		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
11		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
12		eqid	⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
13	1 2 10 4 5 6 8	mhpmpl	⊢ ( 𝜑 → 𝑃 ∈ ( Base ‘ 𝑌 ) )
14	1 2 10 4 5 7 9	mhpmpl	⊢ ( 𝜑 → 𝑄 ∈ ( Base ‘ 𝑌 ) )
15	2 10 11 3 12 13 14	mplmul	⊢ ( 𝜑 → ( 𝑃 · 𝑄 ) = ( 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑑 } ↦ ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑑 ∘f − 𝑒 ) ) ) ) ) ) )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑃 · 𝑄 ) = ( 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑑 } ↦ ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑑 ∘f − 𝑒 ) ) ) ) ) ) )
17		breq2	⊢ ( 𝑑 = 𝑥 → ( 𝑐 ∘r ≤ 𝑑 ↔ 𝑐 ∘r ≤ 𝑥 ) )
18	17	rabbidv	⊢ ( 𝑑 = 𝑥 → { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑑 } = { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } )
19		fvoveq1	⊢ ( 𝑑 = 𝑥 → ( 𝑄 ‘ ( 𝑑 ∘f − 𝑒 ) ) = ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) )
20	19	oveq2d	⊢ ( 𝑑 = 𝑥 → ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑑 ∘f − 𝑒 ) ) ) = ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) )
21	18 20	mpteq12dv	⊢ ( 𝑑 = 𝑥 → ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑑 } ↦ ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑑 ∘f − 𝑒 ) ) ) ) = ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ↦ ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) ) )
22	21	oveq2d	⊢ ( 𝑑 = 𝑥 → ( 𝑅 Σg ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑑 } ↦ ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑑 ∘f − 𝑒 ) ) ) ) ) = ( 𝑅 Σg ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ↦ ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) ) ) )
23	22	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ 𝑑 = 𝑥 ) → ( 𝑅 Σg ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑑 } ↦ ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑑 ∘f − 𝑒 ) ) ) ) ) = ( 𝑅 Σg ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ↦ ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) ) ) )
24		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
25		ovexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑅 Σg ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ↦ ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) ) ) ∈ V )
26	16 23 24 25	fvmptd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( 𝑃 · 𝑄 ) ‘ 𝑥 ) = ( 𝑅 Σg ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ↦ ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) ) ) )
27	26	neeq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ( 𝑃 · 𝑄 ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑅 ) ↔ ( 𝑅 Σg ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ↦ ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) ) ) ≠ ( 0g ‘ 𝑅 ) ) )
28		simp-4l	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ) → 𝜑 )
29		oveq2	⊢ ( 𝑐 = 𝑒 → ( ( ℂfld ↾s ℕ0 ) Σg 𝑐 ) = ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) )
30	29	eqeq1d	⊢ ( 𝑐 = 𝑒 → ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑐 ) = 𝑀 ↔ ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) = 𝑀 ) )
31	30	necon3bbid	⊢ ( 𝑐 = 𝑒 → ( ¬ ( ( ℂfld ↾s ℕ0 ) Σg 𝑐 ) = 𝑀 ↔ ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ) )
32		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ) → 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } )
33		elrabi	⊢ ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } → 𝑒 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
34	32 33	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ) → 𝑒 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
35		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 )
36	31 34 35	elrabd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ) → 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ¬ ( ( ℂfld ↾s ℕ0 ) Σg 𝑐 ) = 𝑀 } )
37		notrab	⊢ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑐 ) = 𝑀 } ) = { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ¬ ( ( ℂfld ↾s ℕ0 ) Σg 𝑐 ) = 𝑀 }
38	36 37	eleqtrrdi	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ) → 𝑒 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑐 ) = 𝑀 } ) )
39		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
40	2 39 10 12 13	mplelf	⊢ ( 𝜑 → 𝑃 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
41		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
42	1 41 12 4 5 6 8	mhpdeg	⊢ ( 𝜑 → ( 𝑃 supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑐 ) = 𝑀 } )
43		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
44	43	rabex	⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V
45	44	a1i	⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V )
46		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
47	40 42 45 46	suppssr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑐 ) = 𝑀 } ) ) → ( 𝑃 ‘ 𝑒 ) = ( 0g ‘ 𝑅 ) )
48	28 38 47	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ) → ( 𝑃 ‘ 𝑒 ) = ( 0g ‘ 𝑅 ) )
49	48	oveq1d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ) → ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) = ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) )
50	5	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ) → 𝑅 ∈ Ring )
51	14	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ) → 𝑄 ∈ ( Base ‘ 𝑌 ) )
52	2 39 10 12 51	mplelf	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ) → 𝑄 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
53		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ) → 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
54		eqid	⊢ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } = { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 }
55	12 54	psrbagconcl	⊢ ( ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( 𝑥 ∘f − 𝑒 ) ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } )
56	53 32 55	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ) → ( 𝑥 ∘f − 𝑒 ) ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } )
57		elrabi	⊢ ( ( 𝑥 ∘f − 𝑒 ) ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } → ( 𝑥 ∘f − 𝑒 ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
58	56 57	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ) → ( 𝑥 ∘f − 𝑒 ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
59	52 58	ffvelrnd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ) → ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ∈ ( Base ‘ 𝑅 ) )
60	39 11 41	ringlz	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) = ( 0g ‘ 𝑅 ) )
61	50 59 60	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) = ( 0g ‘ 𝑅 ) )
62	49 61	eqtrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ) → ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) = ( 0g ‘ 𝑅 ) )
63		simp-4l	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) → 𝜑 )
64		oveq2	⊢ ( 𝑐 = ( 𝑥 ∘f − 𝑒 ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑐 ) = ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) )
65	64	eqeq1d	⊢ ( 𝑐 = ( 𝑥 ∘f − 𝑒 ) → ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑐 ) = 𝑁 ↔ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) = 𝑁 ) )
66	65	necon3bbid	⊢ ( 𝑐 = ( 𝑥 ∘f − 𝑒 ) → ( ¬ ( ( ℂfld ↾s ℕ0 ) Σg 𝑐 ) = 𝑁 ↔ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) )
67		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) → 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
68		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) → 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } )
69	67 68 55	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) → ( 𝑥 ∘f − 𝑒 ) ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } )
70	69 57	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) → ( 𝑥 ∘f − 𝑒 ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
71		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) → ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 )
72	66 70 71	elrabd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) → ( 𝑥 ∘f − 𝑒 ) ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ¬ ( ( ℂfld ↾s ℕ0 ) Σg 𝑐 ) = 𝑁 } )
73		notrab	⊢ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑐 ) = 𝑁 } ) = { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ¬ ( ( ℂfld ↾s ℕ0 ) Σg 𝑐 ) = 𝑁 }
74	72 73	eleqtrrdi	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) → ( 𝑥 ∘f − 𝑒 ) ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑐 ) = 𝑁 } ) )
75	2 39 10 12 14	mplelf	⊢ ( 𝜑 → 𝑄 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
76	1 41 12 4 5 7 9	mhpdeg	⊢ ( 𝜑 → ( 𝑄 supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑐 ) = 𝑁 } )
77	75 76 45 46	suppssr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∘f − 𝑒 ) ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑐 ) = 𝑁 } ) ) → ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) = ( 0g ‘ 𝑅 ) )
78	63 74 77	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) → ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) = ( 0g ‘ 𝑅 ) )
79	78	oveq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) → ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) = ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
80	5	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) → 𝑅 ∈ Ring )
81	13	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) → 𝑃 ∈ ( Base ‘ 𝑌 ) )
82	2 39 10 12 81	mplelf	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) → 𝑃 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
83	33	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → 𝑒 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
84	83	adantr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) → 𝑒 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
85	82 84	ffvelrnd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) → ( 𝑃 ‘ 𝑒 ) ∈ ( Base ‘ 𝑅 ) )
86	39 11 41	ringrz	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑃 ‘ 𝑒 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
87	80 85 86	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) → ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
88	79 87	eqtrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) → ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) = ( 0g ‘ 𝑅 ) )
89		nn0subm	⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )
90		eqid	⊢ ( ℂfld ↾s ℕ0 ) = ( ℂfld ↾s ℕ0 )
91	90	submbas	⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → ℕ0 = ( Base ‘ ( ℂfld ↾s ℕ0 ) ) )
92	89 91	ax-mp	⊢ ℕ0 = ( Base ‘ ( ℂfld ↾s ℕ0 ) )
93		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
94	90 93	subm0	⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → 0 = ( 0g ‘ ( ℂfld ↾s ℕ0 ) ) )
95	89 94	ax-mp	⊢ 0 = ( 0g ‘ ( ℂfld ↾s ℕ0 ) )
96		nn0ex	⊢ ℕ0 ∈ V
97		cnfldadd	⊢ + = ( +g ‘ ℂfld )
98	90 97	ressplusg	⊢ ( ℕ0 ∈ V → + = ( +g ‘ ( ℂfld ↾s ℕ0 ) ) )
99	96 98	ax-mp	⊢ + = ( +g ‘ ( ℂfld ↾s ℕ0 ) )
100		cnring	⊢ ℂfld ∈ Ring
101		ringcmn	⊢ ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
102	100 101	ax-mp	⊢ ℂfld ∈ CMnd
103	90	submcmn	⊢ ( ( ℂfld ∈ CMnd ∧ ℕ0 ∈ ( SubMnd ‘ ℂfld ) ) → ( ℂfld ↾s ℕ0 ) ∈ CMnd )
104	102 89 103	mp2an	⊢ ( ℂfld ↾s ℕ0 ) ∈ CMnd
105	104	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( ℂfld ↾s ℕ0 ) ∈ CMnd )
106	4	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → 𝐼 ∈ 𝑉 )
107	12	psrbagf	⊢ ( 𝑒 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } → 𝑒 : 𝐼 ⟶ ℕ0 )
108	83 107	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → 𝑒 : 𝐼 ⟶ ℕ0 )
109		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
110	12	psrbagf	⊢ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } → 𝑥 : 𝐼 ⟶ ℕ0 )
111	109 110	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → 𝑥 : 𝐼 ⟶ ℕ0 )
112	111	ffnd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → 𝑥 Fn 𝐼 )
113	108	ffnd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → 𝑒 Fn 𝐼 )
114		inidm	⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
115		eqidd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑖 ) = ( 𝑥 ‘ 𝑖 ) )
116		eqidd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑒 ‘ 𝑖 ) = ( 𝑒 ‘ 𝑖 ) )
117	112 113 106 106 114 115 116	offval	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( 𝑥 ∘f − 𝑒 ) = ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑖 ) − ( 𝑒 ‘ 𝑖 ) ) ) )
118		simpl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ 𝑖 ∈ 𝐼 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) )
119		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ 𝑖 ∈ 𝐼 ) → 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } )
120		breq1	⊢ ( 𝑐 = 𝑒 → ( 𝑐 ∘r ≤ 𝑥 ↔ 𝑒 ∘r ≤ 𝑥 ) )
121	120	elrab	⊢ ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ↔ ( 𝑒 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∧ 𝑒 ∘r ≤ 𝑥 ) )
122	121	simprbi	⊢ ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } → 𝑒 ∘r ≤ 𝑥 )
123	119 122	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ 𝑖 ∈ 𝐼 ) → 𝑒 ∘r ≤ 𝑥 )
124		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ 𝑖 ∈ 𝐼 ) → 𝑖 ∈ 𝐼 )
125	113 112 106 106 114 116 115	ofrval	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ 𝑒 ∘r ≤ 𝑥 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑒 ‘ 𝑖 ) ≤ ( 𝑥 ‘ 𝑖 ) )
126	118 123 124 125	syl3anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑒 ‘ 𝑖 ) ≤ ( 𝑥 ‘ 𝑖 ) )
127	108	ffvelrnda	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑒 ‘ 𝑖 ) ∈ ℕ0 )
128	111	ffvelrnda	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑖 ) ∈ ℕ0 )
129		nn0sub	⊢ ( ( ( 𝑒 ‘ 𝑖 ) ∈ ℕ0 ∧ ( 𝑥 ‘ 𝑖 ) ∈ ℕ0 ) → ( ( 𝑒 ‘ 𝑖 ) ≤ ( 𝑥 ‘ 𝑖 ) ↔ ( ( 𝑥 ‘ 𝑖 ) − ( 𝑒 ‘ 𝑖 ) ) ∈ ℕ0 ) )
130	127 128 129	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑒 ‘ 𝑖 ) ≤ ( 𝑥 ‘ 𝑖 ) ↔ ( ( 𝑥 ‘ 𝑖 ) − ( 𝑒 ‘ 𝑖 ) ) ∈ ℕ0 ) )
131	126 130	mpbid	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑖 ) − ( 𝑒 ‘ 𝑖 ) ) ∈ ℕ0 )
132	117 131	fmpt3d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( 𝑥 ∘f − 𝑒 ) : 𝐼 ⟶ ℕ0 )
133	108	ffund	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → Fun 𝑒 )
134		c0ex	⊢ 0 ∈ V
135	106 134	jctir	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( 𝐼 ∈ 𝑉 ∧ 0 ∈ V ) )
136		frnsuppeq	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 0 ∈ V ) → ( 𝑒 : 𝐼 ⟶ ℕ0 → ( 𝑒 supp 0 ) = ( ◡ 𝑒 “ ( ℕ0 ∖ { 0 } ) ) ) )
137	135 108 136	sylc	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( 𝑒 supp 0 ) = ( ◡ 𝑒 “ ( ℕ0 ∖ { 0 } ) ) )
138		dfn2	⊢ ℕ = ( ℕ0 ∖ { 0 } )
139	138	imaeq2i	⊢ ( ◡ 𝑒 “ ℕ ) = ( ◡ 𝑒 “ ( ℕ0 ∖ { 0 } ) )
140	137 139	eqtr4di	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( 𝑒 supp 0 ) = ( ◡ 𝑒 “ ℕ ) )
141	12	psrbag	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑒 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↔ ( 𝑒 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑒 “ ℕ ) ∈ Fin ) ) )
142	106 141	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( 𝑒 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↔ ( 𝑒 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑒 “ ℕ ) ∈ Fin ) ) )
143	83 142	mpbid	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( 𝑒 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑒 “ ℕ ) ∈ Fin ) )
144	143	simprd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( ◡ 𝑒 “ ℕ ) ∈ Fin )
145	140 144	eqeltrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( 𝑒 supp 0 ) ∈ Fin )
146	83	elexd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → 𝑒 ∈ V )
147		isfsupp	⊢ ( ( 𝑒 ∈ V ∧ 0 ∈ V ) → ( 𝑒 finSupp 0 ↔ ( Fun 𝑒 ∧ ( 𝑒 supp 0 ) ∈ Fin ) ) )
148	146 134 147	sylancl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( 𝑒 finSupp 0 ↔ ( Fun 𝑒 ∧ ( 𝑒 supp 0 ) ∈ Fin ) ) )
149	133 145 148	mpbir2and	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → 𝑒 finSupp 0 )
150	112 113 106 106	offun	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → Fun ( 𝑥 ∘f − 𝑒 ) )
151	12	psrbagfsupp	⊢ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } → 𝑥 finSupp 0 )
152	109 151	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → 𝑥 finSupp 0 )
153	152 149	fsuppunfi	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( ( 𝑥 supp 0 ) ∪ ( 𝑒 supp 0 ) ) ∈ Fin )
154		0nn0	⊢ 0 ∈ ℕ0
155	154	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → 0 ∈ ℕ0 )
156		0m0e0	⊢ ( 0 − 0 ) = 0
157	156	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( 0 − 0 ) = 0 )
158	106 155 111 108 157	suppofssd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( ( 𝑥 ∘f − 𝑒 ) supp 0 ) ⊆ ( ( 𝑥 supp 0 ) ∪ ( 𝑒 supp 0 ) ) )
159	153 158	ssfid	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( ( 𝑥 ∘f − 𝑒 ) supp 0 ) ∈ Fin )
160		ovexd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( 𝑥 ∘f − 𝑒 ) ∈ V )
161		isfsupp	⊢ ( ( ( 𝑥 ∘f − 𝑒 ) ∈ V ∧ 0 ∈ V ) → ( ( 𝑥 ∘f − 𝑒 ) finSupp 0 ↔ ( Fun ( 𝑥 ∘f − 𝑒 ) ∧ ( ( 𝑥 ∘f − 𝑒 ) supp 0 ) ∈ Fin ) ) )
162	160 134 161	sylancl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( ( 𝑥 ∘f − 𝑒 ) finSupp 0 ↔ ( Fun ( 𝑥 ∘f − 𝑒 ) ∧ ( ( 𝑥 ∘f − 𝑒 ) supp 0 ) ∈ Fin ) ) )
163	150 159 162	mpbir2and	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( 𝑥 ∘f − 𝑒 ) finSupp 0 )
164	92 95 99 105 106 108 132 149 163	gsumadd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑒 ∘f + ( 𝑥 ∘f − 𝑒 ) ) ) = ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) + ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ) )
165	108	ffvelrnda	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑒 ‘ 𝑏 ) ∈ ℕ0 )
166	165	nn0cnd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑒 ‘ 𝑏 ) ∈ ℂ )
167	111	ffvelrnda	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑏 ) ∈ ℕ0 )
168	167	nn0cnd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑏 ) ∈ ℂ )
169	166 168	pncan3d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ 𝑏 ∈ 𝐼 ) → ( ( 𝑒 ‘ 𝑏 ) + ( ( 𝑥 ‘ 𝑏 ) − ( 𝑒 ‘ 𝑏 ) ) ) = ( 𝑥 ‘ 𝑏 ) )
170	169	mpteq2dva	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑒 ‘ 𝑏 ) + ( ( 𝑥 ‘ 𝑏 ) − ( 𝑒 ‘ 𝑏 ) ) ) ) = ( 𝑏 ∈ 𝐼 ↦ ( 𝑥 ‘ 𝑏 ) ) )
171		fvexd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑒 ‘ 𝑏 ) ∈ V )
172		ovexd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) ∧ 𝑏 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑏 ) − ( 𝑒 ‘ 𝑏 ) ) ∈ V )
173	108	feqmptd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → 𝑒 = ( 𝑏 ∈ 𝐼 ↦ ( 𝑒 ‘ 𝑏 ) ) )
174	111	feqmptd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → 𝑥 = ( 𝑏 ∈ 𝐼 ↦ ( 𝑥 ‘ 𝑏 ) ) )
175	106 167 165 174 173	offval2	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( 𝑥 ∘f − 𝑒 ) = ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑏 ) − ( 𝑒 ‘ 𝑏 ) ) ) )
176	106 171 172 173 175	offval2	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( 𝑒 ∘f + ( 𝑥 ∘f − 𝑒 ) ) = ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑒 ‘ 𝑏 ) + ( ( 𝑥 ‘ 𝑏 ) − ( 𝑒 ‘ 𝑏 ) ) ) ) )
177	170 176 174	3eqtr4d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( 𝑒 ∘f + ( 𝑥 ∘f − 𝑒 ) ) = 𝑥 )
178	177	oveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑒 ∘f + ( 𝑥 ∘f − 𝑒 ) ) ) = ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) )
179	164 178	eqtr3d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) + ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ) = ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) )
180		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) )
181	179 180	eqnetrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) + ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ) ≠ ( 𝑀 + 𝑁 ) )
182		oveq12	⊢ ( ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) = 𝑀 ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) = 𝑁 ) → ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) + ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ) = ( 𝑀 + 𝑁 ) )
183	182	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) = 𝑀 ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) = 𝑁 ) → ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) + ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ) = ( 𝑀 + 𝑁 ) ) )
184	183	necon3ad	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) + ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ) ≠ ( 𝑀 + 𝑁 ) → ¬ ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) = 𝑀 ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) = 𝑁 ) ) )
185	181 184	mpd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ¬ ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) = 𝑀 ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) = 𝑁 ) )
186		neorian	⊢ ( ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ∨ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) ↔ ¬ ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) = 𝑀 ∧ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) = 𝑁 ) )
187	185 186	sylibr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑒 ) ≠ 𝑀 ∨ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑥 ∘f − 𝑒 ) ) ≠ 𝑁 ) )
188	62 88 187	mpjaodan	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ) → ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) = ( 0g ‘ 𝑅 ) )
189	188	mpteq2dva	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) → ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ↦ ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) ) = ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ↦ ( 0g ‘ 𝑅 ) ) )
190	189	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) → ( 𝑅 Σg ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ↦ ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) ) ) = ( 𝑅 Σg ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ↦ ( 0g ‘ 𝑅 ) ) ) )
191		ringmnd	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
192	5 191	syl	⊢ ( 𝜑 → 𝑅 ∈ Mnd )
193	192	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) → 𝑅 ∈ Mnd )
194	44	rabex	⊢ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ∈ V
195	41	gsumz	⊢ ( ( 𝑅 ∈ Mnd ∧ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ∈ V ) → ( 𝑅 Σg ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
196	193 194 195	sylancl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) → ( 𝑅 Σg ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
197	190 196	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) ) → ( 𝑅 Σg ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ↦ ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) ) ) = ( 0g ‘ 𝑅 ) )
198	197	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) ≠ ( 𝑀 + 𝑁 ) → ( 𝑅 Σg ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ↦ ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) )
199	198	necon1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( 𝑅 Σg ( 𝑒 ∈ { 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑐 ∘r ≤ 𝑥 } ↦ ( ( 𝑃 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑄 ‘ ( 𝑥 ∘f − 𝑒 ) ) ) ) ) ≠ ( 0g ‘ 𝑅 ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) = ( 𝑀 + 𝑁 ) ) )
200	27 199	sylbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ( 𝑃 · 𝑄 ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑅 ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) = ( 𝑀 + 𝑁 ) ) )
201	200	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( ( ( 𝑃 · 𝑄 ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑅 ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) = ( 𝑀 + 𝑁 ) ) )
202	6 7	nn0addcld	⊢ ( 𝜑 → ( 𝑀 + 𝑁 ) ∈ ℕ0 )
203	2	mplring	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ Ring )
204	4 5 203	syl2anc	⊢ ( 𝜑 → 𝑌 ∈ Ring )
205	10 3	ringcl	⊢ ( ( 𝑌 ∈ Ring ∧ 𝑃 ∈ ( Base ‘ 𝑌 ) ∧ 𝑄 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑃 · 𝑄 ) ∈ ( Base ‘ 𝑌 ) )
206	204 13 14 205	syl3anc	⊢ ( 𝜑 → ( 𝑃 · 𝑄 ) ∈ ( Base ‘ 𝑌 ) )
207	1 2 10 41 12 4 5 202 206	ismhp3	⊢ ( 𝜑 → ( ( 𝑃 · 𝑄 ) ∈ ( 𝐻 ‘ ( 𝑀 + 𝑁 ) ) ↔ ∀ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( ( ( 𝑃 · 𝑄 ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑅 ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑥 ) = ( 𝑀 + 𝑁 ) ) ) )
208	201 207	mpbird	⊢ ( 𝜑 → ( 𝑃 · 𝑄 ) ∈ ( 𝐻 ‘ ( 𝑀 + 𝑁 ) ) )