Step |
Hyp |
Ref |
Expression |
1 |
|
grplsm0l.b |
|- B = ( Base ` G ) |
2 |
|
grplsm0l.p |
|- .(+) = ( LSSum ` G ) |
3 |
|
grplsm0l.0 |
|- .0. = ( 0g ` G ) |
4 |
1 3
|
grpidcl |
|- ( G e. Grp -> .0. e. B ) |
5 |
4
|
snssd |
|- ( G e. Grp -> { .0. } C_ B ) |
6 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
7 |
1 6 2
|
lsmelvalx |
|- ( ( G e. Grp /\ { .0. } C_ B /\ A C_ B ) -> ( x e. ( { .0. } .(+) A ) <-> E. o e. { .0. } E. a e. A x = ( o ( +g ` G ) a ) ) ) |
8 |
7
|
3expa |
|- ( ( ( G e. Grp /\ { .0. } C_ B ) /\ A C_ B ) -> ( x e. ( { .0. } .(+) A ) <-> E. o e. { .0. } E. a e. A x = ( o ( +g ` G ) a ) ) ) |
9 |
8
|
an32s |
|- ( ( ( G e. Grp /\ A C_ B ) /\ { .0. } C_ B ) -> ( x e. ( { .0. } .(+) A ) <-> E. o e. { .0. } E. a e. A x = ( o ( +g ` G ) a ) ) ) |
10 |
5 9
|
mpidan |
|- ( ( G e. Grp /\ A C_ B ) -> ( x e. ( { .0. } .(+) A ) <-> E. o e. { .0. } E. a e. A x = ( o ( +g ` G ) a ) ) ) |
11 |
10
|
3adant3 |
|- ( ( G e. Grp /\ A C_ B /\ A =/= (/) ) -> ( x e. ( { .0. } .(+) A ) <-> E. o e. { .0. } E. a e. A x = ( o ( +g ` G ) a ) ) ) |
12 |
|
simpl1 |
|- ( ( ( G e. Grp /\ A C_ B /\ A =/= (/) ) /\ a e. A ) -> G e. Grp ) |
13 |
|
simp2 |
|- ( ( G e. Grp /\ A C_ B /\ A =/= (/) ) -> A C_ B ) |
14 |
13
|
sselda |
|- ( ( ( G e. Grp /\ A C_ B /\ A =/= (/) ) /\ a e. A ) -> a e. B ) |
15 |
1 6 3
|
grplid |
|- ( ( G e. Grp /\ a e. B ) -> ( .0. ( +g ` G ) a ) = a ) |
16 |
12 14 15
|
syl2anc |
|- ( ( ( G e. Grp /\ A C_ B /\ A =/= (/) ) /\ a e. A ) -> ( .0. ( +g ` G ) a ) = a ) |
17 |
16
|
eqeq2d |
|- ( ( ( G e. Grp /\ A C_ B /\ A =/= (/) ) /\ a e. A ) -> ( x = ( .0. ( +g ` G ) a ) <-> x = a ) ) |
18 |
|
equcom |
|- ( x = a <-> a = x ) |
19 |
17 18
|
bitrdi |
|- ( ( ( G e. Grp /\ A C_ B /\ A =/= (/) ) /\ a e. A ) -> ( x = ( .0. ( +g ` G ) a ) <-> a = x ) ) |
20 |
19
|
rexbidva |
|- ( ( G e. Grp /\ A C_ B /\ A =/= (/) ) -> ( E. a e. A x = ( .0. ( +g ` G ) a ) <-> E. a e. A a = x ) ) |
21 |
3
|
fvexi |
|- .0. e. _V |
22 |
|
oveq1 |
|- ( o = .0. -> ( o ( +g ` G ) a ) = ( .0. ( +g ` G ) a ) ) |
23 |
22
|
eqeq2d |
|- ( o = .0. -> ( x = ( o ( +g ` G ) a ) <-> x = ( .0. ( +g ` G ) a ) ) ) |
24 |
23
|
rexbidv |
|- ( o = .0. -> ( E. a e. A x = ( o ( +g ` G ) a ) <-> E. a e. A x = ( .0. ( +g ` G ) a ) ) ) |
25 |
21 24
|
rexsn |
|- ( E. o e. { .0. } E. a e. A x = ( o ( +g ` G ) a ) <-> E. a e. A x = ( .0. ( +g ` G ) a ) ) |
26 |
|
risset |
|- ( x e. A <-> E. a e. A a = x ) |
27 |
20 25 26
|
3bitr4g |
|- ( ( G e. Grp /\ A C_ B /\ A =/= (/) ) -> ( E. o e. { .0. } E. a e. A x = ( o ( +g ` G ) a ) <-> x e. A ) ) |
28 |
11 27
|
bitrd |
|- ( ( G e. Grp /\ A C_ B /\ A =/= (/) ) -> ( x e. ( { .0. } .(+) A ) <-> x e. A ) ) |
29 |
28
|
eqrdv |
|- ( ( G e. Grp /\ A C_ B /\ A =/= (/) ) -> ( { .0. } .(+) A ) = A ) |