Theorem 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	⊢ 𝑋 = ran 𝐺
	grpdiv.2	⊢ 𝑁 = ( inv ‘ 𝐺 )
	grpdiv.3	⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
Assertion	grpodivfval	⊢ ( 𝐺 ∈ GrpOp → 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		grpdiv.1	⊢ 𝑋 = ran 𝐺
2		grpdiv.2	⊢ 𝑁 = ( inv ‘ 𝐺 )
3		grpdiv.3	⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
4		rnexg	⊢ ( 𝐺 ∈ GrpOp → ran 𝐺 ∈ V )
5	1 4	eqeltrid	⊢ ( 𝐺 ∈ GrpOp → 𝑋 ∈ V )
6		mpoexga	⊢ ( ( 𝑋 ∈ V ∧ 𝑋 ∈ V ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) ∈ V )
7	5 5 6	syl2anc	⊢ ( 𝐺 ∈ GrpOp → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) ∈ V )
8		rneq	⊢ ( 𝑔 = 𝐺 → ran 𝑔 = ran 𝐺 )
9	8 1	eqtr4di	⊢ ( 𝑔 = 𝐺 → ran 𝑔 = 𝑋 )
10		id	⊢ ( 𝑔 = 𝐺 → 𝑔 = 𝐺 )
11		eqidd	⊢ ( 𝑔 = 𝐺 → 𝑥 = 𝑥 )
12		fveq2	⊢ ( 𝑔 = 𝐺 → ( inv ‘ 𝑔 ) = ( inv ‘ 𝐺 ) )
13	12 2	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( inv ‘ 𝑔 ) = 𝑁 )
14	13	fveq1d	⊢ ( 𝑔 = 𝐺 → ( ( inv ‘ 𝑔 ) ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) )
15	10 11 14	oveq123d	⊢ ( 𝑔 = 𝐺 → ( 𝑥 𝑔 ( ( inv ‘ 𝑔 ) ‘ 𝑦 ) ) = ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) )
16	9 9 15	mpoeq123dv	⊢ ( 𝑔 = 𝐺 → ( 𝑥 ∈ ran 𝑔 , 𝑦 ∈ ran 𝑔 ↦ ( 𝑥 𝑔 ( ( inv ‘ 𝑔 ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) )
17		df-gdiv	⊢ /𝑔 = ( 𝑔 ∈ GrpOp ↦ ( 𝑥 ∈ ran 𝑔 , 𝑦 ∈ ran 𝑔 ↦ ( 𝑥 𝑔 ( ( inv ‘ 𝑔 ) ‘ 𝑦 ) ) ) )
18	16 17	fvmptg	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) ∈ V ) → ( /𝑔 ‘ 𝐺 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) )
19	7 18	mpdan	⊢ ( 𝐺 ∈ GrpOp → ( /𝑔 ‘ 𝐺 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) )
20	3 19	syl5eq	⊢ ( 𝐺 ∈ GrpOp → 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) )