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 ( 𝜑𝐹𝑉 )
gsummgmpropd.g ( 𝜑𝐺𝑊 )
gsummgmpropd.h ( 𝜑𝐻𝑋 )
gsummgmpropd.b ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐻 ) )
gsummgmpropd.m ( 𝜑𝐺 ∈ Mgm )
gsummgmpropd.e ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ 𝐺 ) ∧ 𝑡 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑠 ( +g𝐺 ) 𝑡 ) = ( 𝑠 ( +g𝐻 ) 𝑡 ) )
gsummgmpropd.n ( 𝜑 → Fun 𝐹 )
gsummgmpropd.r ( 𝜑 → ran 𝐹 ⊆ ( Base ‘ 𝐺 ) )
Assertion gsummgmpropd ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐻 Σg 𝐹 ) )

Proof

Step Hyp Ref Expression
1 gsummgmpropd.f ( 𝜑𝐹𝑉 )
2 gsummgmpropd.g ( 𝜑𝐺𝑊 )
3 gsummgmpropd.h ( 𝜑𝐻𝑋 )
4 gsummgmpropd.b ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐻 ) )
5 gsummgmpropd.m ( 𝜑𝐺 ∈ Mgm )
6 gsummgmpropd.e ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ 𝐺 ) ∧ 𝑡 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑠 ( +g𝐺 ) 𝑡 ) = ( 𝑠 ( +g𝐻 ) 𝑡 ) )
7 gsummgmpropd.n ( 𝜑 → Fun 𝐹 )
8 gsummgmpropd.r ( 𝜑 → ran 𝐹 ⊆ ( Base ‘ 𝐺 ) )
9 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
10 eqid ( +g𝐺 ) = ( +g𝐺 )
11 9 10 mgmcl ( ( 𝐺 ∈ Mgm ∧ 𝑠 ∈ ( Base ‘ 𝐺 ) ∧ 𝑡 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑠 ( +g𝐺 ) 𝑡 ) ∈ ( Base ‘ 𝐺 ) )
12 11 3expib ( 𝐺 ∈ Mgm → ( ( 𝑠 ∈ ( Base ‘ 𝐺 ) ∧ 𝑡 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑠 ( +g𝐺 ) 𝑡 ) ∈ ( Base ‘ 𝐺 ) ) )
13 5 12 syl ( 𝜑 → ( ( 𝑠 ∈ ( Base ‘ 𝐺 ) ∧ 𝑡 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑠 ( +g𝐺 ) 𝑡 ) ∈ ( Base ‘ 𝐺 ) ) )
14 13 imp ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ 𝐺 ) ∧ 𝑡 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑠 ( +g𝐺 ) 𝑡 ) ∈ ( Base ‘ 𝐺 ) )
15 1 2 3 4 14 6 7 8 gsumpropd2 ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐻 Σg 𝐹 ) )