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 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
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 𝐹 ) )