Theorem grpsubval

Description: Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014) (Revised by Mario Carneiro, 13-Dec-2014)

	Ref	Expression
Hypotheses	grpsubval.b	$$⊢B={\mathrm{Base}}_G$$
	grpsubval.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	grpsubval.i	$$⊢I={inv}_g\left(G\right)$$
	grpsubval.m	$$⊢\underset{\dot{}}{-}={-}_G$$
Assertion	grpsubval	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{-}Y=X\underset{\dot{}}{+}I\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		grpsubval.b	$$⊢B={\mathrm{Base}}_G$$
2		grpsubval.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grpsubval.i	$$⊢I={inv}_g\left(G\right)$$
4		grpsubval.m	$$⊢\underset{\dot{}}{-}={-}_G$$
5		oveq1	$$⊢x=X\to x\underset{\dot{}}{+}I\left(y\right)=X\underset{\dot{}}{+}I\left(y\right)$$
6		fveq2	$$⊢y=Y\to I\left(y\right)=I\left(Y\right)$$
7	6	oveq2d	$$⊢y=Y\to X\underset{\dot{}}{+}I\left(y\right)=X\underset{\dot{}}{+}I\left(Y\right)$$
8	1 2 3 4	grpsubfval	$$⊢\underset{\dot{}}{-}=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}I\left(y\right)\right)$$
9		ovex	$$⊢X\underset{\dot{}}{+}I\left(Y\right)\in \mathrm{V}$$
10	5 7 8 9	ovmpo	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{-}Y=X\underset{\dot{}}{+}I\left(Y\right)$$