Step |
Hyp |
Ref |
Expression |
1 |
|
lsmsubg.p |
|- .(+) = ( LSSum ` G ) |
2 |
|
lsmsubg.z |
|- Z = ( Cntz ` G ) |
3 |
|
simp3 |
|- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> T C_ ( Z ` U ) ) |
4 |
3
|
sselda |
|- ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ a e. T ) -> a e. ( Z ` U ) ) |
5 |
4
|
adantrr |
|- ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> a e. ( Z ` U ) ) |
6 |
|
simprr |
|- ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> b e. U ) |
7 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
8 |
7 2
|
cntzi |
|- ( ( a e. ( Z ` U ) /\ b e. U ) -> ( a ( +g ` G ) b ) = ( b ( +g ` G ) a ) ) |
9 |
5 6 8
|
syl2anc |
|- ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> ( a ( +g ` G ) b ) = ( b ( +g ` G ) a ) ) |
10 |
9
|
eqeq2d |
|- ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> ( x = ( a ( +g ` G ) b ) <-> x = ( b ( +g ` G ) a ) ) ) |
11 |
10
|
2rexbidva |
|- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( E. a e. T E. b e. U x = ( a ( +g ` G ) b ) <-> E. a e. T E. b e. U x = ( b ( +g ` G ) a ) ) ) |
12 |
|
rexcom |
|- ( E. a e. T E. b e. U x = ( b ( +g ` G ) a ) <-> E. b e. U E. a e. T x = ( b ( +g ` G ) a ) ) |
13 |
11 12
|
bitrdi |
|- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( E. a e. T E. b e. U x = ( a ( +g ` G ) b ) <-> E. b e. U E. a e. T x = ( b ( +g ` G ) a ) ) ) |
14 |
7 1
|
lsmelval |
|- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( x e. ( T .(+) U ) <-> E. a e. T E. b e. U x = ( a ( +g ` G ) b ) ) ) |
15 |
14
|
3adant3 |
|- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( x e. ( T .(+) U ) <-> E. a e. T E. b e. U x = ( a ( +g ` G ) b ) ) ) |
16 |
7 1
|
lsmelval |
|- ( ( U e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) ) -> ( x e. ( U .(+) T ) <-> E. b e. U E. a e. T x = ( b ( +g ` G ) a ) ) ) |
17 |
16
|
ancoms |
|- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( x e. ( U .(+) T ) <-> E. b e. U E. a e. T x = ( b ( +g ` G ) a ) ) ) |
18 |
17
|
3adant3 |
|- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( x e. ( U .(+) T ) <-> E. b e. U E. a e. T x = ( b ( +g ` G ) a ) ) ) |
19 |
13 15 18
|
3bitr4d |
|- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( x e. ( T .(+) U ) <-> x e. ( U .(+) T ) ) ) |
20 |
19
|
eqrdv |
|- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( T .(+) U ) = ( U .(+) T ) ) |