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 ‘ 𝐻 ) )