Step |
Hyp |
Ref |
Expression |
1 |
|
ablsubadd.b |
|- B = ( Base ` G ) |
2 |
|
ablsubadd.p |
|- .+ = ( +g ` G ) |
3 |
|
ablsubadd.m |
|- .- = ( -g ` G ) |
4 |
|
simpl |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> G e. Abel ) |
5 |
|
simprl |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> X e. B ) |
6 |
|
ablgrp |
|- ( G e. Abel -> G e. Grp ) |
7 |
6
|
adantr |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> G e. Grp ) |
8 |
|
simprr |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> Y e. B ) |
9 |
1 3
|
grpsubcl |
|- ( ( G e. Grp /\ Y e. B /\ X e. B ) -> ( Y .- X ) e. B ) |
10 |
7 8 5 9
|
syl3anc |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> ( Y .- X ) e. B ) |
11 |
1 2
|
ablcom |
|- ( ( G e. Abel /\ X e. B /\ ( Y .- X ) e. B ) -> ( X .+ ( Y .- X ) ) = ( ( Y .- X ) .+ X ) ) |
12 |
4 5 10 11
|
syl3anc |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> ( X .+ ( Y .- X ) ) = ( ( Y .- X ) .+ X ) ) |
13 |
1 2 3
|
grpnpcan |
|- ( ( G e. Grp /\ Y e. B /\ X e. B ) -> ( ( Y .- X ) .+ X ) = Y ) |
14 |
7 8 5 13
|
syl3anc |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> ( ( Y .- X ) .+ X ) = Y ) |
15 |
12 14
|
eqtrd |
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> ( X .+ ( Y .- X ) ) = Y ) |