Theorem grpoinvfval

Description: The inverse function of a group. (Contributed by NM, 26-Oct-2006) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpinvfval.1	⊢ 𝑋 = ran 𝐺
	grpinvfval.2	⊢ 𝑈 = ( GId ‘ 𝐺 )
	grpinvfval.3	⊢ 𝑁 = ( inv ‘ 𝐺 )
Assertion	grpoinvfval	⊢ ( 𝐺 ∈ GrpOp → 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) )

Proof

Step	Hyp	Ref	Expression
1		grpinvfval.1	⊢ 𝑋 = ran 𝐺
2		grpinvfval.2	⊢ 𝑈 = ( GId ‘ 𝐺 )
3		grpinvfval.3	⊢ 𝑁 = ( inv ‘ 𝐺 )
4		rnexg	⊢ ( 𝐺 ∈ GrpOp → ran 𝐺 ∈ V )
5	1 4	eqeltrid	⊢ ( 𝐺 ∈ GrpOp → 𝑋 ∈ V )
6		mptexg	⊢ ( 𝑋 ∈ V → ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) ∈ V )
7	5 6	syl	⊢ ( 𝐺 ∈ GrpOp → ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) ∈ V )
8		rneq	⊢ ( 𝑔 = 𝐺 → ran 𝑔 = ran 𝐺 )
9	8 1	eqtr4di	⊢ ( 𝑔 = 𝐺 → ran 𝑔 = 𝑋 )
10		oveq	⊢ ( 𝑔 = 𝐺 → ( 𝑦 𝑔 𝑥 ) = ( 𝑦 𝐺 𝑥 ) )
11		fveq2	⊢ ( 𝑔 = 𝐺 → ( GId ‘ 𝑔 ) = ( GId ‘ 𝐺 ) )
12	11 2	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( GId ‘ 𝑔 ) = 𝑈 )
13	10 12	eqeq12d	⊢ ( 𝑔 = 𝐺 → ( ( 𝑦 𝑔 𝑥 ) = ( GId ‘ 𝑔 ) ↔ ( 𝑦 𝐺 𝑥 ) = 𝑈 ) )
14	9 13	riotaeqbidv	⊢ ( 𝑔 = 𝐺 → ( ℩ 𝑦 ∈ ran 𝑔 ( 𝑦 𝑔 𝑥 ) = ( GId ‘ 𝑔 ) ) = ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) )
15	9 14	mpteq12dv	⊢ ( 𝑔 = 𝐺 → ( 𝑥 ∈ ran 𝑔 ↦ ( ℩ 𝑦 ∈ ran 𝑔 ( 𝑦 𝑔 𝑥 ) = ( GId ‘ 𝑔 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) )
16		df-ginv	⊢ inv = ( 𝑔 ∈ GrpOp ↦ ( 𝑥 ∈ ran 𝑔 ↦ ( ℩ 𝑦 ∈ ran 𝑔 ( 𝑦 𝑔 𝑥 ) = ( GId ‘ 𝑔 ) ) ) )
17	15 16	fvmptg	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) ∈ V ) → ( inv ‘ 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) )
18	7 17	mpdan	⊢ ( 𝐺 ∈ GrpOp → ( inv ‘ 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) )
19	3 18	syl5eq	⊢ ( 𝐺 ∈ GrpOp → 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) )