Theorem grporcan 25949

Description: Right cancellation law for groups. (Contributed by NM, 26-Oct-2006.) (New usage is discouraged.)

Hypothesis

Ref	Expression
grprcan.1	|- X = ran G

Assertion

Ref	Expression
grporcan	|- ( ( G e. GrpOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G C ) = ( B G C ) <-> A = B ) )

Proof of Theorem grporcan

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		grprcan.1	. . . . . . . 8 |- X = ran G
2		eqid 2451	. . . . . . . 8 |- (GId ` G ) = (GId ` G )
3	1, 2	grpoidinv2 25946	. . . . . . 7 |- ( ( G e. GrpOp /\ C e. X ) -> ( ( ( (GId ` G ) G C ) = C /\ ( C G (GId ` G ) ) = C ) /\ E. y e. X ( ( y G C ) = (GId ` G ) /\ ( C G y ) = (GId ` G ) ) ) )
4		simpr 463	. . . . . . . . 9 |- ( ( ( y G C ) = (GId ` G ) /\ ( C G y ) = (GId ` G ) ) -> ( C G y ) = (GId ` G ) )
5	4	reximi 2855	. . . . . . . 8 |- ( E. y e. X ( ( y G C ) = (GId ` G ) /\ ( C G y ) = (GId ` G ) ) -> E. y e. X ( C G y ) = (GId ` G ) )
6	5	adantl 468	. . . . . . 7 |- ( ( ( ( (GId ` G ) G C ) = C /\ ( C G (GId ` G ) ) = C ) /\ E. y e. X ( ( y G C ) = (GId ` G ) /\ ( C G y ) = (GId ` G ) ) ) -> E. y e. X ( C G y ) = (GId ` G ) )
7	3, 6	syl 17	. . . . . 6 |- ( ( G e. GrpOp /\ C e. X ) -> E. y e. X ( C G y ) = (GId ` G ) )
8	7	ad2ant2rl 755	. . . . 5 |- ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) -> E. y e. X ( C G y ) = (GId ` G ) )
9		oveq1 6297	. . . . . . . . . . . 12 |- ( ( A G C ) = ( B G C ) -> ( ( A G C ) G y ) = ( ( B G C ) G y ) )
10	9	ad2antll 735	. . . . . . . . . . 11 |- ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. X /\ ( A G C ) = ( B G C ) ) ) -> ( ( A G C ) G y ) = ( ( B G C ) G y ) )
11	1	grpoass 25931	. . . . . . . . . . . . . 14 |- ( ( G e. GrpOp /\ ( A e. X /\ C e. X /\ y e. X ) ) -> ( ( A G C ) G y ) = ( A G ( C G y ) ) )
12	11	3anassrs 1232	. . . . . . . . . . . . 13 |- ( ( ( ( G e. GrpOp /\ A e. X ) /\ C e. X ) /\ y e. X ) -> ( ( A G C ) G y ) = ( A G ( C G y ) ) )
13	12	adantlrl 726	. . . . . . . . . . . 12 |- ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ y e. X ) -> ( ( A G C ) G y ) = ( A G ( C G y ) ) )
14	13	adantrr 723	. . . . . . . . . . 11 |- ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. X /\ ( A G C ) = ( B G C ) ) ) -> ( ( A G C ) G y ) = ( A G ( C G y ) ) )
15	1	grpoass 25931	. . . . . . . . . . . . . . 15 |- ( ( G e. GrpOp /\ ( B e. X /\ C e. X /\ y e. X ) ) -> ( ( B G C ) G y ) = ( B G ( C G y ) ) )
16	15	3exp2 1227	. . . . . . . . . . . . . 14 |- ( G e. GrpOp -> ( B e. X -> ( C e. X -> ( y e. X -> ( ( B G C ) G y ) = ( B G ( C G y ) ) ) ) ) )
17	16	imp42 599	. . . . . . . . . . . . 13 |- ( ( ( G e. GrpOp /\ ( B e. X /\ C e. X ) ) /\ y e. X ) -> ( ( B G C ) G y ) = ( B G ( C G y ) ) )
18	17	adantllr 725	. . . . . . . . . . . 12 |- ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ y e. X ) -> ( ( B G C ) G y ) = ( B G ( C G y ) ) )
19	18	adantrr 723	. . . . . . . . . . 11 |- ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. X /\ ( A G C ) = ( B G C ) ) ) -> ( ( B G C ) G y ) = ( B G ( C G y ) ) )
20	10, 14, 19	3eqtr3d 2493	. . . . . . . . . 10 |- ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. X /\ ( A G C ) = ( B G C ) ) ) -> ( A G ( C G y ) ) = ( B G ( C G y ) ) )
21	20	adantrrl 730	. . . . . . . . 9 |- ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. X /\ ( ( C G y ) = (GId ` G ) /\ ( A G C ) = ( B G C ) ) ) ) -> ( A G ( C G y ) ) = ( B G ( C G y ) ) )
22		oveq2 6298	. . . . . . . . . . 11 |- ( ( C G y ) = (GId ` G ) -> ( A G ( C G y ) ) = ( A G (GId ` G ) ) )
23	22	ad2antrl 734	. . . . . . . . . 10 |- ( ( y e. X /\ ( ( C G y ) = (GId ` G ) /\ ( A G C ) = ( B G C ) ) ) -> ( A G ( C G y ) ) = ( A G (GId ` G ) ) )
24	23	adantl 468	. . . . . . . . 9 |- ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. X /\ ( ( C G y ) = (GId ` G ) /\ ( A G C ) = ( B G C ) ) ) ) -> ( A G ( C G y ) ) = ( A G (GId ` G ) ) )
25		oveq2 6298	. . . . . . . . . . 11 |- ( ( C G y ) = (GId ` G ) -> ( B G ( C G y ) ) = ( B G (GId ` G ) ) )
26	25	ad2antrl 734	. . . . . . . . . 10 |- ( ( y e. X /\ ( ( C G y ) = (GId ` G ) /\ ( A G C ) = ( B G C ) ) ) -> ( B G ( C G y ) ) = ( B G (GId ` G ) ) )
27	26	adantl 468	. . . . . . . . 9 |- ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. X /\ ( ( C G y ) = (GId ` G ) /\ ( A G C ) = ( B G C ) ) ) ) -> ( B G ( C G y ) ) = ( B G (GId ` G ) ) )
28	21, 24, 27	3eqtr3d 2493	. . . . . . . 8 |- ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. X /\ ( ( C G y ) = (GId ` G ) /\ ( A G C ) = ( B G C ) ) ) ) -> ( A G (GId ` G ) ) = ( B G (GId ` G ) ) )
29	1, 2	grporid 25948	. . . . . . . . 9 |- ( ( G e. GrpOp /\ A e. X ) -> ( A G (GId ` G ) ) = A )
30	29	ad2antrr 732	. . . . . . . 8 |- ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. X /\ ( ( C G y ) = (GId ` G ) /\ ( A G C ) = ( B G C ) ) ) ) -> ( A G (GId ` G ) ) = A )
31	1, 2	grporid 25948	. . . . . . . . . 10 |- ( ( G e. GrpOp /\ B e. X ) -> ( B G (GId ` G ) ) = B )
32	31	ad2ant2r 753	. . . . . . . . 9 |- ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) -> ( B G (GId ` G ) ) = B )
33	32	adantr 467	. . . . . . . 8 |- ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. X /\ ( ( C G y ) = (GId ` G ) /\ ( A G C ) = ( B G C ) ) ) ) -> ( B G (GId ` G ) ) = B )
34	28, 30, 33	3eqtr3d 2493	. . . . . . 7 |- ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. X /\ ( ( C G y ) = (GId ` G ) /\ ( A G C ) = ( B G C ) ) ) ) -> A = B )
35	34	exp45 619	. . . . . 6 |- ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) -> ( y e. X -> ( ( C G y ) = (GId ` G ) -> ( ( A G C ) = ( B G C ) -> A = B ) ) ) )
36	35	rexlimdv 2877	. . . . 5 |- ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) -> ( E. y e. X ( C G y ) = (GId ` G ) -> ( ( A G C ) = ( B G C ) -> A = B ) ) )
37	8, 36	mpd 15	. . . 4 |- ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) -> ( ( A G C ) = ( B G C ) -> A = B ) )
38		oveq1 6297	. . . 4 |- ( A = B -> ( A G C ) = ( B G C ) )
39	37, 38	impbid1 207	. . 3 |- ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) -> ( ( A G C ) = ( B G C ) <-> A = B ) )
40	39	exp43 617	. 2 |- ( G e. GrpOp -> ( A e. X -> ( B e. X -> ( C e. X -> ( ( A G C ) = ( B G C ) <-> A = B ) ) ) ) )
41	40	3imp2 1224	1 |- ( ( G e. GrpOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G C ) = ( B G C ) <-> A = B ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   /\ w3a 985   = wceq 1444   e. wcel 1887   E.wrex 2738   ran crn 4835   ` cfv 5582  (class class class)co 6290   GrpOpcgr 25914  GIdcgi 25915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pr 4639  ax-un 6583

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-fo 5588  df-fv 5590  df-riota 6252  df-ov 6293  df-grpo 25919  df-gid 25920

This theorem is referenced by:  grpoinveu  25950  grpoid  25951  grpodiveq  25984  rngorcan  26124  rngorz  26130  vcrcan  26183  nvrcan  26244  ghomdiv  32182