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

Metamath Proof Explorer

Theorem oppggrp

Description: The opposite of a group is a group. (Contributed by Stefan O'Rear, 26-Aug-2015)

Ref Expression
Hypothesis oppgbas.1 ⊢ 𝑂 = ( oppg ‘ 𝑅 )
Assertion oppggrp ( 𝑅 ∈ Grp → 𝑂 ∈ Grp )

Proof

Step Hyp Ref Expression
1 oppgbas.1 ⊢ 𝑂 = ( oppg ‘ 𝑅 )
2 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3 1 2 oppgbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
4 3 a1i ⊢ ( 𝑅 ∈ Grp → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 ) )
5 eqidd ⊢ ( 𝑅 ∈ Grp → ( +g ‘ 𝑂 ) = ( +g ‘ 𝑂 ) )
6 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
7 1 6 oppgid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑂 )
8 7 a1i ⊢ ( 𝑅 ∈ Grp → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑂 ) )
9 grpmnd ⊢ ( 𝑅 ∈ Grp → 𝑅 ∈ Mnd )
10 1 oppgmnd ⊢ ( 𝑅 ∈ Mnd → 𝑂 ∈ Mnd )
11 9 10 syl ⊢ ( 𝑅 ∈ Grp → 𝑂 ∈ Mnd )
12 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
13 2 12 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
14 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
15 eqid ⊢ ( +g ‘ 𝑂 ) = ( +g ‘ 𝑂 )
16 14 1 15 oppgplus ⊢ ( ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑂 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) )
17 2 14 6 12 grprinv ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ) = ( 0g ‘ 𝑅 ) )
18 16 17 eqtrid ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑂 ) 𝑥 ) = ( 0g ‘ 𝑅 ) )
19 4 5 8 11 13 18 isgrpd2 ⊢ ( 𝑅 ∈ Grp → 𝑂 ∈ Grp )