Metamath Proof Explorer


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