Step |
Hyp |
Ref |
Expression |
1 |
|
ablsubadd.b |
|- B = ( Base ` G ) |
2 |
|
ablsubadd.p |
|- .+ = ( +g ` G ) |
3 |
|
ablsubadd.m |
|- .- = ( -g ` G ) |
4 |
|
ablgrp |
|- ( G e. Abel -> G e. Grp ) |
5 |
4
|
3ad2ant1 |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> G e. Grp ) |
6 |
|
simp2l |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> X e. B ) |
7 |
|
simp2r |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> Y e. B ) |
8 |
1 2
|
grpcl |
|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B ) |
9 |
5 6 7 8
|
syl3anc |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( X .+ Y ) e. B ) |
10 |
|
simp3l |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> Z e. B ) |
11 |
|
simp3r |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> W e. B ) |
12 |
1 2
|
grpcl |
|- ( ( G e. Grp /\ Z e. B /\ W e. B ) -> ( Z .+ W ) e. B ) |
13 |
5 10 11 12
|
syl3anc |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( Z .+ W ) e. B ) |
14 |
|
eqid |
|- ( invg ` G ) = ( invg ` G ) |
15 |
1 2 14 3
|
grpsubval |
|- ( ( ( X .+ Y ) e. B /\ ( Z .+ W ) e. B ) -> ( ( X .+ Y ) .- ( Z .+ W ) ) = ( ( X .+ Y ) .+ ( ( invg ` G ) ` ( Z .+ W ) ) ) ) |
16 |
9 13 15
|
syl2anc |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .- ( Z .+ W ) ) = ( ( X .+ Y ) .+ ( ( invg ` G ) ` ( Z .+ W ) ) ) ) |
17 |
|
ablcmn |
|- ( G e. Abel -> G e. CMnd ) |
18 |
17
|
3ad2ant1 |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> G e. CMnd ) |
19 |
|
simp2 |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( X e. B /\ Y e. B ) ) |
20 |
1 14
|
grpinvcl |
|- ( ( G e. Grp /\ Z e. B ) -> ( ( invg ` G ) ` Z ) e. B ) |
21 |
5 10 20
|
syl2anc |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( invg ` G ) ` Z ) e. B ) |
22 |
1 14
|
grpinvcl |
|- ( ( G e. Grp /\ W e. B ) -> ( ( invg ` G ) ` W ) e. B ) |
23 |
5 11 22
|
syl2anc |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( invg ` G ) ` W ) e. B ) |
24 |
1 2
|
cmn4 |
|- ( ( G e. CMnd /\ ( X e. B /\ Y e. B ) /\ ( ( ( invg ` G ) ` Z ) e. B /\ ( ( invg ` G ) ` W ) e. B ) ) -> ( ( X .+ Y ) .+ ( ( ( invg ` G ) ` Z ) .+ ( ( invg ` G ) ` W ) ) ) = ( ( X .+ ( ( invg ` G ) ` Z ) ) .+ ( Y .+ ( ( invg ` G ) ` W ) ) ) ) |
25 |
18 19 21 23 24
|
syl112anc |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .+ ( ( ( invg ` G ) ` Z ) .+ ( ( invg ` G ) ` W ) ) ) = ( ( X .+ ( ( invg ` G ) ` Z ) ) .+ ( Y .+ ( ( invg ` G ) ` W ) ) ) ) |
26 |
|
simp1 |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> G e. Abel ) |
27 |
1 2 14
|
ablinvadd |
|- ( ( G e. Abel /\ Z e. B /\ W e. B ) -> ( ( invg ` G ) ` ( Z .+ W ) ) = ( ( ( invg ` G ) ` Z ) .+ ( ( invg ` G ) ` W ) ) ) |
28 |
26 10 11 27
|
syl3anc |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( invg ` G ) ` ( Z .+ W ) ) = ( ( ( invg ` G ) ` Z ) .+ ( ( invg ` G ) ` W ) ) ) |
29 |
28
|
oveq2d |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .+ ( ( invg ` G ) ` ( Z .+ W ) ) ) = ( ( X .+ Y ) .+ ( ( ( invg ` G ) ` Z ) .+ ( ( invg ` G ) ` W ) ) ) ) |
30 |
1 2 14 3
|
grpsubval |
|- ( ( X e. B /\ Z e. B ) -> ( X .- Z ) = ( X .+ ( ( invg ` G ) ` Z ) ) ) |
31 |
6 10 30
|
syl2anc |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( X .- Z ) = ( X .+ ( ( invg ` G ) ` Z ) ) ) |
32 |
1 2 14 3
|
grpsubval |
|- ( ( Y e. B /\ W e. B ) -> ( Y .- W ) = ( Y .+ ( ( invg ` G ) ` W ) ) ) |
33 |
7 11 32
|
syl2anc |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( Y .- W ) = ( Y .+ ( ( invg ` G ) ` W ) ) ) |
34 |
31 33
|
oveq12d |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .- Z ) .+ ( Y .- W ) ) = ( ( X .+ ( ( invg ` G ) ` Z ) ) .+ ( Y .+ ( ( invg ` G ) ` W ) ) ) ) |
35 |
25 29 34
|
3eqtr4d |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .+ ( ( invg ` G ) ` ( Z .+ W ) ) ) = ( ( X .- Z ) .+ ( Y .- W ) ) ) |
36 |
16 35
|
eqtrd |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .- ( Z .+ W ) ) = ( ( X .- Z ) .+ ( Y .- W ) ) ) |