---

Definition: rng_abmon
rng_abmon{i}() ==  {r:RngSig| IsMonoid(|r|;+r;0) ∧ Comm(|r|;+r) ∧ IsEqFun(|r|;=b)} 

Lemma: rng_abmon_wf
rng_abmon{i}() ∈ 𝕌'

Definition: rng_mssum
Σx ∈ a. f[x] ==  msFor{r↓+gp} x ∈ a. f[x]

Lemma: rng_mssum_wf
∀s:DSet. ∀r:Rng. ∀f:|s| ⟶ |r|. ∀a:MSet{s}.  (Σx ∈ a. f[x] ∈ |r|)

Lemma: rng_mssum_functionality_wrt_equal
∀s:DSet. ∀r:Rng. ∀f,f':|s| ⟶ |r|. ∀a,a':MSet{s}.
  ((a = a' ∈ MSet{s}) ⇒ (∀x:|s|. ((↑(x ∈b a)) ⇒ (f[x] = f'[x] ∈ |r|))) ⇒ ((Σx ∈ a. f[x]) = (Σx ∈ a'. f'[x]) ∈ |r|))

Lemma: comb_for_rng_mssum_wf
λs,r,f,a,z. Σx ∈ a. f[x] ∈ s:DSet ⟶ r:Rng ⟶ f:(|s| ⟶ |r|) ⟶ a:MSet{s} ⟶ (↓True) ⟶ |r|

