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

Step	Hyp	Ref	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)
6	4, 5	grpoinvcl 10221	. . . . . 6 |- ((G e. GrpOp /\ B e. X) -> (N` B) e. X)
7	6	3adant2 1139	. . . . 5 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (N` B) e. X)
8	4, 5	grpoinvcl 10221	. . . . . 6 |- ((G e. GrpOp /\ A e. X) -> (N` A) e. X)
9	8	3adant3 1140	. . . . 5 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (N` A) e. X)
10	4	grpocl 10193	. . . . 5 |- ((G e. GrpOp /\ (N` B) e. X /\ (N` A) e. X) -> ((N` B)G(N` A)) e. X)
11	1, 7, 9, 10	syl111anc 1349	. . . 4 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> ((N` B)G(N` A)) e. X)
12	4	grpoass 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)))))
13	1, 2, 3, 11, 12	syl13anc 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)
15	4, 14, 5	grporinv 10224	. . . . . . 7 |- ((G e. GrpOp /\ B e. X) -> (BG(N` B)) = (Id` G))
16	15	3adant2 1139	. . . . . 6 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (BG(N` B)) = (Id` G))
17	16	opreq1d 4993	. . . . 5 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> ((BG(N` B))G(N` A)) = ((Id` G)G(N` A)))
18	4	grpoass 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))))
19	1, 3, 7, 9, 18	syl13anc 1351	. . . . 5 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> ((BG(N` B))G(N` A)) = (BG((N` B)G(N` A))))
20	4, 14	grpolid 10214	. . . . . . 7 |- ((G e. GrpOp /\ (N` A) e. X) -> ((Id` G)G(N` A)) = (N` A))
21	8, 20	syldan 595	. . . . . 6 |- ((G e. GrpOp /\ A e. X) -> ((Id` G)G(N` A)) = (N` A))
22	21	3adant3 1140	. . . . 5 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> ((Id` G)G(N` A)) = (N` A))
23	17, 19, 22	3eqtr3d 2181	. . . 4 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (BG((N` B)G(N` A))) = (N` A))
24	23	opreq2d 4994	. . 3 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (AG(BG((N` B)G(N` A)))) = (AG(N` A)))
25	4, 14, 5	grporinv 10224	. . . 4 |- ((G e. GrpOp /\ A e. X) -> (AG(N` A)) = (Id` G))
26	25	3adant3 1140	. . 3 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (AG(N` A)) = (Id` G))
27	13, 24, 26	3eqtrd 2177	. 2 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> ((AGB)G((N` B)G(N` A))) = (Id` G))
28	4	grpocl 10193	. . 3 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (AGB) e. X)
29	4, 14, 5	grpoinvid1 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)))
30	1, 28, 11, 29	syl111anc 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)))
31	27, 30	mpbird 318	1 |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (N` (AGB)) = ((N` B)G(N` A)))

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