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 closure hypotheses. (Revised by SN, 4-Sep-2025)

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