Step |
Hyp |
Ref |
Expression |
1 |
|
eqgabl.x |
|- X = ( Base ` G ) |
2 |
|
eqgabl.n |
|- .- = ( -g ` G ) |
3 |
|
eqgabl.r |
|- .~ = ( G ~QG S ) |
4 |
|
eqid |
|- ( invg ` G ) = ( invg ` G ) |
5 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
6 |
1 4 5 3
|
eqgval |
|- ( ( G e. Abel /\ S C_ X ) -> ( A .~ B <-> ( A e. X /\ B e. X /\ ( ( ( invg ` G ) ` A ) ( +g ` G ) B ) e. S ) ) ) |
7 |
|
simpll |
|- ( ( ( G e. Abel /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> G e. Abel ) |
8 |
|
ablgrp |
|- ( G e. Abel -> G e. Grp ) |
9 |
8
|
ad2antrr |
|- ( ( ( G e. Abel /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> G e. Grp ) |
10 |
|
simprl |
|- ( ( ( G e. Abel /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> A e. X ) |
11 |
1 4
|
grpinvcl |
|- ( ( G e. Grp /\ A e. X ) -> ( ( invg ` G ) ` A ) e. X ) |
12 |
9 10 11
|
syl2anc |
|- ( ( ( G e. Abel /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( invg ` G ) ` A ) e. X ) |
13 |
|
simprr |
|- ( ( ( G e. Abel /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> B e. X ) |
14 |
1 5
|
ablcom |
|- ( ( G e. Abel /\ ( ( invg ` G ) ` A ) e. X /\ B e. X ) -> ( ( ( invg ` G ) ` A ) ( +g ` G ) B ) = ( B ( +g ` G ) ( ( invg ` G ) ` A ) ) ) |
15 |
7 12 13 14
|
syl3anc |
|- ( ( ( G e. Abel /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( ( invg ` G ) ` A ) ( +g ` G ) B ) = ( B ( +g ` G ) ( ( invg ` G ) ` A ) ) ) |
16 |
1 5 4 2
|
grpsubval |
|- ( ( B e. X /\ A e. X ) -> ( B .- A ) = ( B ( +g ` G ) ( ( invg ` G ) ` A ) ) ) |
17 |
13 10 16
|
syl2anc |
|- ( ( ( G e. Abel /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( B .- A ) = ( B ( +g ` G ) ( ( invg ` G ) ` A ) ) ) |
18 |
15 17
|
eqtr4d |
|- ( ( ( G e. Abel /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( ( invg ` G ) ` A ) ( +g ` G ) B ) = ( B .- A ) ) |
19 |
18
|
eleq1d |
|- ( ( ( G e. Abel /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( ( ( invg ` G ) ` A ) ( +g ` G ) B ) e. S <-> ( B .- A ) e. S ) ) |
20 |
19
|
pm5.32da |
|- ( ( G e. Abel /\ S C_ X ) -> ( ( ( A e. X /\ B e. X ) /\ ( ( ( invg ` G ) ` A ) ( +g ` G ) B ) e. S ) <-> ( ( A e. X /\ B e. X ) /\ ( B .- A ) e. S ) ) ) |
21 |
|
df-3an |
|- ( ( A e. X /\ B e. X /\ ( ( ( invg ` G ) ` A ) ( +g ` G ) B ) e. S ) <-> ( ( A e. X /\ B e. X ) /\ ( ( ( invg ` G ) ` A ) ( +g ` G ) B ) e. S ) ) |
22 |
|
df-3an |
|- ( ( A e. X /\ B e. X /\ ( B .- A ) e. S ) <-> ( ( A e. X /\ B e. X ) /\ ( B .- A ) e. S ) ) |
23 |
20 21 22
|
3bitr4g |
|- ( ( G e. Abel /\ S C_ X ) -> ( ( A e. X /\ B e. X /\ ( ( ( invg ` G ) ` A ) ( +g ` G ) B ) e. S ) <-> ( A e. X /\ B e. X /\ ( B .- A ) e. S ) ) ) |
24 |
6 23
|
bitrd |
|- ( ( G e. Abel /\ S C_ X ) -> ( A .~ B <-> ( A e. X /\ B e. X /\ ( B .- A ) e. S ) ) ) |