Theorem grpasscan2d

Description: An associative cancellation law for groups. (Contributed by SN, 29-Jan-2025)

	Ref	Expression
Hypotheses	grpasscan2d.b	|- B = ( Base ` G )
	grpasscan2d.p	|- .+ = ( +g ` G )
	grpasscan2d.n	|- N = ( invg ` G )
	grpasscan2d.g	|- ( ph -> G e. Grp )
	grpasscan2d.1	|- ( ph -> X e. B )
	grpasscan2d.2	|- ( ph -> Y e. B )
Assertion	grpasscan2d	|- ( ph -> ( ( X .+ ( N ` Y ) ) .+ Y ) = X )

Proof

Step	Hyp	Ref	Expression
1		grpasscan2d.b	|- B = ( Base ` G )
2		grpasscan2d.p	|- .+ = ( +g ` G )
3		grpasscan2d.n	|- N = ( invg ` G )
4		grpasscan2d.g	|- ( ph -> G e. Grp )
5		grpasscan2d.1	|- ( ph -> X e. B )
6		grpasscan2d.2	|- ( ph -> Y e. B )
7	1 2 3	grpasscan2	|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( X .+ ( N ` Y ) ) .+ Y ) = X )
8	4 5 6 7	syl3anc	|- ( ph -> ( ( X .+ ( N ` Y ) ) .+ Y ) = X )