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 = {Base}_{G}$
	grpsubval.p	$⊢ \underset{˙}{+} = +_{G}$
	grpsubval.i	$⊢ I = {inv}_{g} (G)$
	grpsubval.m	$⊢ \underset{˙}{-} = -_{G}$
Assertion	grpsubval	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{-} Y = X \underset{˙}{+} I (Y)$

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

Metamath Proof Explorer