Theorem grpoinvval

Description: The inverse of a group element. (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	grpoinvval	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) = ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		grpinvfval.1	⊢ 𝑋 = ran 𝐺
2		grpinvfval.2	⊢ 𝑈 = ( GId ‘ 𝐺 )
3		grpinvfval.3	⊢ 𝑁 = ( inv ‘ 𝐺 )
4	1 2 3	grpoinvfval	⊢ ( 𝐺 ∈ GrpOp → 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) )
5	4	fveq1d	⊢ ( 𝐺 ∈ GrpOp → ( 𝑁 ‘ 𝐴 ) = ( ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) ‘ 𝐴 ) )
6		oveq2	⊢ ( 𝑥 = 𝐴 → ( 𝑦 𝐺 𝑥 ) = ( 𝑦 𝐺 𝐴 ) )
7	6	eqeq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 𝐺 𝑥 ) = 𝑈 ↔ ( 𝑦 𝐺 𝐴 ) = 𝑈 ) )
8	7	riotabidv	⊢ ( 𝑥 = 𝐴 → ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) = ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 ) )
9		eqid	⊢ ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) )
10		riotaex	⊢ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 ) ∈ V
11	8 9 10	fvmpt	⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) ‘ 𝐴 ) = ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 ) )
12	5 11	sylan9eq	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) = ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 ) )