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

Metamath Proof Explorer

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