Theorem grpasscan2

Description: An associative cancellation law for groups. (Contributed by Paul Chapman, 17-Apr-2009) (Revised by AV, 30-Aug-2021)

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

Proof

Step	Hyp	Ref	Expression
1		grplcan.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grplcan.p	⊢ + = ( +g ‘ 𝐺 )
3		grpasscan1.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
4		simp1	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐺 ∈ Grp )
5		simp2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
6	1 3	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑌 ) ∈ 𝐵 )
7	6	3adant2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑌 ) ∈ 𝐵 )
8		simp3	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
9	1 2	grpass	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑁 ‘ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 + ( 𝑁 ‘ 𝑌 ) ) + 𝑌 ) = ( 𝑋 + ( ( 𝑁 ‘ 𝑌 ) + 𝑌 ) ) )
10	4 5 7 8 9	syl13anc	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + ( 𝑁 ‘ 𝑌 ) ) + 𝑌 ) = ( 𝑋 + ( ( 𝑁 ‘ 𝑌 ) + 𝑌 ) ) )
11		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
12	1 2 11 3	grplinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑌 ) + 𝑌 ) = ( 0g ‘ 𝐺 ) )
13	12	3adant2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑌 ) + 𝑌 ) = ( 0g ‘ 𝐺 ) )
14	13	oveq2d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + ( ( 𝑁 ‘ 𝑌 ) + 𝑌 ) ) = ( 𝑋 + ( 0g ‘ 𝐺 ) ) )
15	1 2 11	grprid	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 + ( 0g ‘ 𝐺 ) ) = 𝑋 )
16	15	3adant3	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + ( 0g ‘ 𝐺 ) ) = 𝑋 )
17	10 14 16	3eqtrd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + ( 𝑁 ‘ 𝑌 ) ) + 𝑌 ) = 𝑋 )