HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem grp2inv 10923
Description: Double inverse law for groups. Lemma 2.2.1(c) of [Herstein] p. 55.
Hypotheses
Ref Expression
grpasscan1.1 |- X = ran G
grpasscan1.2 |- N = (inv` G)
Assertion
Ref Expression
grp2inv |- ((G e. GrpOp /\ A e. X) -> (N` (N` A)) = A)

Proof of Theorem grp2inv
StepHypRef Expression
1 grpasscan1.1 . . . . 5 |- X = ran G
2 grpasscan1.2 . . . . 5 |- N = (inv` G)
31, 2grpoinvcl 10912 . . . 4 |- ((G e. GrpOp /\ A e. X) -> (N` A) e. X)
4 eqid 2092 . . . . 5 |- (Id` G) = (Id` G)
51, 4, 2grporinv 10915 . . . 4 |- ((G e. GrpOp /\ (N` A) e. X) -> ((N` A)G(N` (N` A))) = (Id` G))
63, 5syldan 521 . . 3 |- ((G e. GrpOp /\ A e. X) -> ((N` A)G(N` (N` A))) = (Id` G))
71, 4, 2grpolinv 10914 . . 3 |- ((G e. GrpOp /\ A e. X) -> ((N` A)GA) = (Id` G))
86, 7eqtr4d 2127 . 2 |- ((G e. GrpOp /\ A e. X) -> ((N` A)G(N` (N` A))) = ((N` A)GA))
91, 2grpoinvcl 10912 . . . . 5 |- ((G e. GrpOp /\ (N` A) e. X) -> (N` (N` A)) e. X)
103, 9syldan 521 . . . 4 |- ((G e. GrpOp /\ A e. X) -> (N` (N` A)) e. X)
11 simpr 511 . . . 4 |- ((G e. GrpOp /\ A e. X) -> A e. X)
1210, 11, 33jca 1229 . . 3 |- ((G e. GrpOp /\ A e. X) -> ((N` (N` A)) e. X /\ A e. X /\ (N` A) e. X))
131grpolcan 10919 . . 3 |- ((G e. GrpOp /\ ((N` (N` A)) e. X /\ A e. X /\ (N` A) e. X)) -> (((N` A)G(N` (N` A))) = ((N` A)GA) <-> (N` (N` A)) = A))
1412, 13syldan 521 . 2 |- ((G e. GrpOp /\ A e. X) -> (((N` A)G(N` (N` A))) = ((N` A)GA) <-> (N` (N` A)) = A))
158, 14mpbid 239 1 |- ((G e. GrpOp /\ A e. X) -> (N` (N` A)) = A)
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 209   /\ wa 418   /\ w3a 1037   = wceq 1592   e. wcel 1594  ran crn 4138  ` cfv 4149  (class class class)co 5067  GrpOpcgr 10870  Idcgi 10871  invcgn 10872
This theorem is referenced by:  grpinvf 10924  grpdivinv 10928  grpinvdiv 10929  gxneg 10949  gxneg2 10950  gxinv2 10954  gxsuc 10955  gxmul 10961  nvnegneg 11168  ghomf1olem 13896  mult2inv 15272  vec2inv 15310
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1516  ax-6 1517  ax-7 1518  ax-gen 1519  ax-8 1596  ax-10 1597  ax-11 1598  ax-12 1599  ax-13 1600  ax-14 1601  ax-17 1608  ax-9 1620  ax-4 1626  ax-16 1803  ax-ext 2074  ax-rep 3599  ax-sep 3609  ax-nul 3619  ax-pr 3679  ax-un 3947
This theorem depends on definitions:  df-bi 210  df-or 419  df-an 420  df-3an 1039  df-ex 1521  df-sb 1765  df-eu 1992  df-mo 1993  df-clab 2080  df-cleq 2085  df-clel 2088  df-ne 2220  df-ral 2314  df-rex 2315  df-reu 2316  df-rab 2317  df-v 2501  df-sbc 2671  df-dif 2804  df-un 2806  df-in 2808  df-ss 2810  df-nul 3066  df-if 3166  df-sn 3237  df-pr 3238  df-op 3241  df-uni 3365  df-br 3510  df-opab 3568  df-id 3765  df-xp 4151  df-rel 4152  df-cnv 4153  df-co 4154  df-dm 4155  df-rn 4156  df-res 4157  df-ima 4158  df-fun 4159  df-fn 4160  df-f 4161  df-fo 4163  df-fv 4165  df-opr 5069  df-mpt 5202  df-iota 5374  df-riota 5896  df-grpo 10875  df-gid 10876  df-ginv 10877
Copyright terms: Public domain