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

Metamath Proof Explorer

Theorem gsummgmpropd

Description: A stronger version of gsumpropd if at least one of the involved structures is a magma, see gsumpropd2 . (Contributed by AV, 31-Jan-2020)

Ref Expression
Hypotheses gsummgmpropd.f ⊢ φ → F ∈ V
gsummgmpropd.g ⊢ φ → G ∈ W
gsummgmpropd.h ⊢ φ → H ∈ X
gsummgmpropd.b ⊢ φ → Base G = Base H
gsummgmpropd.m ⊢ φ → G ∈ Mgm
gsummgmpropd.e ⊢ φ ∧ s ∈ Base G ∧ t ∈ Base G → s + G t = s + H t
gsummgmpropd.n ⊢ φ → Fun ⁡ F
gsummgmpropd.r ⊢ φ → ran ⁡ F ⊆ Base G
Assertion gsummgmpropd ⊢ φ → ∑ G F = ∑ H F

Proof

Step Hyp Ref Expression
1 gsummgmpropd.f ⊢ φ → F ∈ V
2 gsummgmpropd.g ⊢ φ → G ∈ W
3 gsummgmpropd.h ⊢ φ → H ∈ X
4 gsummgmpropd.b ⊢ φ → Base G = Base H
5 gsummgmpropd.m ⊢ φ → G ∈ Mgm
6 gsummgmpropd.e ⊢ φ ∧ s ∈ Base G ∧ t ∈ Base G → s + G t = s + H t
7 gsummgmpropd.n ⊢ φ → Fun ⁡ F
8 gsummgmpropd.r ⊢ φ → ran ⁡ F ⊆ Base G
9 eqid ⊢ Base G = Base G
10 eqid ⊢ + G = + G
11 9 10 mgmcl ⊢ G ∈ Mgm ∧ s ∈ Base G ∧ t ∈ Base G → s + G t ∈ Base G
12 11 3expib ⊢ G ∈ Mgm → s ∈ Base G ∧ t ∈ Base G → s + G t ∈ Base G
13 5 12 syl ⊢ φ → s ∈ Base G ∧ t ∈ Base G → s + G t ∈ Base G
14 13 imp ⊢ φ ∧ s ∈ Base G ∧ t ∈ Base G → s + G t ∈ Base G
15 1 2 3 4 14 6 7 8 gsumpropd2 ⊢ φ → ∑ G F = ∑ H F