Step |
Hyp |
Ref |
Expression |
1 |
|
grpsubid.b |
|- B = ( Base ` G ) |
2 |
|
grpsubid.o |
|- .0. = ( 0g ` G ) |
3 |
|
grpsubid.m |
|- .- = ( -g ` G ) |
4 |
|
grpsubadd0sub.p |
|- .+ = ( +g ` G ) |
5 |
|
eqid |
|- ( invg ` G ) = ( invg ` G ) |
6 |
1 4 5 3
|
grpsubval |
|- ( ( X e. B /\ Y e. B ) -> ( X .- Y ) = ( X .+ ( ( invg ` G ) ` Y ) ) ) |
7 |
6
|
3adant1 |
|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .- Y ) = ( X .+ ( ( invg ` G ) ` Y ) ) ) |
8 |
1 3 5 2
|
grpinvval2 |
|- ( ( G e. Grp /\ Y e. B ) -> ( ( invg ` G ) ` Y ) = ( .0. .- Y ) ) |
9 |
8
|
3adant2 |
|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( invg ` G ) ` Y ) = ( .0. .- Y ) ) |
10 |
9
|
oveq2d |
|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ ( ( invg ` G ) ` Y ) ) = ( X .+ ( .0. .- Y ) ) ) |
11 |
7 10
|
eqtrd |
|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .- Y ) = ( X .+ ( .0. .- Y ) ) ) |