Step |
Hyp |
Ref |
Expression |
1 |
|
grpsubval.b |
|- B = ( Base ` G ) |
2 |
|
grpsubval.p |
|- .+ = ( +g ` G ) |
3 |
|
grpsubval.i |
|- I = ( invg ` G ) |
4 |
|
grpsubval.m |
|- .- = ( -g ` G ) |
5 |
|
fveq2 |
|- ( g = G -> ( Base ` g ) = ( Base ` G ) ) |
6 |
5 1
|
eqtr4di |
|- ( g = G -> ( Base ` g ) = B ) |
7 |
|
fveq2 |
|- ( g = G -> ( +g ` g ) = ( +g ` G ) ) |
8 |
7 2
|
eqtr4di |
|- ( g = G -> ( +g ` g ) = .+ ) |
9 |
|
eqidd |
|- ( g = G -> x = x ) |
10 |
|
fveq2 |
|- ( g = G -> ( invg ` g ) = ( invg ` G ) ) |
11 |
10 3
|
eqtr4di |
|- ( g = G -> ( invg ` g ) = I ) |
12 |
11
|
fveq1d |
|- ( g = G -> ( ( invg ` g ) ` y ) = ( I ` y ) ) |
13 |
8 9 12
|
oveq123d |
|- ( g = G -> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) = ( x .+ ( I ` y ) ) ) |
14 |
6 6 13
|
mpoeq123dv |
|- ( g = G -> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) = ( x e. B , y e. B |-> ( x .+ ( I ` y ) ) ) ) |
15 |
|
df-sbg |
|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) ) |
16 |
1
|
fvexi |
|- B e. _V |
17 |
2
|
fvexi |
|- .+ e. _V |
18 |
17
|
rnex |
|- ran .+ e. _V |
19 |
|
p0ex |
|- { (/) } e. _V |
20 |
18 19
|
unex |
|- ( ran .+ u. { (/) } ) e. _V |
21 |
|
df-ov |
|- ( x .+ ( I ` y ) ) = ( .+ ` <. x , ( I ` y ) >. ) |
22 |
|
fvrn0 |
|- ( .+ ` <. x , ( I ` y ) >. ) e. ( ran .+ u. { (/) } ) |
23 |
21 22
|
eqeltri |
|- ( x .+ ( I ` y ) ) e. ( ran .+ u. { (/) } ) |
24 |
23
|
rgen2w |
|- A. x e. B A. y e. B ( x .+ ( I ` y ) ) e. ( ran .+ u. { (/) } ) |
25 |
16 16 20 24
|
mpoexw |
|- ( x e. B , y e. B |-> ( x .+ ( I ` y ) ) ) e. _V |
26 |
14 15 25
|
fvmpt |
|- ( G e. _V -> ( -g ` G ) = ( x e. B , y e. B |-> ( x .+ ( I ` y ) ) ) ) |
27 |
4 26
|
eqtrid |
|- ( G e. _V -> .- = ( x e. B , y e. B |-> ( x .+ ( I ` y ) ) ) ) |
28 |
|
fvprc |
|- ( -. G e. _V -> ( -g ` G ) = (/) ) |
29 |
4 28
|
eqtrid |
|- ( -. G e. _V -> .- = (/) ) |
30 |
|
fvprc |
|- ( -. G e. _V -> ( Base ` G ) = (/) ) |
31 |
1 30
|
eqtrid |
|- ( -. G e. _V -> B = (/) ) |
32 |
31
|
olcd |
|- ( -. G e. _V -> ( B = (/) \/ B = (/) ) ) |
33 |
|
0mpo0 |
|- ( ( B = (/) \/ B = (/) ) -> ( x e. B , y e. B |-> ( x .+ ( I ` y ) ) ) = (/) ) |
34 |
32 33
|
syl |
|- ( -. G e. _V -> ( x e. B , y e. B |-> ( x .+ ( I ` y ) ) ) = (/) ) |
35 |
29 34
|
eqtr4d |
|- ( -. G e. _V -> .- = ( x e. B , y e. B |-> ( x .+ ( I ` y ) ) ) ) |
36 |
27 35
|
pm2.61i |
|- .- = ( x e. B , y e. B |-> ( x .+ ( I ` y ) ) ) |