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 𝐹 ) )