Metamath Proof Explorer


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 eqtr4di ( ( 𝐺 ∈ 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 𝑂 ) )