Metamath Proof Explorer

Theorem ablsub2inv

Description: Abelian group subtraction of two inverses. (Contributed by Stefan O'Rear, 24-May-2015)

Ref Expression
Hypotheses ablsub2inv.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
ablsub2inv.m ⊢ − = ( -g ‘ 𝐺 )
ablsub2inv.n ⊢ 𝑁 = ( invg ‘ 𝐺 )
ablsub2inv.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
ablsub2inv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
ablsub2inv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion ablsub2inv ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) − ( 𝑁 ‘ 𝑌 ) ) = ( 𝑌 − 𝑋 ) )

Proof

Step Hyp Ref Expression
1 ablsub2inv.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ablsub2inv.m ⊢ − = ( -g ‘ 𝐺 )
3 ablsub2inv.n ⊢ 𝑁 = ( invg ‘ 𝐺 )
4 ablsub2inv.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
5 ablsub2inv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 ablsub2inv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
8 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
9 4 8 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
10 1 3 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 )
11 9 5 10 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 )
12 1 7 2 3 9 11 6 grpsubinv ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) − ( 𝑁 ‘ 𝑌 ) ) = ( ( 𝑁 ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑌 ) )
13 1 7 ablcom ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑌 ) = ( 𝑌 ( +g ‘ 𝐺 ) ( 𝑁 ‘ 𝑋 ) ) )
14 4 11 6 13 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑌 ) = ( 𝑌 ( +g ‘ 𝐺 ) ( 𝑁 ‘ 𝑋 ) ) )
15 1 3 grpinvinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑌 ) ) = 𝑌 )
16 9 6 15 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑁 ‘ 𝑌 ) ) = 𝑌 )
17 16 oveq1d ⊢ ( 𝜑 → ( ( 𝑁 ‘ ( 𝑁 ‘ 𝑌 ) ) ( +g ‘ 𝐺 ) ( 𝑁 ‘ 𝑋 ) ) = ( 𝑌 ( +g ‘ 𝐺 ) ( 𝑁 ‘ 𝑋 ) ) )
18 14 17 eqtr4d ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑌 ) = ( ( 𝑁 ‘ ( 𝑁 ‘ 𝑌 ) ) ( +g ‘ 𝐺 ) ( 𝑁 ‘ 𝑋 ) ) )
19 1 3 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑌 ) ∈ 𝐵 )
20 9 6 19 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑌 ) ∈ 𝐵 )
21 1 7 3 grpinvadd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑁 ‘ 𝑌 ) ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑋 ( +g ‘ 𝐺 ) ( 𝑁 ‘ 𝑌 ) ) ) = ( ( 𝑁 ‘ ( 𝑁 ‘ 𝑌 ) ) ( +g ‘ 𝐺 ) ( 𝑁 ‘ 𝑋 ) ) )
22 9 5 20 21 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑋 ( +g ‘ 𝐺 ) ( 𝑁 ‘ 𝑌 ) ) ) = ( ( 𝑁 ‘ ( 𝑁 ‘ 𝑌 ) ) ( +g ‘ 𝐺 ) ( 𝑁 ‘ 𝑋 ) ) )
23 18 22 eqtr4d ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑌 ) = ( 𝑁 ‘ ( 𝑋 ( +g ‘ 𝐺 ) ( 𝑁 ‘ 𝑌 ) ) ) )
24 1 7 3 2 grpsubval ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( 𝑁 ‘ 𝑌 ) ) )
25 5 6 24 syl2anc ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( 𝑁 ‘ 𝑌 ) ) )
26 25 fveq2d ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑋 − 𝑌 ) ) = ( 𝑁 ‘ ( 𝑋 ( +g ‘ 𝐺 ) ( 𝑁 ‘ 𝑌 ) ) ) )
27 23 26 eqtr4d ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑌 ) = ( 𝑁 ‘ ( 𝑋 − 𝑌 ) ) )
28 1 2 3 grpinvsub ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑋 − 𝑌 ) ) = ( 𝑌 − 𝑋 ) )
29 9 5 6 28 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑋 − 𝑌 ) ) = ( 𝑌 − 𝑋 ) )
30 12 27 29 3eqtrd ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) − ( 𝑁 ‘ 𝑌 ) ) = ( 𝑌 − 𝑋 ) )