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

Theorem grpinvop 10925
Description: The inverse of the group operation reverses the arguments. Lemma 2.2.1(d) of [Herstein] p. 55.
Hypotheses
Ref Expression
grpasscan1.1 |- X = ran G
grpasscan1.2 |- N = (inv` G)
Assertion
Ref Expression
grpinvop |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (N` (AGB)) = ((N` B)G(N` A)))

Proof of Theorem grpinvop
StepHypRef Expression
1 simp1 1055 . . . 4 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> G e. GrpOp)
2 simp2 1056 . . . 4 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> A e. X)
3 simp3 1057 . . . 4 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> B e. X)
4 grpasscan1.1 . . . . . . 7 |- X = ran G
5 grpasscan1.2 . . . . . . 7 |- N = (inv` G)
64, 5grpoinvcl 10912 . . . . . 6 |- ((G e. GrpOp /\ B e. X) -> (N` B) e. X)
763adant2 1074 . . . . 5 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (N` B) e. X)
84, 5grpoinvcl 10912 . . . . . 6 |- ((G e. GrpOp /\ A e. X) -> (N` A) e. X)
983adant3 1075 . . . . 5 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (N` A) e. X)
104grpocl 10886 . . . . 5 |- ((G e. GrpOp /\ (N` B) e. X /\ (N` A) e. X) -> ((N` B)G(N` A)) e. X)
111, 7, 9, 10syl111anc 1278 . . . 4 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> ((N` B)G(N` A)) e. X)
124grpoass 10889 . . . 4 |- ((G e. GrpOp /\ (A e. X /\ B e. X /\ ((N` B)G(N` A)) e. X)) -> ((AGB)G((N` B)G(N` A))) = (AG(BG((N` B)G(N` A)))))
131, 2, 3, 11, 12syl13anc 1280 . . 3 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> ((AGB)G((N` B)G(N` A))) = (AG(BG((N` B)G(N` A)))))
14 eqid 2092 . . . . . . . 8 |- (Id` G) = (Id` G)
154, 14, 5grporinv 10915 . . . . . . 7 |- ((G e. GrpOp /\ B e. X) -> (BG(N` B)) = (Id` G))
16153adant2 1074 . . . . . 6 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (BG(N` B)) = (Id` G))
1716opreq1d 5079 . . . . 5 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> ((BG(N` B))G(N` A)) = ((Id`
G)G(N` A)))
184grpoass 10889 . . . . . 6 |- ((G e. GrpOp /\ (B e. X /\ (N` B) e. X /\ (N` A) e. X)) -> ((BG(N` B))G(N` A)) = (BG((N` B)G(N` A))))
191, 3, 7, 9, 18syl13anc 1280 . . . . 5 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> ((BG(N` B))G(N` A)) = (BG((N` B)G(N` A))))
204, 14grpolid 10905 . . . . . . 7 |- ((G e. GrpOp /\ (N` A) e. X) -> ((Id` G)G(N` A)) = (N` A))
218, 20syldan 521 . . . . . 6 |- ((G e. GrpOp /\ A e. X) -> ((Id` G)G(N` A)) = (N` A))
22213adant3 1075 . . . . 5 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> ((Id` G)G(N` A)) = (N` A))
2317, 19, 223eqtr3d 2132 . . . 4 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (BG((N` B)G(N` A))) = (N` A))
2423opreq2d 5080 . . 3 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (AG(BG((N` B)G(N` A)))) = (AG(N` A)))
254, 14, 5grporinv 10915 . . . 4 |- ((G e. GrpOp /\ A e. X) -> (AG(N` A)) = (Id` G))
26253adant3 1075 . . 3 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (AG(N` A)) = (Id` G))
2713, 24, 263eqtrd 2128 . 2 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> ((AGB)G((N` B)G(N` A))) = (Id` G))
284grpocl 10886 . . 3 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (AGB) e. X)
294, 14, 5grpoinvid1 10916 . . 3 |- ((G e. GrpOp /\ (AGB) e. X /\ ((N` B)G(N` A)) e. X) -> ((N` (AGB)) = ((N` B)G(N` A)) <-> ((AGB)G((N` B)G(N` A))) = (Id`
G)))
301, 28, 11, 29syl111anc 1278 . 2 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> ((N` (AGB)) = ((N` B)G(N` A)) <-> ((AGB)G((N` B)G(N` A))) = (Id` G)))
3127, 30mpbird 269 1 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (N` (AGB)) = ((N` B)G(N` A)))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 209   /\ 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:  grpinvdiv 10929  grppnpcan2 10937  gxcom 10952  gxinv 10953  gxsuc 10955  gxdi 10982  ablinvop 15195  invaddvec 15316
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