Metamath Proof Explorer

Theorem ablsub4

Description: Commutative/associative subtraction law for Abelian groups. (Contributed by NM, 31-Mar-2014)

Ref Expression
Hypotheses ablsubadd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
ablsubadd.p ⊢ + = ( +g ‘ 𝐺 )
ablsubadd.m ⊢ − = ( -g ‘ 𝐺 )
Assertion ablsub4 ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑌 ) − ( 𝑍 + 𝑊 ) ) = ( ( 𝑋 − 𝑍 ) + ( 𝑌 − 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 ablsubadd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ablsubadd.p ⊢ + = ( +g ‘ 𝐺 )
3 ablsubadd.m ⊢ − = ( -g ‘ 𝐺 )
4 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
5 4 3ad2ant1 ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝐺 ∈ Grp )
6 simp2l ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
7 simp2r ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
8 1 2 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
9 5 6 7 8 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
10 simp3l ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝑍 ∈ 𝐵 )
11 simp3r ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝑊 ∈ 𝐵 )
12 1 2 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑍 + 𝑊 ) ∈ 𝐵 )
13 5 10 11 12 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( 𝑍 + 𝑊 ) ∈ 𝐵 )
14 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
15 1 2 14 3 grpsubval ⊢ ( ( ( 𝑋 + 𝑌 ) ∈ 𝐵 ∧ ( 𝑍 + 𝑊 ) ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) − ( 𝑍 + 𝑊 ) ) = ( ( 𝑋 + 𝑌 ) + ( ( invg ‘ 𝐺 ) ‘ ( 𝑍 + 𝑊 ) ) ) )
16 9 13 15 syl2anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑌 ) − ( 𝑍 + 𝑊 ) ) = ( ( 𝑋 + 𝑌 ) + ( ( invg ‘ 𝐺 ) ‘ ( 𝑍 + 𝑊 ) ) ) )
17 ablcmn ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ CMnd )
18 17 3ad2ant1 ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝐺 ∈ CMnd )
19 simp2 ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
20 1 14 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 )
21 5 10 20 syl2anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 )
22 1 14 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑊 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑊 ) ∈ 𝐵 )
23 5 11 22 syl2anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑊 ) ∈ 𝐵 )
24 1 2 cmn4 ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑊 ) ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑌 ) + ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑊 ) ) ) = ( ( 𝑋 + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) + ( 𝑌 + ( ( invg ‘ 𝐺 ) ‘ 𝑊 ) ) ) )
25 18 19 21 23 24 syl112anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑌 ) + ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑊 ) ) ) = ( ( 𝑋 + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) + ( 𝑌 + ( ( invg ‘ 𝐺 ) ‘ 𝑊 ) ) ) )
26 simp1 ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝐺 ∈ Abel )
27 1 2 14 ablinvadd ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝑍 + 𝑊 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑊 ) ) )
28 26 10 11 27 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝑍 + 𝑊 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑊 ) ) )
29 28 oveq2d ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑌 ) + ( ( invg ‘ 𝐺 ) ‘ ( 𝑍 + 𝑊 ) ) ) = ( ( 𝑋 + 𝑌 ) + ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑊 ) ) ) )
30 1 2 14 3 grpsubval ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 − 𝑍 ) = ( 𝑋 + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) )
31 6 10 30 syl2anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( 𝑋 − 𝑍 ) = ( 𝑋 + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) )
32 1 2 14 3 grpsubval ⊢ ( ( 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑌 − 𝑊 ) = ( 𝑌 + ( ( invg ‘ 𝐺 ) ‘ 𝑊 ) ) )
33 7 11 32 syl2anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( 𝑌 − 𝑊 ) = ( 𝑌 + ( ( invg ‘ 𝐺 ) ‘ 𝑊 ) ) )
34 31 33 oveq12d ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( 𝑋 − 𝑍 ) + ( 𝑌 − 𝑊 ) ) = ( ( 𝑋 + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) + ( 𝑌 + ( ( invg ‘ 𝐺 ) ‘ 𝑊 ) ) ) )
35 25 29 34 3eqtr4d ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑌 ) + ( ( invg ‘ 𝐺 ) ‘ ( 𝑍 + 𝑊 ) ) ) = ( ( 𝑋 − 𝑍 ) + ( 𝑌 − 𝑊 ) ) )
36 16 35 eqtrd ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑌 ) − ( 𝑍 + 𝑊 ) ) = ( ( 𝑋 − 𝑍 ) + ( 𝑌 − 𝑊 ) ) )