Theorem grpoinvop

Description: The inverse of the group operation reverses the arguments. Lemma 2.2.1(d) of Herstein p. 55. (Contributed by NM, 27-Oct-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpasscan1.1	⊢ 𝑋 = ran 𝐺
	grpasscan1.2	⊢ 𝑁 = ( inv ‘ 𝐺 )
Assertion	grpoinvop	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) = ( ( 𝑁 ‘ 𝐵 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		grpasscan1.1	⊢ 𝑋 = ran 𝐺
2		grpasscan1.2	⊢ 𝑁 = ( inv ‘ 𝐺 )
3		simp1	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐺 ∈ GrpOp )
4		simp2	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
5		simp3	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
6	1 2	grpoinvcl	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) ∈ 𝑋 )
7	6	3adant2	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) ∈ 𝑋 )
8	1 2	grpoinvcl	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 )
9	8	3adant3	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 )
10	1	grpocl	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑁 ‘ 𝐵 ) ∈ 𝑋 ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐵 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) ∈ 𝑋 )
11	3 7 9 10	syl3anc	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐵 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) ∈ 𝑋 )
12	1	grpoass	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝑁 ‘ 𝐵 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( 𝑁 ‘ 𝐵 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) ) = ( 𝐴 𝐺 ( 𝐵 𝐺 ( ( 𝑁 ‘ 𝐵 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) ) ) )
13	3 4 5 11 12	syl13anc	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( 𝑁 ‘ 𝐵 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) ) = ( 𝐴 𝐺 ( 𝐵 𝐺 ( ( 𝑁 ‘ 𝐵 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) ) ) )
14		eqid	⊢ ( GId ‘ 𝐺 ) = ( GId ‘ 𝐺 )
15	1 14 2	grporinv	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝐺 ( 𝑁 ‘ 𝐵 ) ) = ( GId ‘ 𝐺 ) )
16	15	3adant2	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝐺 ( 𝑁 ‘ 𝐵 ) ) = ( GId ‘ 𝐺 ) )
17	16	oveq1d	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐵 𝐺 ( 𝑁 ‘ 𝐵 ) ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) = ( ( GId ‘ 𝐺 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) )
18	1	grpoass	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝐵 ) ∈ 𝑋 ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 ) ) → ( ( 𝐵 𝐺 ( 𝑁 ‘ 𝐵 ) ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) = ( 𝐵 𝐺 ( ( 𝑁 ‘ 𝐵 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) ) )
19	3 5 7 9 18	syl13anc	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐵 𝐺 ( 𝑁 ‘ 𝐵 ) ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) = ( 𝐵 𝐺 ( ( 𝑁 ‘ 𝐵 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) ) )
20	1 14	grpolid	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 ) → ( ( GId ‘ 𝐺 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) = ( 𝑁 ‘ 𝐴 ) )
21	8 20	syldan	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( GId ‘ 𝐺 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) = ( 𝑁 ‘ 𝐴 ) )
22	21	3adant3	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( GId ‘ 𝐺 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) = ( 𝑁 ‘ 𝐴 ) )
23	17 19 22	3eqtr3d	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝐺 ( ( 𝑁 ‘ 𝐵 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) ) = ( 𝑁 ‘ 𝐴 ) )
24	23	oveq2d	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( 𝐵 𝐺 ( ( 𝑁 ‘ 𝐵 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) ) ) = ( 𝐴 𝐺 ( 𝑁 ‘ 𝐴 ) ) )
25	1 14 2	grporinv	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 ( 𝑁 ‘ 𝐴 ) ) = ( GId ‘ 𝐺 ) )
26	25	3adant3	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( 𝑁 ‘ 𝐴 ) ) = ( GId ‘ 𝐺 ) )
27	13 24 26	3eqtrd	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( 𝑁 ‘ 𝐵 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) ) = ( GId ‘ 𝐺 ) )
28	1	grpocl	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
29	1 14 2	grpoinvid1	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ ( ( 𝑁 ‘ 𝐵 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) = ( ( 𝑁 ‘ 𝐵 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) ↔ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( 𝑁 ‘ 𝐵 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) ) = ( GId ‘ 𝐺 ) ) )
30	3 28 11 29	syl3anc	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) = ( ( 𝑁 ‘ 𝐵 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) ↔ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( 𝑁 ‘ 𝐵 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) ) = ( GId ‘ 𝐺 ) ) )
31	27 30	mpbird	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) = ( ( 𝑁 ‘ 𝐵 ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) )