Step |
Hyp |
Ref |
Expression |
1 |
|
grpsubadd.b |
|- B = ( Base ` G ) |
2 |
|
grpsubadd.p |
|- .+ = ( +g ` G ) |
3 |
|
grpsubadd.m |
|- .- = ( -g ` G ) |
4 |
|
simpl |
|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> G e. Grp ) |
5 |
|
simpr1 |
|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. B ) |
6 |
|
simpr2 |
|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y e. B ) |
7 |
|
eqid |
|- ( invg ` G ) = ( invg ` G ) |
8 |
1 7
|
grpinvcl |
|- ( ( G e. Grp /\ Z e. B ) -> ( ( invg ` G ) ` Z ) e. B ) |
9 |
8
|
3ad2antr3 |
|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( invg ` G ) ` Z ) e. B ) |
10 |
1 2
|
grpass |
|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ ( ( invg ` G ) ` Z ) e. B ) ) -> ( ( X .+ Y ) .+ ( ( invg ` G ) ` Z ) ) = ( X .+ ( Y .+ ( ( invg ` G ) ` Z ) ) ) ) |
11 |
4 5 6 9 10
|
syl13anc |
|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .+ ( ( invg ` G ) ` Z ) ) = ( X .+ ( Y .+ ( ( invg ` G ) ` Z ) ) ) ) |
12 |
1 2
|
grpcl |
|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B ) |
13 |
12
|
3adant3r3 |
|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .+ Y ) e. B ) |
14 |
|
simpr3 |
|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z e. B ) |
15 |
1 2 7 3
|
grpsubval |
|- ( ( ( X .+ Y ) e. B /\ Z e. B ) -> ( ( X .+ Y ) .- Z ) = ( ( X .+ Y ) .+ ( ( invg ` G ) ` Z ) ) ) |
16 |
13 14 15
|
syl2anc |
|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .- Z ) = ( ( X .+ Y ) .+ ( ( invg ` G ) ` Z ) ) ) |
17 |
1 2 7 3
|
grpsubval |
|- ( ( Y e. B /\ Z e. B ) -> ( Y .- Z ) = ( Y .+ ( ( invg ` G ) ` Z ) ) ) |
18 |
6 14 17
|
syl2anc |
|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y .- Z ) = ( Y .+ ( ( invg ` G ) ` Z ) ) ) |
19 |
18
|
oveq2d |
|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .+ ( Y .- Z ) ) = ( X .+ ( Y .+ ( ( invg ` G ) ` Z ) ) ) ) |
20 |
11 16 19
|
3eqtr4d |
|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .- Z ) = ( X .+ ( Y .- Z ) ) ) |