Theorem invoppggim

Description: The inverse is an antiautomorphism on any group. (Contributed by Stefan O'Rear, 26-Aug-2015)

	Ref	Expression
Hypotheses	invoppggim.o	⊢ 𝑂 = ( oppg ‘ 𝐺 )
	invoppggim.i	⊢ 𝐼 = ( invg ‘ 𝐺 )
Assertion	invoppggim	⊢ ( 𝐺 ∈ Grp → 𝐼 ∈ ( 𝐺 GrpIso 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		invoppggim.o	⊢ 𝑂 = ( oppg ‘ 𝐺 )
2		invoppggim.i	⊢ 𝐼 = ( invg ‘ 𝐺 )
3		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4	1 3	oppgbas	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝑂 )
5		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
6		eqid	⊢ ( +g ‘ 𝑂 ) = ( +g ‘ 𝑂 )
7		id	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Grp )
8	1	oppggrp	⊢ ( 𝐺 ∈ Grp → 𝑂 ∈ Grp )
9	3 2	grpinvf	⊢ ( 𝐺 ∈ Grp → 𝐼 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐺 ) )
10	3 5 2	grpinvadd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐼 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝐼 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑥 ) ) )
11	10	3expb	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝐼 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝐼 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑥 ) ) )
12	5 1 6	oppgplus	⊢ ( ( 𝐼 ‘ 𝑥 ) ( +g ‘ 𝑂 ) ( 𝐼 ‘ 𝑦 ) ) = ( ( 𝐼 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑥 ) )
13	11 12	syl6eqr	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝐼 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝐼 ‘ 𝑥 ) ( +g ‘ 𝑂 ) ( 𝐼 ‘ 𝑦 ) ) )
14	3 4 5 6 7 8 9 13	isghmd	⊢ ( 𝐺 ∈ Grp → 𝐼 ∈ ( 𝐺 GrpHom 𝑂 ) )
15	3 2 7	grpinvf1o	⊢ ( 𝐺 ∈ Grp → 𝐼 : ( Base ‘ 𝐺 ) –1-1-onto→ ( Base ‘ 𝐺 ) )
16	3 4	isgim	⊢ ( 𝐼 ∈ ( 𝐺 GrpIso 𝑂 ) ↔ ( 𝐼 ∈ ( 𝐺 GrpHom 𝑂 ) ∧ 𝐼 : ( Base ‘ 𝐺 ) –1-1-onto→ ( Base ‘ 𝐺 ) ) )
17	14 15 16	sylanbrc	⊢ ( 𝐺 ∈ Grp → 𝐼 ∈ ( 𝐺 GrpIso 𝑂 ) )