Theorem oppginv

Description: Inverses in a group are a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015)

	Ref	Expression
Hypotheses	oppgbas.1	⊢ 𝑂 = ( oppg ‘ 𝑅 )
	oppginv.2	⊢ 𝐼 = ( invg ‘ 𝑅 )
Assertion	oppginv	⊢ ( 𝑅 ∈ Grp → 𝐼 = ( invg ‘ 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		oppgbas.1	⊢ 𝑂 = ( oppg ‘ 𝑅 )
2		oppginv.2	⊢ 𝐼 = ( invg ‘ 𝑅 )
3		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4	3 2	grpinvf	⊢ ( 𝑅 ∈ Grp → 𝐼 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
5		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
6		eqid	⊢ ( +g ‘ 𝑂 ) = ( +g ‘ 𝑂 )
7	5 1 6	oppgplus	⊢ ( ( 𝐼 ‘ 𝑥 ) ( +g ‘ 𝑂 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑅 ) ( 𝐼 ‘ 𝑥 ) )
8		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
9	3 5 8 2	grprinv	⊢ ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) ( 𝐼 ‘ 𝑥 ) ) = ( 0g ‘ 𝑅 ) )
10	7 9	syl5eq	⊢ ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐼 ‘ 𝑥 ) ( +g ‘ 𝑂 ) 𝑥 ) = ( 0g ‘ 𝑅 ) )
11	10	ralrimiva	⊢ ( 𝑅 ∈ Grp → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝐼 ‘ 𝑥 ) ( +g ‘ 𝑂 ) 𝑥 ) = ( 0g ‘ 𝑅 ) )
12	1	oppggrp	⊢ ( 𝑅 ∈ Grp → 𝑂 ∈ Grp )
13	1 3	oppgbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
14	1 8	oppgid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑂 )
15		eqid	⊢ ( invg ‘ 𝑂 ) = ( invg ‘ 𝑂 )
16	13 6 14 15	isgrpinv	⊢ ( 𝑂 ∈ Grp → ( ( 𝐼 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝐼 ‘ 𝑥 ) ( +g ‘ 𝑂 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ) ↔ ( invg ‘ 𝑂 ) = 𝐼 ) )
17	12 16	syl	⊢ ( 𝑅 ∈ Grp → ( ( 𝐼 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝐼 ‘ 𝑥 ) ( +g ‘ 𝑂 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ) ↔ ( invg ‘ 𝑂 ) = 𝐼 ) )
18	4 11 17	mpbi2and	⊢ ( 𝑅 ∈ Grp → ( invg ‘ 𝑂 ) = 𝐼 )
19	18	eqcomd	⊢ ( 𝑅 ∈ Grp → 𝐼 = ( invg ‘ 𝑂 ) )