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

Metamath Proof Explorer

Theorem grpsubpropd

Description: Weak property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 27-Mar-2015)

Ref Expression
Hypotheses grpsubpropd.b ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐻 ) )
grpsubpropd.p ⊢ ( 𝜑 → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) )
Assertion grpsubpropd ( 𝜑 → ( -g ‘ 𝐺 ) = ( -g ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 grpsubpropd.b ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐻 ) )
2 grpsubpropd.p ⊢ ( 𝜑 → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) )
3 eqidd ⊢ ( 𝜑 → 𝑎 = 𝑎 )
4 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
5 2 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) )
6 4 1 5 grpinvpropd ⊢ ( 𝜑 → ( invg ‘ 𝐺 ) = ( invg ‘ 𝐻 ) )
7 6 fveq1d ⊢ ( 𝜑 → ( ( invg ‘ 𝐺 ) ‘ 𝑏 ) = ( ( invg ‘ 𝐻 ) ‘ 𝑏 ) )
8 2 3 7 oveq123d ⊢ ( 𝜑 → ( 𝑎 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑏 ) ) = ( 𝑎 ( +g ‘ 𝐻 ) ( ( invg ‘ 𝐻 ) ‘ 𝑏 ) ) )
9 1 1 8 mpoeq123dv ⊢ ( 𝜑 → ( 𝑎 ∈ ( Base ‘ 𝐺 ) , 𝑏 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑏 ) ) ) = ( 𝑎 ∈ ( Base ‘ 𝐻 ) , 𝑏 ∈ ( Base ‘ 𝐻 ) ↦ ( 𝑎 ( +g ‘ 𝐻 ) ( ( invg ‘ 𝐻 ) ‘ 𝑏 ) ) ) )
10 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
11 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
12 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
13 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
14 10 11 12 13 grpsubfval ⊢ ( -g ‘ 𝐺 ) = ( 𝑎 ∈ ( Base ‘ 𝐺 ) , 𝑏 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑏 ) ) )
15 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
16 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
17 eqid ⊢ ( invg ‘ 𝐻 ) = ( invg ‘ 𝐻 )
18 eqid ⊢ ( -g ‘ 𝐻 ) = ( -g ‘ 𝐻 )
19 15 16 17 18 grpsubfval ⊢ ( -g ‘ 𝐻 ) = ( 𝑎 ∈ ( Base ‘ 𝐻 ) , 𝑏 ∈ ( Base ‘ 𝐻 ) ↦ ( 𝑎 ( +g ‘ 𝐻 ) ( ( invg ‘ 𝐻 ) ‘ 𝑏 ) ) )
20 9 14 19 3eqtr4g ⊢ ( 𝜑 → ( -g ‘ 𝐺 ) = ( -g ‘ 𝐻 ) )