Gyrogroup implies left-inverse property loop
Given: A gyrogroup , elements .
To prove: There exists unique such that and there exists unique such that (together, these prove it's a loop). Further, (this shows the left inverse property).
|Step no.||Assertion/construction||Facts used||Given data used||Previous steps used||Explanation|
|1||is the identity map for all .||We note that, for any , . By uniqueness of , we get .|
|2||Suppose are such that . Then, is the identity map.||gyroassociativity||Step (1)||By the left loop property, which is the identity map by Step (1).|
|3||is equal to the identity map.||Step (2)|
|4||We have . This simplifies to .||Step (3)||By Step (3), we obtain that and thus it simplifies to .|
|5||left loop property||we use that|
|6||We have . In particular, exists and is uniquely determined by .||Step (5)||Consider the gyroassociativity of : . Simplifying the left side gives . Now use Step (5) and we are done.|
Steps (4) and (6) complete the proof.