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↔AGB=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→AGN⁡A=AGB
5 4 adantl ⊢G∈GrpOp∧A∈X∧B∈X∧N⁡A=B→AGN⁡A=AGB
6 1 2 3 grporinv ⊢G∈GrpOp∧A∈X→AGN⁡A=U
7 6 3adant3 ⊢G∈GrpOp∧A∈X∧B∈X→AGN⁡A=U
8 7 adantr ⊢G∈GrpOp∧A∈X∧B∈X∧N⁡A=B→AGN⁡A=U
9 5 8 eqtr3d ⊢G∈GrpOp∧A∈X∧B∈X∧N⁡A=B→AGB=U
10 oveq2 ⊢AGB=U→N⁡AGAGB=N⁡AGU
11 10 adantl ⊢G∈GrpOp∧A∈X∧B∈X∧AGB=U→N⁡AGAGB=N⁡AGU
12 1 2 3 grpolinv ⊢G∈GrpOp∧A∈X→N⁡AGA=U
13 12 oveq1d ⊢G∈GrpOp∧A∈X→N⁡AGAGB=UGB
14 13 3adant3 ⊢G∈GrpOp∧A∈X∧B∈X→N⁡AGAGB=UGB
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⁡AGAGB=N⁡AGAGB
21 19 20 syldan ⊢G∈GrpOp∧A∈X∧B∈X→N⁡AGAGB=N⁡AGAGB
22 21 3impb ⊢G∈GrpOp∧A∈X∧B∈X→N⁡AGAGB=N⁡AGAGB
23 14 22 eqtr3d ⊢G∈GrpOp∧A∈X∧B∈X→UGB=N⁡AGAGB
24 1 2 grpolid ⊢G∈GrpOp∧B∈X→UGB=B
25 24 3adant2 ⊢G∈GrpOp∧A∈X∧B∈X→UGB=B
26 23 25 eqtr3d ⊢G∈GrpOp∧A∈X∧B∈X→N⁡AGAGB=B
27 26 adantr ⊢G∈GrpOp∧A∈X∧B∈X∧AGB=U→N⁡AGAGB=B
28 1 2 grporid ⊢G∈GrpOp∧N⁡A∈X→N⁡AGU=N⁡A
29 15 28 syldan ⊢G∈GrpOp∧A∈X→N⁡AGU=N⁡A
30 29 3adant3 ⊢G∈GrpOp∧A∈X∧B∈X→N⁡AGU=N⁡A
31 30 adantr ⊢G∈GrpOp∧A∈X∧B∈X∧AGB=U→N⁡AGU=N⁡A
32 11 27 31 3eqtr3rd ⊢G∈GrpOp∧A∈X∧B∈X∧AGB=U→N⁡A=B
33 9 32 impbida ⊢G∈GrpOp∧A∈X∧B∈X→N⁡A=B↔AGB=U