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

Theorem grpinvop 10234
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 1120 . . . 4 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> G e. GrpOp)
2 simp2 1121 . . . 4 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> A e. X)
3 simp3 1122 . . . 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 10221 . . . . . 6 |- ((G e. GrpOp /\ B e. X) -> (N` B) e. X)
763adant2 1139 . . . . 5 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (N` B) e. X)
84, 5grpoinvcl 10221 . . . . . 6 |- ((G e. GrpOp /\ A e. X) -> (N` A) e. X)
983adant3 1140 . . . . 5 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (N` A) e. X)
104grpocl 10193 . . . . 5 |- ((G e. GrpOp /\ (N` B) e. X /\ (N` A) e. X) -> ((N` B)G(N` A)) e. X)
111, 7, 9, 10syl111anc 1349 . . . 4 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> ((N` B)G(N` A)) e. X)
124grpoass 10196 . . . 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 1351 . . 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 2141 . . . . . . . 8 |- (Id` G) = (Id` G)
154, 14, 5grporinv 10224 . . . . . . 7 |- ((G e. GrpOp /\ B e. X) -> (BG(N` B)) = (Id` G))
16153adant2 1139 . . . . . 6 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (BG(N` B)) = (Id` G))
1716opreq1d 4993 . . . . 5 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> ((BG(N` B))G(N` A)) = ((Id`
G)G(N` A)))
184grpoass 10196 . . . . . 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 1351 . . . . 5 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> ((BG(N` B))G(N` A)) = (BG((N` B)G(N` A))))
204, 14grpolid 10214 . . . . . . 7 |- ((G e. GrpOp /\ (N` A) e. X) -> ((Id` G)G(N` A)) = (N` A))
218, 20syldan 595 . . . . . 6 |- ((G e. GrpOp /\ A e. X) -> ((Id` G)G(N` A)) = (N` A))
22213adant3 1140 . . . . 5 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> ((Id` G)G(N` A)) = (N` A))
2317, 19, 223eqtr3d 2181 . . . 4 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (BG((N` B)G(N` A))) = (N` A))
2423opreq2d 4994 . . 3 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (AG(BG((N` B)G(N` A)))) = (AG(N` A)))
254, 14, 5grporinv 10224 . . . 4 |- ((G e. GrpOp /\ A e. X) -> (AG(N` A)) = (Id` G))
26253adant3 1140 . . 3 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (AG(N` A)) = (Id` G))
2713, 24, 263eqtrd 2177 . 2 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> ((AGB)G((N` B)G(N` A))) = (Id` G))
284grpocl 10193 . . 3 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (AGB) e. X)
294, 14, 5grpoinvid1 10225 . . 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 1349 . 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 318 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 219   /\ w3a 1102   = wceq 1586   e. wcel 1588  ran crn 4120  ` cfv 4131  (class class class)co 4981  GrpOpcgr 10177  Idcgi 10178  invcgn 10179
This theorem is referenced by:  grpinvdiv 10238  grppnpcan2 10246  gxcom 10261  gxinv 10262  gxsuc 10264  gxdi 10291  ablinvop 15449  invaddvec 15563
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929
This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-op 3246  df-uni 3367  df-br 3508  df-opab 3566  df-id 3747  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-opr 4983  df-grpo 10182  df-gid 10183  df-ginv 10184
Copyright terms: Public domain