Step |
Hyp |
Ref |
Expression |
1 |
|
grpcominv.b |
|- B = ( Base ` G ) |
2 |
|
grpcominv.p |
|- .+ = ( +g ` G ) |
3 |
|
grpcominv.n |
|- N = ( invg ` G ) |
4 |
|
grpcominv.g |
|- ( ph -> G e. Grp ) |
5 |
|
grpcominv.x |
|- ( ph -> X e. B ) |
6 |
|
grpcominv.y |
|- ( ph -> Y e. B ) |
7 |
|
grpcominv.1 |
|- ( ph -> ( X .+ Y ) = ( Y .+ X ) ) |
8 |
1 3 4 6
|
grpinvcld |
|- ( ph -> ( N ` Y ) e. B ) |
9 |
1 2 4 8 6 5
|
grpassd |
|- ( ph -> ( ( ( N ` Y ) .+ Y ) .+ X ) = ( ( N ` Y ) .+ ( Y .+ X ) ) ) |
10 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
11 |
1 2 10 3 4 6
|
grplinvd |
|- ( ph -> ( ( N ` Y ) .+ Y ) = ( 0g ` G ) ) |
12 |
11
|
oveq1d |
|- ( ph -> ( ( ( N ` Y ) .+ Y ) .+ X ) = ( ( 0g ` G ) .+ X ) ) |
13 |
1 2 10 4 5
|
grplidd |
|- ( ph -> ( ( 0g ` G ) .+ X ) = X ) |
14 |
12 13
|
eqtr2d |
|- ( ph -> X = ( ( ( N ` Y ) .+ Y ) .+ X ) ) |
15 |
7
|
oveq2d |
|- ( ph -> ( ( N ` Y ) .+ ( X .+ Y ) ) = ( ( N ` Y ) .+ ( Y .+ X ) ) ) |
16 |
9 14 15
|
3eqtr4rd |
|- ( ph -> ( ( N ` Y ) .+ ( X .+ Y ) ) = X ) |
17 |
1 2 4 8 5 6
|
grpassd |
|- ( ph -> ( ( ( N ` Y ) .+ X ) .+ Y ) = ( ( N ` Y ) .+ ( X .+ Y ) ) ) |
18 |
1 2 3 4 5 6
|
grpasscan2d |
|- ( ph -> ( ( X .+ ( N ` Y ) ) .+ Y ) = X ) |
19 |
16 17 18
|
3eqtr4rd |
|- ( ph -> ( ( X .+ ( N ` Y ) ) .+ Y ) = ( ( ( N ` Y ) .+ X ) .+ Y ) ) |
20 |
1 2 4 5 8
|
grpcld |
|- ( ph -> ( X .+ ( N ` Y ) ) e. B ) |
21 |
1 2 4 8 5
|
grpcld |
|- ( ph -> ( ( N ` Y ) .+ X ) e. B ) |
22 |
1 2
|
grprcan |
|- ( ( G e. Grp /\ ( ( X .+ ( N ` Y ) ) e. B /\ ( ( N ` Y ) .+ X ) e. B /\ Y e. B ) ) -> ( ( ( X .+ ( N ` Y ) ) .+ Y ) = ( ( ( N ` Y ) .+ X ) .+ Y ) <-> ( X .+ ( N ` Y ) ) = ( ( N ` Y ) .+ X ) ) ) |
23 |
4 20 21 6 22
|
syl13anc |
|- ( ph -> ( ( ( X .+ ( N ` Y ) ) .+ Y ) = ( ( ( N ` Y ) .+ X ) .+ Y ) <-> ( X .+ ( N ` Y ) ) = ( ( N ` Y ) .+ X ) ) ) |
24 |
19 23
|
mpbid |
|- ( ph -> ( X .+ ( N ` Y ) ) = ( ( N ` Y ) .+ X ) ) |