Lemma: rng_mssum_functionality_wrt_bsubmset
∀s:DSet. ∀r:Rng. ∀f,f':|s| ⟶ |r|. ∀p,q:MSet{s}.
  ((∀x:|s|. ((↑(x ∈b q - p)) ⇒ (f'[x] = 0 ∈ |r|)))
  ⇒ (↑(p ⊆b q))
  ⇒ (∀x:|s|. ((↑(x ∈b p)) ⇒ (f[x] = f'[x] ∈ |r|)))
  ⇒ ((Σx ∈ p. f[x]) = (Σx ∈ q. f'[x]) ∈ |r|))

Lemma: rng_mssum_elim_lemma
∀[s,r,as,f:Top].  (Σx ∈ mk_mset(as). f[x] ~ Σ{r} x ∈ as. f[x])

Lemma: rng_times_mssum_l
∀s:DSet. ∀r:Rng. ∀f:|s| ⟶ |r|. ∀u:|r|. ∀a:MSet{s}.  ((u * (Σx ∈ a. f[x])) = (Σx ∈ a. (u * f[x])) ∈ |r|)

Lemma: rng_times_mssum_r
∀s:DSet. ∀r:Rng. ∀f:|s| ⟶ |r|. ∀u:|r|. ∀a:MSet{s}.  (((Σx ∈ a. f[x]) * u) = (Σx ∈ a. (f[x] * u)) ∈ |r|)

Lemma: rng_mssum_when_swap
∀s:DSet. ∀r:Rng. ∀f:|s| ⟶ |r|. ∀b:𝔹. ∀a:MSet{s}.  ((Σx ∈ a. (when b. f[x])) = (when b. (Σx ∈ a. f[x])) ∈ |r|)

Lemma: rng_mssum_swap
∀r:Rng. ∀s,s':DSet. ∀f:|s| ⟶ |s'| ⟶ |r|. ∀a:MSet{s}. ∀b:MSet{s'}.
  ((Σx ∈ a. Σy ∈ b. f[x;y]) = (Σy ∈ b. Σx ∈ a. f[x;y]) ∈ |r|)

Lemma: rng_mssum_of_plus
∀r:Rng. ∀s:DSet. ∀e,f:|s| ⟶ |r|. ∀a:MSet{s}.  ((Σx ∈ a. (e[x] +r f[x])) = ((Σx ∈ a. e[x]) +r (Σx ∈ a. f[x])) ∈ |r|)

Lemma: rng_mssum_dom_shift
∀s:DSet. ∀r:Rng. ∀f:|s| ⟶ |r|. ∀p,q:MSet{s}.
  ((↑(p ⊆b q)) ⇒ (∀x:|s|. ((↑(x ∈b q - p)) ⇒ (f[x] = 0 ∈ |r|))) ⇒ ((Σx ∈ p. f[x]) = (Σx ∈ q. f[x]) ∈ |r|))

Definition: mod_mssum
Σm x ∈ a. f[x] ==  msFor{m↓grp} x ∈ a. f[x]

Lemma: mod_mssum_wf
∀s:DSet. ∀r:Rng. ∀m:r-Module. ∀f:|s| ⟶ m.car. ∀a:MSet{s}.  (Σm x ∈ a. f[x] ∈ m.car)

Lemma: comb_for_mod_mssum_wf
λs,r,m,f,a,z. Σm x ∈ a. f[x] ∈ s:DSet ⟶ r:Rng ⟶ m:r-Module ⟶ f:(|s| ⟶ m.car) ⟶ a:MSet{s} ⟶ (↓True) ⟶ m.car

Lemma: mod_mssum_functionality
∀s:DSet. ∀r:Rng. ∀m:r-Module. ∀f,f':|s| ⟶ m.car. ∀a,a':MSet{s}.
  ((a = a' ∈ MSet{s})
  ⇒ (∀x:|s|. ((↑(x ∈b a)) ⇒ (f[x] = f'[x] ∈ m.car)))
  ⇒ ((Σm x ∈ a. f[x]) = (Σm x ∈ a'. f'[x]) ∈ m.car))

Lemma: rng_fset_for_when_eq
∀s:DSet. ∀r:Rng. ∀f:|s| ⟶ |r|. ∀e:|s|. ∀as:FiniteSet{s}.
  ((↑(e ∈b as)) ⇒ ((Σx ∈ as. (when x (=b) e. f[x])) = f[e] ∈ |r|))

Lemma: mod_times_mssum_l
∀s:DSet. ∀r:Rng. ∀m:algebra{i:l}(r). ∀f:|s| ⟶ m.car. ∀u:m.car. ∀a:MSet{s}.
  ((u m.times (Σm x ∈ a. f[x])) = (Σm x ∈ a. (u m.times f[x])) ∈ m.car)

Lemma: mod_times_mssum_r
∀s:DSet. ∀r:Rng. ∀m:algebra{i:l}(r). ∀f:|s| ⟶ m.car. ∀u:m.car. ∀a:MSet{s}.
  (((Σm x ∈ a. f[x]) m.times u) = (Σm x ∈ a. (f[x] m.times u)) ∈ m.car)

Lemma: mod_action_mssum_l
∀s:DSet. ∀r:Rng. ∀m:r-Module. ∀f:|s| ⟶ m.car. ∀u:|r|. ∀a:MSet{s}.
  ((u m.act (Σm x ∈ a. f[x])) = (Σm x ∈ a. (u m.act f[x])) ∈ m.car)

Lemma: mod_action_mssum_r
∀s:DSet. ∀r:Rng. ∀m:r-Module. ∀f:|s| ⟶ |r|. ∀u:m.car. ∀a:MSet{s}.
  (((Σx ∈ a. f[x]) m.act u) = (Σm x ∈ a. (f[x] m.act u)) ∈ m.car)

Lemma: mod_action_when_l
∀r:Rng. ∀m:r-Module. ∀u:|r|. ∀x:m.car. ∀b:𝔹.  ((u m.act (when b. x)) = (when b. (u m.act x)) ∈ m.car)

Lemma: mod_action_when_r
∀r:Rng. ∀m:r-Module. ∀u:|r|. ∀x:m.car. ∀b:𝔹.  (((when b. u) m.act x) = (when b. (u m.act x)) ∈ m.car)

Lemma: mod_mssum_swap
∀r:Rng. ∀m:r-Module. ∀s,s':DSet. ∀f:|s| ⟶ |s'| ⟶ m.car. ∀a:MSet{s}. ∀b:MSet{s'}.
  ((Σm x ∈ a. Σm y ∈ b. f[x;y]) = (Σm y ∈ b. Σm x ∈ a. f[x;y]) ∈ m.car)



Home Index