Metamath Proof Explorer


Theorem grpolcan

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

Ref Expression
Hypothesis grplcan.1 X=ranG
Assertion grpolcan GGrpOpAXBXCXCGA=CGBA=B

Proof

Step Hyp Ref Expression
1 grplcan.1 X=ranG
2 oveq2 CGA=CGBinvGCGCGA=invGCGCGB
3 2 adantl GGrpOpAXBXCXCGA=CGBinvGCGCGA=invGCGCGB
4 eqid GIdG=GIdG
5 eqid invG=invG
6 1 4 5 grpolinv GGrpOpCXinvGCGC=GIdG
7 6 adantlr GGrpOpAXCXinvGCGC=GIdG
8 7 oveq1d GGrpOpAXCXinvGCGCGA=GIdGGA
9 1 5 grpoinvcl GGrpOpCXinvGCX
10 9 adantrl GGrpOpAXCXinvGCX
11 simprr GGrpOpAXCXCX
12 simprl GGrpOpAXCXAX
13 10 11 12 3jca GGrpOpAXCXinvGCXCXAX
14 1 grpoass GGrpOpinvGCXCXAXinvGCGCGA=invGCGCGA
15 13 14 syldan GGrpOpAXCXinvGCGCGA=invGCGCGA
16 15 anassrs GGrpOpAXCXinvGCGCGA=invGCGCGA
17 1 4 grpolid GGrpOpAXGIdGGA=A
18 17 adantr GGrpOpAXCXGIdGGA=A
19 8 16 18 3eqtr3d GGrpOpAXCXinvGCGCGA=A
20 19 adantrl GGrpOpAXBXCXinvGCGCGA=A
21 20 adantr GGrpOpAXBXCXCGA=CGBinvGCGCGA=A
22 6 adantrl GGrpOpBXCXinvGCGC=GIdG
23 22 oveq1d GGrpOpBXCXinvGCGCGB=GIdGGB
24 9 adantrl GGrpOpBXCXinvGCX
25 simprr GGrpOpBXCXCX
26 simprl GGrpOpBXCXBX
27 24 25 26 3jca GGrpOpBXCXinvGCXCXBX
28 1 grpoass GGrpOpinvGCXCXBXinvGCGCGB=invGCGCGB
29 27 28 syldan GGrpOpBXCXinvGCGCGB=invGCGCGB
30 1 4 grpolid GGrpOpBXGIdGGB=B
31 30 adantrr GGrpOpBXCXGIdGGB=B
32 23 29 31 3eqtr3d GGrpOpBXCXinvGCGCGB=B
33 32 adantlr GGrpOpAXBXCXinvGCGCGB=B
34 33 adantr GGrpOpAXBXCXCGA=CGBinvGCGCGB=B
35 3 21 34 3eqtr3d GGrpOpAXBXCXCGA=CGBA=B
36 35 exp53 GGrpOpAXBXCXCGA=CGBA=B
37 36 3imp2 GGrpOpAXBXCXCGA=CGBA=B
38 oveq2 A=BCGA=CGB
39 37 38 impbid1 GGrpOpAXBXCXCGA=CGBA=B