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	syl5eq	⊢ ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑂 ) 𝑥 ) = ( 0g ‘ 𝑅 ) )
19	4 5 8 11 13 18	isgrpd2	⊢ ( 𝑅 ∈ Grp → 𝑂 ∈ Grp )