Theorem ablinvadd

Description: The inverse of an Abelian group operation. (Contributed by NM, 31-Mar-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ablinvadd.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		ablinvadd.p	⊢ + = ( +g ‘ 𝐺 )
3		ablinvadd.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
4		ablgrp	⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
5	1 2 3	grpinvadd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝑁 ‘ 𝑌 ) + ( 𝑁 ‘ 𝑋 ) ) )
6	4 5	syl3an1	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝑁 ‘ 𝑌 ) + ( 𝑁 ‘ 𝑋 ) ) )
7		simp1	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐺 ∈ Abel )
8	4	3ad2ant1	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐺 ∈ Grp )
9		simp2	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
10	1 3	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 )
11	8 9 10	syl2anc	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 )
12		simp3	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
13	1 3	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑌 ) ∈ 𝐵 )
14	8 12 13	syl2anc	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑌 ) ∈ 𝐵 )
15	1 2	ablcom	⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 ∧ ( 𝑁 ‘ 𝑌 ) ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑋 ) + ( 𝑁 ‘ 𝑌 ) ) = ( ( 𝑁 ‘ 𝑌 ) + ( 𝑁 ‘ 𝑋 ) ) )
16	7 11 14 15	syl3anc	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑋 ) + ( 𝑁 ‘ 𝑌 ) ) = ( ( 𝑁 ‘ 𝑌 ) + ( 𝑁 ‘ 𝑋 ) ) )
17	6 16	eqtr4d	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝑁 ‘ 𝑋 ) + ( 𝑁 ‘ 𝑌 ) ) )