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

Proof

Step	Hyp	Ref	Expression
1		gsumpropd2.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		gsumpropd2.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
3		gsumpropd2.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑋 )
4		gsumpropd2.b	⊢ ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐻 ) )
5		gsumpropd2.c	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ 𝐺 ) ∧ 𝑡 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) ∈ ( Base ‘ 𝐺 ) )
6		gsumpropd2.e	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ 𝐺 ) ∧ 𝑡 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) )
7		gsumpropd2.n	⊢ ( 𝜑 → Fun 𝐹 )
8		gsumpropd2.r	⊢ ( 𝜑 → ran 𝐹 ⊆ ( Base ‘ 𝐺 ) )
9		eqid	⊢ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) = ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) )
10		eqid	⊢ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) = ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) )
11	1 2 3 4 5 6 7 8 9 10	gsumpropd2lem	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐻 Σg 𝐹 ) )