Theorem oppggrpb

Description: Bidirectional form of oppggrp . (Contributed by Stefan O'Rear, 26-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		oppgbas.1	⊢ 𝑂 = ( oppg ‘ 𝑅 )
2	1	oppggrp	⊢ ( 𝑅 ∈ Grp → 𝑂 ∈ Grp )
3		eqid	⊢ ( oppg ‘ 𝑂 ) = ( oppg ‘ 𝑂 )
4	3	oppggrp	⊢ ( 𝑂 ∈ Grp → ( oppg ‘ 𝑂 ) ∈ Grp )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6	1 5	oppgbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
7	3 6	oppgbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( oppg ‘ 𝑂 ) )
8	7	a1i	⊢ ( ⊤ → ( Base ‘ 𝑅 ) = ( Base ‘ ( oppg ‘ 𝑂 ) ) )
9		eqidd	⊢ ( ⊤ → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
10		eqid	⊢ ( +g ‘ 𝑂 ) = ( +g ‘ 𝑂 )
11		eqid	⊢ ( +g ‘ ( oppg ‘ 𝑂 ) ) = ( +g ‘ ( oppg ‘ 𝑂 ) )
12	10 3 11	oppgplus	⊢ ( 𝑥 ( +g ‘ ( oppg ‘ 𝑂 ) ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 )
13		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
14	13 1 10	oppgplus	⊢ ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 )
15	12 14	eqtri	⊢ ( 𝑥 ( +g ‘ ( oppg ‘ 𝑂 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 )
16	15	a1i	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( +g ‘ ( oppg ‘ 𝑂 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) )
17	8 9 16	grppropd	⊢ ( ⊤ → ( ( oppg ‘ 𝑂 ) ∈ Grp ↔ 𝑅 ∈ Grp ) )
18	17	mptru	⊢ ( ( oppg ‘ 𝑂 ) ∈ Grp ↔ 𝑅 ∈ Grp )
19	4 18	sylib	⊢ ( 𝑂 ∈ Grp → 𝑅 ∈ Grp )
20	2 19	impbii	⊢ ( 𝑅 ∈ Grp ↔ 𝑂 ∈ Grp )