This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝑑 = 𝑥 → { 𝑐 ∈ { ℎ ∈ ( ℕ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 ⊢ ( 𝜑 → ( 𝑃 · 𝑄 ) ∈ ( 𝐻 ‘ ( 𝑀 + 𝑁 ) ) )