This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑂 ) )