Metamath Proof Explorer

Theorem grpoinvid2

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 grpoinvid2 ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) = 𝐵 ↔ ( 𝐵 𝐺 𝐴 ) = 𝑈 ) )

Proof

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