Theorem grppnpcan2 8027

Description: Group theory analog of pnpcan2t 5451.

Hypotheses

Ref	Expression
grpdivf.1	|- X = ran G
grpdivf.3	|- D = ( /g ` G)

Assertion

Ref	Expression
grppnpcan2	|- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGC)D(BGC)) = (ADB))

Proof of Theorem grppnpcan2

Step	Hyp	Ref	Expression
1		grpdivf.1	. . . 4 |- X = ran G
2		eqid 1468	. . . 4 |- (inv` G) = (inv` G)
3		grpdivf.3	. . . 4 |- D = ( /g ` G)
4	1, 2, 3	grpdivval 8017	. . 3 |- ((G e. Grp /\ (AGC) e. X /\ (BGC) e. X) -> ((AGC)D(BGC)) = ((AGC)G((inv` G)` (BGC))))
5		pm3.26 319	. . 3 |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> G e. Grp)
6	1	grpcl 7978	. . . 4 |- ((G e. Grp /\ A e. X /\ C e. X) -> (AGC) e. X)
7	6	3adant3r2 841	. . 3 |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> (AGC) e. X)
8	1	grpcl 7978	. . . 4 |- ((G e. Grp /\ B e. X /\ C e. X) -> (BGC) e. X)
9	8	3adant3r1 840	. . 3 |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> (BGC) e. X)
10	4, 5, 7, 9	syl3anc 856	. 2 |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGC)D(BGC)) = ((AGC)G((inv` G)` (BGC))))
11	1, 2	grpinvop 8015	. . . 4 |- ((G e. Grp /\ B e. X /\ C e. X) -> ((inv` G)` (BGC)) = (((inv` G)` C)G((inv` G)` B)))
12	11	3adant3r1 840	. . 3 |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> ((inv` G)` (BGC)) = (((inv` G)` C)G((inv` G)` B)))
13	12	opreq2d 3961	. 2 |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGC)G((inv` G)` (BGC))) = ((AGC)G(((inv` G)` C)G((inv` G)` B))))
14		eqid 1468	. . . . . . . . 9 |- (Id` G) = (Id` G)
15	1, 14, 2	grprinv 8005	. . . . . . . 8 |- ((G e. Grp /\ C e. X) -> (CG((inv` G)` C)) = (Id` G))
16	15	3adant2 796	. . . . . . 7 |- ((G e. Grp /\ B e. X /\ C e. X) -> (CG((inv` G)` C)) = (Id` G))
17	16	opreq1d 3960	. . . . . 6 |- ((G e. Grp /\ B e. X /\ C e. X) -> ((CG((inv` G)` C))G((inv` G)` B)) = ((Id` G)G((inv` G)` B)))
18	1	grpass 7981	. . . . . . 7 |- ((G e. Grp /\ (C e. X /\ ((inv` G)` C) e. X /\ ((inv` G)` B) e. X)) -> ((CG((inv` G)` C))G((inv` G)` B)) = (CG(((inv` G)` C)G((inv` G)` B))))
19		3simp1 786	. . . . . . 7 |- ((G e. Grp /\ B e. X /\ C e. X) -> G e. Grp)
20		3simp3 788	. . . . . . . 8 |- ((G e. Grp /\ B e. X /\ C e. X) -> C e. X)
21	1, 2	grpinvcl 8002	. . . . . . . . 9 |- ((G e. Grp /\ C e. X) -> ((inv` G)` C) e. X)
22	21	3adant2 796	. . . . . . . 8 |- ((G e. Grp /\ B e. X /\ C e. X) -> ((inv` G)` C) e. X)
23	1, 2	grpinvcl 8002	. . . . . . . . 9 |- ((G e. Grp /\ B e. X) -> ((inv` G)` B) e. X)
24	23	3adant3 797	. . . . . . . 8 |- ((G e. Grp /\ B e. X /\ C e. X) -> ((inv` G)` B) e. X)
25	20, 22, 24	3jca 817	. . . . . . 7 |- ((G e. Grp /\ B e. X /\ C e. X) -> (C e. X /\ ((inv` G)` C) e. X /\ ((inv` G)` B) e. X))
26	18, 19, 25	sylanc 471	. . . . . 6 |- ((G e. Grp /\ B e. X /\ C e. X) -> ((CG((inv` G)` C))G((inv` G)` B)) = (CG(((inv` G)` C)G((inv` G)` B))))
27	1, 14	grplid 7995	. . . . . . . 8 |- ((G e. Grp /\ ((inv` G)` B) e. X) -> ((Id` G)G((inv` G)` B)) = ((inv` G)` B))
28	23, 27	syldan 467	. . . . . . 7 |- ((G e. Grp /\ B e. X) -> ((Id` G)G((inv` G)` B)) = ((inv` G)` B))
29	28	3adant3 797	. . . . . 6 |- ((G e. Grp /\ B e. X /\ C e. X) -> ((Id` G)G((inv` G)` B)) = ((inv` G)` B))
30	17, 26, 29	3eqtr3d 1507	. . . . 5 |- ((G e. Grp /\ B e. X /\ C e. X) -> (CG(((inv` G)` C)G((inv` G)` B))) = ((inv` G)` B))
31	30	3adant3r1 840	. . . 4 |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> (CG(((inv` G)` C)G((inv` G)` B))) = ((inv` G)` B))
32	31	opreq2d 3961	. . 3 |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> (AG(CG(((inv` G)` C)G((inv` G)` B)))) = (AG((inv` G)` B)))
33		3simp1 786	. . . . . 6 |- ((A e. X /\ B e. X /\ C e. X) -> A e. X)
34	33	adantl 388	. . . . 5 |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> A e. X)
35		3simp3 788	. . . . . 6 |- ((A e. X /\ B e. X /\ C e. X) -> C e. X)
36	35	adantl 388	. . . . 5 |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> C e. X)
37	1	grpcl 7978	. . . . . 6 |- ((G e. Grp /\ ((inv` G)` C) e. X /\ ((inv` G)` B) e. X) -> (((inv` G)` C)G((inv` G)` B)) e. X)
38	21	3ad2antr3 812	. . . . . 6 |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> ((inv` G)` C) e. X)
39	23	3ad2antr2 811	. . . . . 6 |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> ((inv` G)` B) e. X)
40	37, 5, 38, 39	syl3anc 856	. . . . 5 |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> (((inv` G)` C)G((inv` G)` B)) e. X)
41	34, 36, 40	3jca 817	. . . 4 |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> (A e. X /\ C e. X /\ (((inv` G)` C)G((inv` G)` B)) e. X))
42	1	grpass 7981	. . . 4 |- ((G e. Grp /\ (A e. X /\ C e. X /\ (((inv` G)` C)G((inv` G)` B)) e. X)) -> ((AGC)G(((inv` G)` C)G((inv` G)` B))) = (AG(CG(((inv` G)` C)G((inv` G)` B)))))
43	41, 42	syldan 467	. . 3 |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGC)G(((inv` G)` C)G((inv` G)` B))) = (AG(CG(((inv` G)` C)G((inv` G)` B)))))
44	1, 2, 3	grpdivval 8017	. . . 4 |- ((G e. Grp /\ A e. X /\ B e. X) -> (ADB) = (AG((inv` G)` B)))
45	44	3adant3r3 842	. . 3 |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> (ADB) = (AG((inv` G)` B)))
46	32, 43, 45	3eqtr4d 1509	. 2 |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGC)G(((inv` G)` C)G((inv` G)` B))) = (ADB))
47	10, 13, 46	3eqtrd 1503	1 |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGC)D(BGC)) = (ADB))

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 773   = wceq 953   e. wcel 955  ran crn 3161  ` cfv 3172  (class class class)co 3948  Grpcgr 7967  Idcgi 7968  invcgn 7969   /g cgs 7970

This theorem is referenced by:  grpnnncan2 8028  va1cnlem 8279

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-pow 2732  ax-pr 2769  ax-un 2857

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-reu 1643  df-rab 1644  df-v 1803  df-sbc 1932  df-csb 1992  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-id 2824  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fn 3183  df-f 3184  df-fo 3186  df-fv 3188  df-opr 3950  df-oprab 3951  df-grp 7971  df-gid 7972  df-ginv 7973  df-gdiv 7974

Copyright terms: Public domain