Metamath Proof Explorer

Theorem grpoinvid1

Description: The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 27-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypotheses grpinv.1 ⊢ 𝑋 = ran 𝐺
grpinv.2 ⊢ 𝑈 = ( GId ‘ 𝐺 )
grpinv.3 ⊢ 𝑁 = ( inv ‘ 𝐺 )
Assertion grpoinvid1 ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) = 𝐵 ↔ ( 𝐴 𝐺 𝐵 ) = 𝑈 ) )

Proof

Step Hyp Ref Expression
1 grpinv.1 ⊢ 𝑋 = ran 𝐺
2 grpinv.2 ⊢ 𝑈 = ( GId ‘ 𝐺 )
3 grpinv.3 ⊢ 𝑁 = ( inv ‘ 𝐺 )
4 oveq2 ⊢ ( ( 𝑁 ‘ 𝐴 ) = 𝐵 → ( 𝐴 𝐺 ( 𝑁 ‘ 𝐴 ) ) = ( 𝐴 𝐺 𝐵 ) )
5 4 adantl ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑁 ‘ 𝐴 ) = 𝐵 ) → ( 𝐴 𝐺 ( 𝑁 ‘ 𝐴 ) ) = ( 𝐴 𝐺 𝐵 ) )
6 1 2 3 grporinv ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 ( 𝑁 ‘ 𝐴 ) ) = 𝑈 )
7 6 3adant3 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( 𝑁 ‘ 𝐴 ) ) = 𝑈 )
8 7 adantr ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑁 ‘ 𝐴 ) = 𝐵 ) → ( 𝐴 𝐺 ( 𝑁 ‘ 𝐴 ) ) = 𝑈 )
9 5 8 eqtr3d ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑁 ‘ 𝐴 ) = 𝐵 ) → ( 𝐴 𝐺 𝐵 ) = 𝑈 )
10 oveq2 ⊢ ( ( 𝐴 𝐺 𝐵 ) = 𝑈 → ( ( 𝑁 ‘ 𝐴 ) 𝐺 ( 𝐴 𝐺 𝐵 ) ) = ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝑈 ) )
11 10 adantl ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝐺 𝐵 ) = 𝑈 ) → ( ( 𝑁 ‘ 𝐴 ) 𝐺 ( 𝐴 𝐺 𝐵 ) ) = ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝑈 ) )
12 1 2 3 grpolinv ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) = 𝑈 )
13 12 oveq1d ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) 𝐺 𝐵 ) = ( 𝑈 𝐺 𝐵 ) )
14 13 3adant3 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) 𝐺 𝐵 ) = ( 𝑈 𝐺 𝐵 ) )
15 1 3 grpoinvcl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 )
16 15 adantrr ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 )
17 simprl ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
18 simprr ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 )
19 16 17 18 3jca ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) )
20 1 grpoass ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) 𝐺 𝐵 ) = ( ( 𝑁 ‘ 𝐴 ) 𝐺 ( 𝐴 𝐺 𝐵 ) ) )
21 19 20 syldan ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) 𝐺 𝐵 ) = ( ( 𝑁 ‘ 𝐴 ) 𝐺 ( 𝐴 𝐺 𝐵 ) ) )
22 21 3impb ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) 𝐺 𝐵 ) = ( ( 𝑁 ‘ 𝐴 ) 𝐺 ( 𝐴 𝐺 𝐵 ) ) )
23 14 22 eqtr3d ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑈 𝐺 𝐵 ) = ( ( 𝑁 ‘ 𝐴 ) 𝐺 ( 𝐴 𝐺 𝐵 ) ) )
24 1 2 grpolid ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ) → ( 𝑈 𝐺 𝐵 ) = 𝐵 )
25 24 3adant2 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑈 𝐺 𝐵 ) = 𝐵 )
26 23 25 eqtr3d ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) 𝐺 ( 𝐴 𝐺 𝐵 ) ) = 𝐵 )
27 26 adantr ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝐺 𝐵 ) = 𝑈 ) → ( ( 𝑁 ‘ 𝐴 ) 𝐺 ( 𝐴 𝐺 𝐵 ) ) = 𝐵 )
28 1 2 grporid ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝑈 ) = ( 𝑁 ‘ 𝐴 ) )
29 15 28 syldan ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝑈 ) = ( 𝑁 ‘ 𝐴 ) )
30 29 3adant3 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝑈 ) = ( 𝑁 ‘ 𝐴 ) )
31 30 adantr ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝐺 𝐵 ) = 𝑈 ) → ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝑈 ) = ( 𝑁 ‘ 𝐴 ) )
32 11 27 31 3eqtr3rd ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝐺 𝐵 ) = 𝑈 ) → ( 𝑁 ‘ 𝐴 ) = 𝐵 )
33 9 32 impbida ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) = 𝐵 ↔ ( 𝐴 𝐺 𝐵 ) = 𝑈 ) )