grpodivfval

Description: Group division (or subtraction) operation. (Contributed by NM, 15-Feb-2008) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpdiv.1	$⊢ X = ran G$
	grpdiv.2	$⊢ N = inv (G)$
	grpdiv.3	$⊢ D = /_{g} (G)$
Assertion	grpodivfval	$⊢ G \in GrpOp \to D = (x \in X, y \in X ⟼ x G N (y))$

Proof

Step	Hyp	Ref	Expression
1		grpdiv.1	$⊢ X = ran G$
2		grpdiv.2	$⊢ N = inv (G)$
3		grpdiv.3	$⊢ D = /_{g} (G)$
4		rnexg	$⊢ G \in GrpOp \to ran G \in V$
5	1 4	eqeltrid	$⊢ G \in GrpOp \to X \in V$
6		mpoexga	$⊢ (X \in V \land X \in V) \to (x \in X, y \in X ⟼ x G N (y)) \in V$
7	5 5 6	syl2anc	$⊢ G \in GrpOp \to (x \in X, y \in X ⟼ x G N (y)) \in V$
8		rneq	$⊢ g = G \to ran g = ran G$
9	8 1	eqtr4di	$⊢ g = G \to ran g = X$
10		id	$⊢ g = G \to g = G$
11		eqidd	$⊢ g = G \to x = x$
12		fveq2	$⊢ g = G \to inv (g) = inv (G)$
13	12 2	eqtr4di	$⊢ g = G \to inv (g) = N$
14	13	fveq1d	$⊢ g = G \to inv (g) (y) = N (y)$
15	10 11 14	oveq123d	$⊢ g = G \to x g inv (g) (y) = x G N (y)$
16	9 9 15	mpoeq123dv	$⊢ g = G \to (x \in ran g, y \in ran g ⟼ x g inv (g) (y)) = (x \in X, y \in X ⟼ x G N (y))$
17		df-gdiv	$⊢ /_{g} = (g \in GrpOp ⟼ (x \in ran g, y \in ran g ⟼ x g inv (g) (y)))$
18	16 17	fvmptg	$⊢ (G \in GrpOp \land (x \in X, y \in X ⟼ x G N (y)) \in V) \to /_{g} (G) = (x \in X, y \in X ⟼ x G N (y))$
19	7 18	mpdan	$⊢ G \in GrpOp \to /_{g} (G) = (x \in X, y \in X ⟼ x G N (y))$
20	3 19	syl5eq	$⊢ G \in GrpOp \to D = (x \in X, y \in X ⟼ x G N (y))$

Metamath Proof Explorer

Theorem grpodivfval

Proof