Theorem grpasscan1

Description: An associative cancellation law for groups. (Contributed by Paul Chapman, 25-Feb-2008) (Revised by AV, 30-Aug-2021)

	Ref	Expression
Hypotheses	grplcan.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grplcan.p	⊢ + = ( +g ‘ 𝐺 )
	grpasscan1.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
Assertion	grpasscan1	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + ( ( 𝑁 ‘ 𝑋 ) + 𝑌 ) ) = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		grplcan.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grplcan.p	⊢ + = ( +g ‘ 𝐺 )
3		grpasscan1.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
4		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
5	1 2 4 3	grprinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 + ( 𝑁 ‘ 𝑋 ) ) = ( 0g ‘ 𝐺 ) )
6	5	3adant3	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + ( 𝑁 ‘ 𝑋 ) ) = ( 0g ‘ 𝐺 ) )
7	6	oveq1d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + ( 𝑁 ‘ 𝑋 ) ) + 𝑌 ) = ( ( 0g ‘ 𝐺 ) + 𝑌 ) )
8	1 3	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 )
9	1 2	grpass	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 + ( 𝑁 ‘ 𝑋 ) ) + 𝑌 ) = ( 𝑋 + ( ( 𝑁 ‘ 𝑋 ) + 𝑌 ) ) )
10	9	3exp2	⊢ ( 𝐺 ∈ Grp → ( 𝑋 ∈ 𝐵 → ( ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 → ( 𝑌 ∈ 𝐵 → ( ( 𝑋 + ( 𝑁 ‘ 𝑋 ) ) + 𝑌 ) = ( 𝑋 + ( ( 𝑁 ‘ 𝑋 ) + 𝑌 ) ) ) ) ) )
11	10	imp	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 → ( 𝑌 ∈ 𝐵 → ( ( 𝑋 + ( 𝑁 ‘ 𝑋 ) ) + 𝑌 ) = ( 𝑋 + ( ( 𝑁 ‘ 𝑋 ) + 𝑌 ) ) ) ) )
12	8 11	mpd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 ∈ 𝐵 → ( ( 𝑋 + ( 𝑁 ‘ 𝑋 ) ) + 𝑌 ) = ( 𝑋 + ( ( 𝑁 ‘ 𝑋 ) + 𝑌 ) ) ) )
13	12	3impia	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + ( 𝑁 ‘ 𝑋 ) ) + 𝑌 ) = ( 𝑋 + ( ( 𝑁 ‘ 𝑋 ) + 𝑌 ) ) )
14	1 2 4	grplid	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) + 𝑌 ) = 𝑌 )
15	14	3adant2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) + 𝑌 ) = 𝑌 )
16	7 13 15	3eqtr3d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + ( ( 𝑁 ‘ 𝑋 ) + 𝑌 ) ) = 𝑌 )