Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mhpmulcl Structured version   Visualization version   GIF version

Theorem mhpmulcl 20835
 Description: A product of homogeneous polynomials is a homogeneous polynomial whose degree is the sum of the degrees of the factors. Compare mdegmulle2 24721 (which shows less-than-or-equal instead of equal). (Contributed by SN, 22-Jul-2024.)
Hypotheses
Ref Expression
mhpmulcl.h 𝐻 = (𝐼 mHomP 𝑅)
mhpmulcl.y 𝑌 = (𝐼 mPoly 𝑅)
mhpmulcl.t · = (.r𝑌)
mhpmulcl.i (𝜑𝐼𝑉)
mhpmulcl.r (𝜑𝑅 ∈ Ring)
mhpmulcl.m (𝜑𝑀 ∈ ℕ0)
mhpmulcl.n (𝜑𝑁 ∈ ℕ0)
mhpmulcl.p (𝜑𝑃 ∈ (𝐻𝑀))
mhpmulcl.q (𝜑𝑄 ∈ (𝐻𝑁))
Assertion
Ref Expression
mhpmulcl (𝜑 → (𝑃 · 𝑄) ∈ (𝐻‘(𝑀 + 𝑁)))

Proof of Theorem mhpmulcl
Dummy variables 𝑏 𝑑 𝑒 𝑖 𝑥 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mhpmulcl.y . . . . . . . 8 𝑌 = (𝐼 mPoly 𝑅)
2 eqid 2798 . . . . . . . 8 (Base‘𝑌) = (Base‘𝑌)
3 eqid 2798 . . . . . . . 8 (.r𝑅) = (.r𝑅)
4 mhpmulcl.t . . . . . . . 8 · = (.r𝑌)
5 eqid 2798 . . . . . . . 8 { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}
6 mhpmulcl.h . . . . . . . . 9 𝐻 = (𝐼 mHomP 𝑅)
7 mhpmulcl.i . . . . . . . . 9 (𝜑𝐼𝑉)
8 mhpmulcl.r . . . . . . . . 9 (𝜑𝑅 ∈ Ring)
9 mhpmulcl.m . . . . . . . . 9 (𝜑𝑀 ∈ ℕ0)
10 mhpmulcl.p . . . . . . . . 9 (𝜑𝑃 ∈ (𝐻𝑀))
116, 1, 2, 7, 8, 9, 10mhpmpl 20830 . . . . . . . 8 (𝜑𝑃 ∈ (Base‘𝑌))
12 mhpmulcl.n . . . . . . . . 9 (𝜑𝑁 ∈ ℕ0)
13 mhpmulcl.q . . . . . . . . 9 (𝜑𝑄 ∈ (𝐻𝑁))
146, 1, 2, 7, 8, 12, 13mhpmpl 20830 . . . . . . . 8 (𝜑𝑄 ∈ (Base‘𝑌))
151, 2, 3, 4, 5, 11, 14mplmul 20717 . . . . . . 7 (𝜑 → (𝑃 · 𝑄) = (𝑑 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ (𝑅 Σg (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑑} ↦ ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑑f𝑒)))))))
1615adantr 484 . . . . . 6 ((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → (𝑃 · 𝑄) = (𝑑 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ (𝑅 Σg (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑑} ↦ ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑑f𝑒)))))))
17 breq2 5037 . . . . . . . . . 10 (𝑑 = 𝑥 → (𝑐r𝑑𝑐r𝑥))
1817rabbidv 3427 . . . . . . . . 9 (𝑑 = 𝑥 → {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑑} = {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥})
19 fvoveq1 7165 . . . . . . . . . 10 (𝑑 = 𝑥 → (𝑄‘(𝑑f𝑒)) = (𝑄‘(𝑥f𝑒)))
2019oveq2d 7158 . . . . . . . . 9 (𝑑 = 𝑥 → ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑑f𝑒))) = ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑥f𝑒))))
2118, 20mpteq12dv 5118 . . . . . . . 8 (𝑑 = 𝑥 → (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑑} ↦ ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑑f𝑒)))) = (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} ↦ ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑥f𝑒)))))
2221oveq2d 7158 . . . . . . 7 (𝑑 = 𝑥 → (𝑅 Σg (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑑} ↦ ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑑f𝑒))))) = (𝑅 Σg (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} ↦ ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑥f𝑒))))))
2322adantl 485 . . . . . 6 (((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ 𝑑 = 𝑥) → (𝑅 Σg (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑑} ↦ ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑑f𝑒))))) = (𝑅 Σg (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} ↦ ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑥f𝑒))))))
24 simpr 488 . . . . . 6 ((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → 𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
25 ovexd 7177 . . . . . 6 ((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → (𝑅 Σg (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} ↦ ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑥f𝑒))))) ∈ V)
2616, 23, 24, 25fvmptd 6759 . . . . 5 ((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → ((𝑃 · 𝑄)‘𝑥) = (𝑅 Σg (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} ↦ ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑥f𝑒))))))
2726neeq1d 3046 . . . 4 ((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → (((𝑃 · 𝑄)‘𝑥) ≠ (0g𝑅) ↔ (𝑅 Σg (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} ↦ ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑥f𝑒))))) ≠ (0g𝑅)))
28 simp-4l 782 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg 𝑒) ≠ 𝑀) → 𝜑)
29 oveq2 7150 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑒 → ((ℂflds0) Σg 𝑐) = ((ℂflds0) Σg 𝑒))
3029eqeq1d 2800 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑒 → (((ℂflds0) Σg 𝑐) = 𝑀 ↔ ((ℂflds0) Σg 𝑒) = 𝑀))
3130necon3bbid 3024 . . . . . . . . . . . . . . 15 (𝑐 = 𝑒 → (¬ ((ℂflds0) Σg 𝑐) = 𝑀 ↔ ((ℂflds0) Σg 𝑒) ≠ 𝑀))
32 simplr 768 . . . . . . . . . . . . . . . 16 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg 𝑒) ≠ 𝑀) → 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥})
33 elrabi 3623 . . . . . . . . . . . . . . . 16 (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} → 𝑒 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
3432, 33syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg 𝑒) ≠ 𝑀) → 𝑒 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
35 simpr 488 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg 𝑒) ≠ 𝑀) → ((ℂflds0) Σg 𝑒) ≠ 𝑀)
3631, 34, 35elrabd 3631 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg 𝑒) ≠ 𝑀) → 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ¬ ((ℂflds0) Σg 𝑐) = 𝑀})
37 notrab 4234 . . . . . . . . . . . . . 14 ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∖ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑐) = 𝑀}) = {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ¬ ((ℂflds0) Σg 𝑐) = 𝑀}
3836, 37eleqtrrdi 2901 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg 𝑒) ≠ 𝑀) → 𝑒 ∈ ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∖ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑐) = 𝑀}))
39 eqid 2798 . . . . . . . . . . . . . . 15 (Base‘𝑅) = (Base‘𝑅)
401, 39, 2, 5, 11mplelf 20706 . . . . . . . . . . . . . 14 (𝜑𝑃:{ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}⟶(Base‘𝑅))
41 eqid 2798 . . . . . . . . . . . . . . 15 (0g𝑅) = (0g𝑅)
426, 41, 5, 7, 8, 9, 10mhpdeg 20831 . . . . . . . . . . . . . 14 (𝜑 → (𝑃 supp (0g𝑅)) ⊆ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑐) = 𝑀})
43 ovex 7175 . . . . . . . . . . . . . . . 16 (ℕ0m 𝐼) ∈ V
4443rabex 5202 . . . . . . . . . . . . . . 15 { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∈ V
4544a1i 11 . . . . . . . . . . . . . 14 (𝜑 → { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∈ V)
46 fvexd 6667 . . . . . . . . . . . . . 14 (𝜑 → (0g𝑅) ∈ V)
4740, 42, 45, 46suppssr 7858 . . . . . . . . . . . . 13 ((𝜑𝑒 ∈ ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∖ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑐) = 𝑀})) → (𝑃𝑒) = (0g𝑅))
4828, 38, 47syl2anc 587 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg 𝑒) ≠ 𝑀) → (𝑃𝑒) = (0g𝑅))
4948oveq1d 7157 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg 𝑒) ≠ 𝑀) → ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑥f𝑒))) = ((0g𝑅)(.r𝑅)(𝑄‘(𝑥f𝑒))))
508ad4antr 731 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg 𝑒) ≠ 𝑀) → 𝑅 ∈ Ring)
5114ad4antr 731 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg 𝑒) ≠ 𝑀) → 𝑄 ∈ (Base‘𝑌))
521, 39, 2, 5, 51mplelf 20706 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg 𝑒) ≠ 𝑀) → 𝑄:{ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}⟶(Base‘𝑅))
53 simp-4r 783 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg 𝑒) ≠ 𝑀) → 𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
54 eqid 2798 . . . . . . . . . . . . . . . 16 {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} = {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}
555, 54psrbagconcl 20639 . . . . . . . . . . . . . . 15 ((𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (𝑥f𝑒) ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥})
5653, 32, 55syl2anc 587 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg 𝑒) ≠ 𝑀) → (𝑥f𝑒) ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥})
57 elrabi 3623 . . . . . . . . . . . . . 14 ((𝑥f𝑒) ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} → (𝑥f𝑒) ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
5856, 57syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg 𝑒) ≠ 𝑀) → (𝑥f𝑒) ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
5952, 58ffvelrnd 6836 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg 𝑒) ≠ 𝑀) → (𝑄‘(𝑥f𝑒)) ∈ (Base‘𝑅))
6039, 3, 41ringlz 19351 . . . . . . . . . . . 12 ((𝑅 ∈ Ring ∧ (𝑄‘(𝑥f𝑒)) ∈ (Base‘𝑅)) → ((0g𝑅)(.r𝑅)(𝑄‘(𝑥f𝑒))) = (0g𝑅))
6150, 59, 60syl2anc 587 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg 𝑒) ≠ 𝑀) → ((0g𝑅)(.r𝑅)(𝑄‘(𝑥f𝑒))) = (0g𝑅))
6249, 61eqtrd 2833 . . . . . . . . . 10 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg 𝑒) ≠ 𝑀) → ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑥f𝑒))) = (0g𝑅))
63 simp-4l 782 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁) → 𝜑)
64 oveq2 7150 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑥f𝑒) → ((ℂflds0) Σg 𝑐) = ((ℂflds0) Σg (𝑥f𝑒)))
6564eqeq1d 2800 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑥f𝑒) → (((ℂflds0) Σg 𝑐) = 𝑁 ↔ ((ℂflds0) Σg (𝑥f𝑒)) = 𝑁))
6665necon3bbid 3024 . . . . . . . . . . . . . . 15 (𝑐 = (𝑥f𝑒) → (¬ ((ℂflds0) Σg 𝑐) = 𝑁 ↔ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁))
67 simp-4r 783 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁) → 𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
68 simplr 768 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁) → 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥})
6967, 68, 55syl2anc 587 . . . . . . . . . . . . . . . 16 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁) → (𝑥f𝑒) ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥})
7069, 57syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁) → (𝑥f𝑒) ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
71 simpr 488 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁) → ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁)
7266, 70, 71elrabd 3631 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁) → (𝑥f𝑒) ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ¬ ((ℂflds0) Σg 𝑐) = 𝑁})
73 notrab 4234 . . . . . . . . . . . . . 14 ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∖ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑐) = 𝑁}) = {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ¬ ((ℂflds0) Σg 𝑐) = 𝑁}
7472, 73eleqtrrdi 2901 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁) → (𝑥f𝑒) ∈ ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∖ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑐) = 𝑁}))
751, 39, 2, 5, 14mplelf 20706 . . . . . . . . . . . . . 14 (𝜑𝑄:{ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}⟶(Base‘𝑅))
766, 41, 5, 7, 8, 12, 13mhpdeg 20831 . . . . . . . . . . . . . 14 (𝜑 → (𝑄 supp (0g𝑅)) ⊆ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑐) = 𝑁})
7775, 76, 45, 46suppssr 7858 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥f𝑒) ∈ ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∖ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑐) = 𝑁})) → (𝑄‘(𝑥f𝑒)) = (0g𝑅))
7863, 74, 77syl2anc 587 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁) → (𝑄‘(𝑥f𝑒)) = (0g𝑅))
7978oveq2d 7158 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁) → ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑥f𝑒))) = ((𝑃𝑒)(.r𝑅)(0g𝑅)))
808ad4antr 731 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁) → 𝑅 ∈ Ring)
8111ad4antr 731 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁) → 𝑃 ∈ (Base‘𝑌))
821, 39, 2, 5, 81mplelf 20706 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁) → 𝑃:{ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}⟶(Base‘𝑅))
8333adantl 485 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → 𝑒 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
8483adantr 484 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁) → 𝑒 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
8582, 84ffvelrnd 6836 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁) → (𝑃𝑒) ∈ (Base‘𝑅))
8639, 3, 41ringrz 19352 . . . . . . . . . . . 12 ((𝑅 ∈ Ring ∧ (𝑃𝑒) ∈ (Base‘𝑅)) → ((𝑃𝑒)(.r𝑅)(0g𝑅)) = (0g𝑅))
8780, 85, 86syl2anc 587 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁) → ((𝑃𝑒)(.r𝑅)(0g𝑅)) = (0g𝑅))
8879, 87eqtrd 2833 . . . . . . . . . 10 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁) → ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑥f𝑒))) = (0g𝑅))
89 nn0subm 20164 . . . . . . . . . . . . . . . 16 0 ∈ (SubMnd‘ℂfld)
90 eqid 2798 . . . . . . . . . . . . . . . . 17 (ℂflds0) = (ℂflds0)
9190submbas 17988 . . . . . . . . . . . . . . . 16 (ℕ0 ∈ (SubMnd‘ℂfld) → ℕ0 = (Base‘(ℂflds0)))
9289, 91ax-mp 5 . . . . . . . . . . . . . . 15 0 = (Base‘(ℂflds0))
93 cnfld0 20133 . . . . . . . . . . . . . . . . 17 0 = (0g‘ℂfld)
9490, 93subm0 17989 . . . . . . . . . . . . . . . 16 (ℕ0 ∈ (SubMnd‘ℂfld) → 0 = (0g‘(ℂflds0)))
9589, 94ax-mp 5 . . . . . . . . . . . . . . 15 0 = (0g‘(ℂflds0))
96 nn0ex 11906 . . . . . . . . . . . . . . . 16 0 ∈ V
97 cnfldadd 20114 . . . . . . . . . . . . . . . . 17 + = (+g‘ℂfld)
9890, 97ressplusg 16621 . . . . . . . . . . . . . . . 16 (ℕ0 ∈ V → + = (+g‘(ℂflds0)))
9996, 98ax-mp 5 . . . . . . . . . . . . . . 15 + = (+g‘(ℂflds0))
100 cnring 20131 . . . . . . . . . . . . . . . . . 18 fld ∈ Ring
101 ringcmn 19345 . . . . . . . . . . . . . . . . . 18 (ℂfld ∈ Ring → ℂfld ∈ CMnd)
102100, 101ax-mp 5 . . . . . . . . . . . . . . . . 17 fld ∈ CMnd
10390submcmn 18969 . . . . . . . . . . . . . . . . 17 ((ℂfld ∈ CMnd ∧ ℕ0 ∈ (SubMnd‘ℂfld)) → (ℂflds0) ∈ CMnd)
104102, 89, 103mp2an 691 . . . . . . . . . . . . . . . 16 (ℂflds0) ∈ CMnd
105104a1i 11 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (ℂflds0) ∈ CMnd)
1067ad3antrrr 729 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → 𝐼𝑉)
1075psrbagf 20623 . . . . . . . . . . . . . . . 16 (𝑒 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} → 𝑒:𝐼⟶ℕ0)
10883, 107syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → 𝑒:𝐼⟶ℕ0)
109 simpllr 775 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → 𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
1105psrbagf 20623 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} → 𝑥:𝐼⟶ℕ0)
111109, 110syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → 𝑥:𝐼⟶ℕ0)
112111ffnd 6493 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → 𝑥 Fn 𝐼)
113108ffnd 6493 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → 𝑒 Fn 𝐼)
114 inidm 4147 . . . . . . . . . . . . . . . . 17 (𝐼𝐼) = 𝐼
115 eqidd 2799 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ 𝑖𝐼) → (𝑥𝑖) = (𝑥𝑖))
116 eqidd 2799 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ 𝑖𝐼) → (𝑒𝑖) = (𝑒𝑖))
117112, 113, 106, 106, 114, 115, 116offval 7405 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (𝑥f𝑒) = (𝑖𝐼 ↦ ((𝑥𝑖) − (𝑒𝑖))))
118 simpl 486 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ 𝑖𝐼) → (((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}))
119 simplr 768 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ 𝑖𝐼) → 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥})
120 breq1 5036 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = 𝑒 → (𝑐r𝑥𝑒r𝑥))
121120elrab 3629 . . . . . . . . . . . . . . . . . . . 20 (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} ↔ (𝑒 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∧ 𝑒r𝑥))
122121simprbi 500 . . . . . . . . . . . . . . . . . . 19 (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} → 𝑒r𝑥)
123119, 122syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ 𝑖𝐼) → 𝑒r𝑥)
124 simpr 488 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ 𝑖𝐼) → 𝑖𝐼)
125113, 112, 106, 106, 114, 116, 115ofrval 7408 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ 𝑒r𝑥𝑖𝐼) → (𝑒𝑖) ≤ (𝑥𝑖))
126118, 123, 124, 125syl3anc 1368 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ 𝑖𝐼) → (𝑒𝑖) ≤ (𝑥𝑖))
127108ffvelrnda 6835 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ 𝑖𝐼) → (𝑒𝑖) ∈ ℕ0)
128111ffvelrnda 6835 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ 𝑖𝐼) → (𝑥𝑖) ∈ ℕ0)
129 nn0sub 11950 . . . . . . . . . . . . . . . . . 18 (((𝑒𝑖) ∈ ℕ0 ∧ (𝑥𝑖) ∈ ℕ0) → ((𝑒𝑖) ≤ (𝑥𝑖) ↔ ((𝑥𝑖) − (𝑒𝑖)) ∈ ℕ0))
130127, 128, 129syl2anc 587 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ 𝑖𝐼) → ((𝑒𝑖) ≤ (𝑥𝑖) ↔ ((𝑥𝑖) − (𝑒𝑖)) ∈ ℕ0))
131126, 130mpbid 235 . . . . . . . . . . . . . . . 16 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ 𝑖𝐼) → ((𝑥𝑖) − (𝑒𝑖)) ∈ ℕ0)
132117, 131fmpt3d 6864 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (𝑥f𝑒):𝐼⟶ℕ0)
133108ffund 6496 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → Fun 𝑒)
134 c0ex 10639 . . . . . . . . . . . . . . . . . . . 20 0 ∈ V
135106, 134jctir 524 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (𝐼𝑉 ∧ 0 ∈ V))
136 frnsuppeq 7837 . . . . . . . . . . . . . . . . . . 19 ((𝐼𝑉 ∧ 0 ∈ V) → (𝑒:𝐼⟶ℕ0 → (𝑒 supp 0) = (𝑒 “ (ℕ0 ∖ {0}))))
137135, 108, 136sylc 65 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (𝑒 supp 0) = (𝑒 “ (ℕ0 ∖ {0})))
138 dfn2 11913 . . . . . . . . . . . . . . . . . . 19 ℕ = (ℕ0 ∖ {0})
139138imaeq2i 5897 . . . . . . . . . . . . . . . . . 18 (𝑒 “ ℕ) = (𝑒 “ (ℕ0 ∖ {0}))
140137, 139eqtr4di 2851 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (𝑒 supp 0) = (𝑒 “ ℕ))
1415psrbag 20622 . . . . . . . . . . . . . . . . . . . 20 (𝐼𝑉 → (𝑒 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↔ (𝑒:𝐼⟶ℕ0 ∧ (𝑒 “ ℕ) ∈ Fin)))
142106, 141syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (𝑒 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↔ (𝑒:𝐼⟶ℕ0 ∧ (𝑒 “ ℕ) ∈ Fin)))
14383, 142mpbid 235 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (𝑒:𝐼⟶ℕ0 ∧ (𝑒 “ ℕ) ∈ Fin))
144143simprd 499 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (𝑒 “ ℕ) ∈ Fin)
145140, 144eqeltrd 2890 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (𝑒 supp 0) ∈ Fin)
14683elexd 3461 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → 𝑒 ∈ V)
147 isfsupp 8836 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ V ∧ 0 ∈ V) → (𝑒 finSupp 0 ↔ (Fun 𝑒 ∧ (𝑒 supp 0) ∈ Fin)))
148146, 134, 147sylancl 589 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (𝑒 finSupp 0 ↔ (Fun 𝑒 ∧ (𝑒 supp 0) ∈ Fin)))
149133, 145, 148mpbir2and 712 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → 𝑒 finSupp 0)
150112, 113, 106, 106offun 7410 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → Fun (𝑥f𝑒))
1515psrbagfsupp 20625 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} → 𝑥 finSupp 0)
152109, 151syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → 𝑥 finSupp 0)
153152, 149fsuppunfi 8852 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → ((𝑥 supp 0) ∪ (𝑒 supp 0)) ∈ Fin)
154 0nn0 11915 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℕ0
155154a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → 0 ∈ ℕ0)
156 0m0e0 11760 . . . . . . . . . . . . . . . . . . 19 (0 − 0) = 0
157156a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (0 − 0) = 0)
158106, 155, 111, 108, 157suppofssd 7865 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → ((𝑥f𝑒) supp 0) ⊆ ((𝑥 supp 0) ∪ (𝑒 supp 0)))
159153, 158ssfid 8740 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → ((𝑥f𝑒) supp 0) ∈ Fin)
160 ovexd 7177 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (𝑥f𝑒) ∈ V)
161 isfsupp 8836 . . . . . . . . . . . . . . . . 17 (((𝑥f𝑒) ∈ V ∧ 0 ∈ V) → ((𝑥f𝑒) finSupp 0 ↔ (Fun (𝑥f𝑒) ∧ ((𝑥f𝑒) supp 0) ∈ Fin)))
162160, 134, 161sylancl 589 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → ((𝑥f𝑒) finSupp 0 ↔ (Fun (𝑥f𝑒) ∧ ((𝑥f𝑒) supp 0) ∈ Fin)))
163150, 159, 162mpbir2and 712 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (𝑥f𝑒) finSupp 0)
16492, 95, 99, 105, 106, 108, 132, 149, 163gsumadd 19054 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → ((ℂflds0) Σg (𝑒f + (𝑥f𝑒))) = (((ℂflds0) Σg 𝑒) + ((ℂflds0) Σg (𝑥f𝑒))))
165108ffvelrnda 6835 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ 𝑏𝐼) → (𝑒𝑏) ∈ ℕ0)
166165nn0cnd 11962 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ 𝑏𝐼) → (𝑒𝑏) ∈ ℂ)
167111ffvelrnda 6835 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ 𝑏𝐼) → (𝑥𝑏) ∈ ℕ0)
168167nn0cnd 11962 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ 𝑏𝐼) → (𝑥𝑏) ∈ ℂ)
169166, 168pncan3d 11004 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ 𝑏𝐼) → ((𝑒𝑏) + ((𝑥𝑏) − (𝑒𝑏))) = (𝑥𝑏))
170169mpteq2dva 5128 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (𝑏𝐼 ↦ ((𝑒𝑏) + ((𝑥𝑏) − (𝑒𝑏)))) = (𝑏𝐼 ↦ (𝑥𝑏)))
171 fvexd 6667 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ 𝑏𝐼) → (𝑒𝑏) ∈ V)
172 ovexd 7177 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) ∧ 𝑏𝐼) → ((𝑥𝑏) − (𝑒𝑏)) ∈ V)
173108feqmptd 6715 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → 𝑒 = (𝑏𝐼 ↦ (𝑒𝑏)))
174111feqmptd 6715 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → 𝑥 = (𝑏𝐼 ↦ (𝑥𝑏)))
175106, 167, 165, 174, 173offval2 7416 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (𝑥f𝑒) = (𝑏𝐼 ↦ ((𝑥𝑏) − (𝑒𝑏))))
176106, 171, 172, 173, 175offval2 7416 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (𝑒f + (𝑥f𝑒)) = (𝑏𝐼 ↦ ((𝑒𝑏) + ((𝑥𝑏) − (𝑒𝑏)))))
177170, 176, 1743eqtr4d 2843 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (𝑒f + (𝑥f𝑒)) = 𝑥)
178177oveq2d 7158 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → ((ℂflds0) Σg (𝑒f + (𝑥f𝑒))) = ((ℂflds0) Σg 𝑥))
179164, 178eqtr3d 2835 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (((ℂflds0) Σg 𝑒) + ((ℂflds0) Σg (𝑥f𝑒))) = ((ℂflds0) Σg 𝑥))
180 simplr 768 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁))
181179, 180eqnetrd 3054 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (((ℂflds0) Σg 𝑒) + ((ℂflds0) Σg (𝑥f𝑒))) ≠ (𝑀 + 𝑁))
182 oveq12 7151 . . . . . . . . . . . . . 14 ((((ℂflds0) Σg 𝑒) = 𝑀 ∧ ((ℂflds0) Σg (𝑥f𝑒)) = 𝑁) → (((ℂflds0) Σg 𝑒) + ((ℂflds0) Σg (𝑥f𝑒))) = (𝑀 + 𝑁))
183182a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → ((((ℂflds0) Σg 𝑒) = 𝑀 ∧ ((ℂflds0) Σg (𝑥f𝑒)) = 𝑁) → (((ℂflds0) Σg 𝑒) + ((ℂflds0) Σg (𝑥f𝑒))) = (𝑀 + 𝑁)))
184183necon3ad 3000 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → ((((ℂflds0) Σg 𝑒) + ((ℂflds0) Σg (𝑥f𝑒))) ≠ (𝑀 + 𝑁) → ¬ (((ℂflds0) Σg 𝑒) = 𝑀 ∧ ((ℂflds0) Σg (𝑥f𝑒)) = 𝑁)))
185181, 184mpd 15 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → ¬ (((ℂflds0) Σg 𝑒) = 𝑀 ∧ ((ℂflds0) Σg (𝑥f𝑒)) = 𝑁))
186 neorian 3081 . . . . . . . . . . 11 ((((ℂflds0) Σg 𝑒) ≠ 𝑀 ∨ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁) ↔ ¬ (((ℂflds0) Σg 𝑒) = 𝑀 ∧ ((ℂflds0) Σg (𝑥f𝑒)) = 𝑁))
187185, 186sylibr 237 . . . . . . . . . 10 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → (((ℂflds0) Σg 𝑒) ≠ 𝑀 ∨ ((ℂflds0) Σg (𝑥f𝑒)) ≠ 𝑁))
18862, 88, 187mpjaodan 956 . . . . . . . . 9 ((((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) ∧ 𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥}) → ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑥f𝑒))) = (0g𝑅))
189188mpteq2dva 5128 . . . . . . . 8 (((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) → (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} ↦ ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑥f𝑒)))) = (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} ↦ (0g𝑅)))
190189oveq2d 7158 . . . . . . 7 (((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) → (𝑅 Σg (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} ↦ ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑥f𝑒))))) = (𝑅 Σg (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} ↦ (0g𝑅))))
191 ringmnd 19318 . . . . . . . . . 10 (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
1928, 191syl 17 . . . . . . . . 9 (𝜑𝑅 ∈ Mnd)
193192ad2antrr 725 . . . . . . . 8 (((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) → 𝑅 ∈ Mnd)
19444rabex 5202 . . . . . . . 8 {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} ∈ V
19541gsumz 18009 . . . . . . . 8 ((𝑅 ∈ Mnd ∧ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} ∈ V) → (𝑅 Σg (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} ↦ (0g𝑅))) = (0g𝑅))
196193, 194, 195sylancl 589 . . . . . . 7 (((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) → (𝑅 Σg (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} ↦ (0g𝑅))) = (0g𝑅))
197190, 196eqtrd 2833 . . . . . 6 (((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) ∧ ((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁)) → (𝑅 Σg (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} ↦ ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑥f𝑒))))) = (0g𝑅))
198197ex 416 . . . . 5 ((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → (((ℂflds0) Σg 𝑥) ≠ (𝑀 + 𝑁) → (𝑅 Σg (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} ↦ ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑥f𝑒))))) = (0g𝑅)))
199198necon1d 3009 . . . 4 ((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → ((𝑅 Σg (𝑒 ∈ {𝑐 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ 𝑐r𝑥} ↦ ((𝑃𝑒)(.r𝑅)(𝑄‘(𝑥f𝑒))))) ≠ (0g𝑅) → ((ℂflds0) Σg 𝑥) = (𝑀 + 𝑁)))
20027, 199sylbid 243 . . 3 ((𝜑𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → (((𝑃 · 𝑄)‘𝑥) ≠ (0g𝑅) → ((ℂflds0) Σg 𝑥) = (𝑀 + 𝑁)))
201200ralrimiva 3149 . 2 (𝜑 → ∀𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} (((𝑃 · 𝑄)‘𝑥) ≠ (0g𝑅) → ((ℂflds0) Σg 𝑥) = (𝑀 + 𝑁)))
2029, 12nn0addcld 11964 . . 3 (𝜑 → (𝑀 + 𝑁) ∈ ℕ0)
2031mplring 20726 . . . . 5 ((𝐼𝑉𝑅 ∈ Ring) → 𝑌 ∈ Ring)
2047, 8, 203syl2anc 587 . . . 4 (𝜑𝑌 ∈ Ring)
2052, 4ringcl 19325 . . . 4 ((𝑌 ∈ Ring ∧ 𝑃 ∈ (Base‘𝑌) ∧ 𝑄 ∈ (Base‘𝑌)) → (𝑃 · 𝑄) ∈ (Base‘𝑌))
206204, 11, 14, 205syl3anc 1368 . . 3 (𝜑 → (𝑃 · 𝑄) ∈ (Base‘𝑌))
2076, 1, 2, 41, 5, 7, 8, 202, 206ismhp3 20829 . 2 (𝜑 → ((𝑃 · 𝑄) ∈ (𝐻‘(𝑀 + 𝑁)) ↔ ∀𝑥 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} (((𝑃 · 𝑄)‘𝑥) ≠ (0g𝑅) → ((ℂflds0) Σg 𝑥) = (𝑀 + 𝑁))))
208201, 207mpbird 260 1 (𝜑 → (𝑃 · 𝑄) ∈ (𝐻‘(𝑀 + 𝑁)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  {crab 3110  Vcvv 3441   ∖ cdif 3879   ∪ cun 3880  {csn 4527   class class class wbr 5033   ↦ cmpt 5113  ◡ccnv 5521   “ cima 5525  Fun wfun 6323  ⟶wf 6325  ‘cfv 6329  (class class class)co 7142   ∘f cof 7395   ∘r cofr 7396   supp csupp 7823   ↑m cmap 8404  Fincfn 8507   finSupp cfsupp 8832  0cc0 10541   + caddc 10544   ≤ cle 10680   − cmin 10874  ℕcn 11640  ℕ0cn0 11900  Basecbs 16492   ↾s cress 16493  +gcplusg 16574  .rcmulr 16575  0gc0g 16722   Σg cgsu 16723  Mndcmnd 17920  SubMndcsubmnd 17964  CMndccmn 18916  Ringcrg 19308  ℂfldccnfld 20109   mPoly cmpl 20611   mHomP cmhp 20815 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7451  ax-cnex 10597  ax-resscn 10598  ax-1cn 10599  ax-icn 10600  ax-addcl 10601  ax-addrcl 10602  ax-mulcl 10603  ax-mulrcl 10604  ax-mulcom 10605  ax-addass 10606  ax-mulass 10607  ax-distr 10608  ax-i2m1 10609  ax-1ne0 10610  ax-1rid 10611  ax-rnegex 10612  ax-rrecex 10613  ax-cnre 10614  ax-pre-lttri 10615  ax-pre-lttrn 10616  ax-pre-ltadd 10617  ax-pre-mulgt0 10618  ax-addf 10620  ax-mulf 10621 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3722  df-csb 3830  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-pss 3901  df-nul 4246  df-if 4428  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5441  df-so 5442  df-fr 5481  df-se 5482  df-we 5483  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6288  df-fun 6331  df-fn 6332  df-f 6333  df-f1 6334  df-fo 6335  df-f1o 6336  df-fv 6337  df-isom 6338  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-of 7397  df-ofr 7398  df-om 7571  df-1st 7681  df-2nd 7682  df-supp 7824  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-1o 8100  df-2o 8101  df-oadd 8104  df-er 8287  df-map 8406  df-pm 8407  df-ixp 8460  df-en 8508  df-dom 8509  df-sdom 8510  df-fin 8511  df-fsupp 8833  df-oi 8973  df-card 9367  df-pnf 10681  df-mnf 10682  df-xr 10683  df-ltxr 10684  df-le 10685  df-sub 10876  df-neg 10877  df-nn 11641  df-2 11703  df-3 11704  df-4 11705  df-5 11706  df-6 11707  df-7 11708  df-8 11709  df-9 11710  df-n0 11901  df-z 11987  df-dec 12104  df-uz 12249  df-fz 12903  df-fzo 13046  df-seq 13382  df-hash 13704  df-struct 16494  df-ndx 16495  df-slot 16496  df-base 16498  df-sets 16499  df-ress 16500  df-plusg 16587  df-mulr 16588  df-starv 16589  df-sca 16590  df-vsca 16591  df-tset 16593  df-ple 16594  df-ds 16596  df-unif 16597  df-0g 16724  df-gsum 16725  df-mre 16866  df-mrc 16867  df-acs 16869  df-mgm 17861  df-sgrp 17910  df-mnd 17921  df-mhm 17965  df-submnd 17966  df-grp 18115  df-minusg 18116  df-mulg 18235  df-subg 18286  df-ghm 18366  df-cntz 18457  df-cmn 18918  df-abl 18919  df-mgp 19251  df-ur 19263  df-ring 19310  df-cring 19311  df-subrg 19544  df-cnfld 20110  df-psr 20614  df-mpl 20616  df-mhp 20819 This theorem is referenced by:  mhppwdeg  20836
 Copyright terms: Public domain W3C validator