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 ⊢ X = ran ⁡ G
grpinv.2 ⊢ U = GId ⁡ G
grpinv.3 ⊢ N = inv ⁡ G
Assertion grpoinvid1 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → N ⁡ A = B ↔ A G B = U

Proof

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