Metamath Proof Explorer

Theorem gsumpropd2

Description: A stronger version of gsumpropd , working for magma, where only the closure of the addition operation on a common base is required, see gsummgmpropd . (Contributed by Thierry Arnoux, 28-Jun-2017)

Ref Expression
Hypotheses gsumpropd2.f ⊢φ→F∈V
gsumpropd2.g ⊢φ→G∈W
gsumpropd2.h ⊢φ→H∈X
gsumpropd2.b ⊢φ→BaseG=BaseH
gsumpropd2.c ⊢φ∧s∈BaseG∧t∈BaseG→s+Gt∈BaseG
gsumpropd2.e ⊢φ∧s∈BaseG∧t∈BaseG→s+Gt=s+Ht
gsumpropd2.n ⊢φ→Fun⁡F
gsumpropd2.r ⊢φ→ran⁡F⊆BaseG
Assertion gsumpropd2 ⊢φ→∑GF=∑HF

Proof

Step Hyp Ref Expression
1 gsumpropd2.f ⊢φ→F∈V
2 gsumpropd2.g ⊢φ→G∈W
3 gsumpropd2.h ⊢φ→H∈X
4 gsumpropd2.b ⊢φ→BaseG=BaseH
5 gsumpropd2.c ⊢φ∧s∈BaseG∧t∈BaseG→s+Gt∈BaseG
6 gsumpropd2.e ⊢φ∧s∈BaseG∧t∈BaseG→s+Gt=s+Ht
7 gsumpropd2.n ⊢φ→Fun⁡F
8 gsumpropd2.r ⊢φ→ran⁡F⊆BaseG
9 eqid ⊢F-1V∖s∈BaseG|∀t∈BaseGs+Gt=t∧t+Gs=t=F-1V∖s∈BaseG|∀t∈BaseGs+Gt=t∧t+Gs=t
10 eqid ⊢F-1V∖s∈BaseH|∀t∈BaseHs+Ht=t∧t+Hs=t=F-1V∖s∈BaseH|∀t∈BaseHs+Ht=t∧t+Hs=t
11 1 2 3 4 5 6 7 8 9 10 gsumpropd2lem ⊢φ→∑GF=∑HF