---

Step * 1 1 1 of Lemma bag-summation-equal-implies-all-equal-1


1. Assoc(ℤ;λx,y. (x + y))
2. Comm(ℤ;λx,y. (x + y))
3. T : Type
4. f : T ⟶ ℤ
5. g : T ⟶ ℤ
6. x : T
7. u : T
8. v : T List
9. (∀x:T. (x ↓∈ v ⇒ (f[x] ≤ g[x]))) ⇒ (Σ(x∈v). g[x] ≤ Σ(x∈v). f[x]) ⇒ x ↓∈ v ⇒ (f[x] = g[x] ∈ ℤ)
10. ∀x:T. (x ↓∈ u.v ⇒ (f[x] ≤ g[x]))
11. (g[u] + Σ(x∈v). g[x]) ≤ (f[u] + Σ(x∈v). f[x])
12. (x = u ∈ T) ↓∨ x ↓∈ v
13. IsMonoid(ℤ;λx,y. (x + y);0)
⊢ f[x] = g[x] ∈ ℤ
BY
{ ((Assert f[u] ≤ g[u] BY
          (BackThruSomeHyp THEN BagMemberD 0 THEN Auto))
   THEN (Assert Σ(x∈v). g[x] ≤ Σ(x∈v). f[x] BY
               Auto)
   ) }

1
1. Assoc(ℤ;λx,y. (x + y))
2. Comm(ℤ;λx,y. (x + y))
3. T : Type
4. f : T ⟶ ℤ
5. g : T ⟶ ℤ
6. x : T
7. u : T
8. v : T List
9. (∀x:T. (x ↓∈ v ⇒ (f[x] ≤ g[x]))) ⇒ (Σ(x∈v). g[x] ≤ Σ(x∈v). f[x]) ⇒ x ↓∈ v ⇒ (f[x] = g[x] ∈ ℤ)
10. ∀x:T. (x ↓∈ u.v ⇒ (f[x] ≤ g[x]))
11. (g[u] + Σ(x∈v). g[x]) ≤ (f[u] + Σ(x∈v). f[x])
12. (x = u ∈ T) ↓∨ x ↓∈ v
13. IsMonoid(ℤ;λx,y. (x + y);0)
14. f[u] ≤ g[u]
15. Σ(x∈v). g[x] ≤ Σ(x∈v). f[x]
⊢ f[x] = g[x] ∈ ℤ

---

Latex:

---

Latex:

1.  Assoc(\mBbbZ{};\mlambda{}x,y.  (x  +  y))
2.  Comm(\mBbbZ{};\mlambda{}x,y.  (x  +  y))
3.  T  :  Type
4.  f  :  T  {}\mrightarrow{}  \mBbbZ{}
5.  g  :  T  {}\mrightarrow{}  \mBbbZ{}
6.  x  :  T
7.  u  :  T
8.  v  :  T  List
9.  (\mforall{}x:T.  (x  \mdownarrow{}\mmember{}  v  {}\mRightarrow{}  (f[x]  \mleq{}  g[x])))  {}\mRightarrow{}  (\mSigma{}(x\mmember{}v).  g[x]  \mleq{}  \mSigma{}(x\mmember{}v).  f[x])  {}\mRightarrow{}  x  \mdownarrow{}\mmember{}  v  {}\mRightarrow{}  (f[x]  =  g[x])
10.  \mforall{}x:T.  (x  \mdownarrow{}\mmember{}  u.v  {}\mRightarrow{}  (f[x]  \mleq{}  g[x]))
11.  (g[u]  +  \mSigma{}(x\mmember{}v).  g[x])  \mleq{}  (f[u]  +  \mSigma{}(x\mmember{}v).  f[x])
12.  (x  =  u)  \mdownarrow{}\mvee{}  x  \mdownarrow{}\mmember{}  v
13.  IsMonoid(\mBbbZ{};\mlambda{}x,y.  (x  +  y);0)
\mvdash{}  f[x]  =  g[x]


By

---

Latex:
((Assert  f[u]  \mleq{}  g[u]  BY
                (BackThruSomeHyp  THEN  BagMemberD  0  THEN  Auto))
  THEN  (Assert  \mSigma{}(x\mmember{}v).  g[x]  \mleq{}  \mSigma{}(x\mmember{}v).  f[x]  BY
                          Auto)
  )

---

Home Index