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

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 ⊢ φ → Base G = Base H
gsumpropd2.c ⊢ φ ∧ s ∈ Base G ∧ t ∈ Base G → s + G t ∈ Base G
gsumpropd2.e ⊢ φ ∧ s ∈ Base G ∧ t ∈ Base G → s + G t = s + H t
gsumpropd2.n ⊢ φ → Fun ⁡ F
gsumpropd2.r ⊢ φ → ran ⁡ F ⊆ Base G
Assertion gsumpropd2 ⊢ φ → ∑ G F = ∑ H F

Proof

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