Theorem grpinvf

Description: The group inversion operation is a function on the base set. (Contributed by Mario Carneiro, 4-May-2015)

	Ref	Expression
Hypotheses	grpinvcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grpinvcl.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
Assertion	grpinvf	⊢ ( 𝐺 ∈ Grp → 𝑁 : 𝐵 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		grpinvcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grpinvcl.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
3		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
4		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
5	1 3 4	grpinveu	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ∃! 𝑦 ∈ 𝐵 ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) )
6		riotacl	⊢ ( ∃! 𝑦 ∈ 𝐵 ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) → ( ℩ 𝑦 ∈ 𝐵 ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) ∈ 𝐵 )
7	5 6	syl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( ℩ 𝑦 ∈ 𝐵 ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) ∈ 𝐵 )
8	1 3 4 2	grpinvfval	⊢ 𝑁 = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
9	7 8	fmptd	⊢ ( 𝐺 ∈ Grp → 𝑁 : 𝐵 ⟶ 𝐵 )