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) Remove sethood hypothesis. (Revised by SN, 18-May-2025)

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