Theorem grpsubpropd

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

	Ref	Expression
Hypotheses	grpsubpropd.b	$$⊢\phi \to {\mathrm{Base}}_G={\mathrm{Base}}_H$$
	grpsubpropd.p	$$⊢\phi \to {+}_G={+}_H$$
Assertion	grpsubpropd	$$⊢\phi \to {-}_G={-}_H$$

Proof

Step	Hyp	Ref	Expression
1		grpsubpropd.b	$$⊢\phi \to {\mathrm{Base}}_G={\mathrm{Base}}_H$$
2		grpsubpropd.p	$$⊢\phi \to {+}_G={+}_H$$
3		eqidd	$$⊢\phi \to a=a$$
4		eqidd	$$⊢\phi \to {\mathrm{Base}}_G={\mathrm{Base}}_G$$
5	2	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\right)\to x{+}_{G}y=x{+}_{H}y$$
6	4 1 5	grpinvpropd	$$⊢\phi \to {inv}_g\left(G\right)={inv}_g\left(H\right)$$
7	6	fveq1d	$$⊢\phi \to {inv}_g\left(G\right)\left(b\right)={inv}_g\left(H\right)\left(b\right)$$
8	2 3 7	oveq123d	$$⊢\phi \to a{+}_G{inv}_g\left(G\right)\left(b\right)=a{+}_H{inv}_g\left(H\right)\left(b\right)$$
9	1 1 8	mpoeq123dv	$$⊢\phi \to \left(a\in {\mathrm{Base}}_G,b\in {\mathrm{Base}}_G⟼a{+}_G{inv}_g\left(G\right)\left(b\right)\right)=\left(a\in {\mathrm{Base}}_H,b\in {\mathrm{Base}}_H⟼a{+}_H{inv}_g\left(H\right)\left(b\right)\right)$$
10		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
11		eqid	$$⊢{+}_G={+}_G$$
12		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
13		eqid	$$⊢{-}_G={-}_G$$
14	10 11 12 13	grpsubfval	$$⊢{-}_G=\left(a\in {\mathrm{Base}}_G,b\in {\mathrm{Base}}_G⟼a{+}_G{inv}_g\left(G\right)\left(b\right)\right)$$
15		eqid	$$⊢{\mathrm{Base}}_H={\mathrm{Base}}_H$$
16		eqid	$$⊢{+}_H={+}_H$$
17		eqid	$$⊢{inv}_g\left(H\right)={inv}_g\left(H\right)$$
18		eqid	$$⊢{-}_H={-}_H$$
19	15 16 17 18	grpsubfval	$$⊢{-}_H=\left(a\in {\mathrm{Base}}_H,b\in {\mathrm{Base}}_H⟼a{+}_H{inv}_g\left(H\right)\left(b\right)\right)$$
20	9 14 19	3eqtr4g	$$⊢\phi \to {-}_G={-}_H$$