Step |
Hyp |
Ref |
Expression |
1 |
|
grpinvval.b |
|- B = ( Base ` G ) |
2 |
|
grpinvval.p |
|- .+ = ( +g ` G ) |
3 |
|
grpinvval.o |
|- .0. = ( 0g ` G ) |
4 |
|
grpinvval.n |
|- N = ( invg ` 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 |
8
|
oveqd |
|- ( g = G -> ( y ( +g ` g ) x ) = ( y .+ x ) ) |
10 |
|
fveq2 |
|- ( g = G -> ( 0g ` g ) = ( 0g ` G ) ) |
11 |
10 3
|
eqtr4di |
|- ( g = G -> ( 0g ` g ) = .0. ) |
12 |
9 11
|
eqeq12d |
|- ( g = G -> ( ( y ( +g ` g ) x ) = ( 0g ` g ) <-> ( y .+ x ) = .0. ) ) |
13 |
6 12
|
riotaeqbidv |
|- ( g = G -> ( iota_ y e. ( Base ` g ) ( y ( +g ` g ) x ) = ( 0g ` g ) ) = ( iota_ y e. B ( y .+ x ) = .0. ) ) |
14 |
6 13
|
mpteq12dv |
|- ( g = G -> ( x e. ( Base ` g ) |-> ( iota_ y e. ( Base ` g ) ( y ( +g ` g ) x ) = ( 0g ` g ) ) ) = ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) ) |
15 |
|
df-minusg |
|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ y e. ( Base ` g ) ( y ( +g ` g ) x ) = ( 0g ` g ) ) ) ) |
16 |
1
|
fvexi |
|- B e. _V |
17 |
|
p0ex |
|- { (/) } e. _V |
18 |
17 16
|
unex |
|- ( { (/) } u. B ) e. _V |
19 |
|
ssun2 |
|- B C_ ( { (/) } u. B ) |
20 |
|
riotacl |
|- ( E! y e. B ( y .+ x ) = .0. -> ( iota_ y e. B ( y .+ x ) = .0. ) e. B ) |
21 |
19 20
|
sselid |
|- ( E! y e. B ( y .+ x ) = .0. -> ( iota_ y e. B ( y .+ x ) = .0. ) e. ( { (/) } u. B ) ) |
22 |
|
ssun1 |
|- { (/) } C_ ( { (/) } u. B ) |
23 |
|
riotaund |
|- ( -. E! y e. B ( y .+ x ) = .0. -> ( iota_ y e. B ( y .+ x ) = .0. ) = (/) ) |
24 |
|
riotaex |
|- ( iota_ y e. B ( y .+ x ) = .0. ) e. _V |
25 |
24
|
elsn |
|- ( ( iota_ y e. B ( y .+ x ) = .0. ) e. { (/) } <-> ( iota_ y e. B ( y .+ x ) = .0. ) = (/) ) |
26 |
23 25
|
sylibr |
|- ( -. E! y e. B ( y .+ x ) = .0. -> ( iota_ y e. B ( y .+ x ) = .0. ) e. { (/) } ) |
27 |
22 26
|
sselid |
|- ( -. E! y e. B ( y .+ x ) = .0. -> ( iota_ y e. B ( y .+ x ) = .0. ) e. ( { (/) } u. B ) ) |
28 |
21 27
|
pm2.61i |
|- ( iota_ y e. B ( y .+ x ) = .0. ) e. ( { (/) } u. B ) |
29 |
28
|
rgenw |
|- A. x e. B ( iota_ y e. B ( y .+ x ) = .0. ) e. ( { (/) } u. B ) |
30 |
16 18 29
|
mptexw |
|- ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) e. _V |
31 |
14 15 30
|
fvmpt |
|- ( G e. _V -> ( invg ` G ) = ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) ) |
32 |
|
fvprc |
|- ( -. G e. _V -> ( invg ` G ) = (/) ) |
33 |
|
mpt0 |
|- ( x e. (/) |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) = (/) |
34 |
32 33
|
eqtr4di |
|- ( -. G e. _V -> ( invg ` G ) = ( x e. (/) |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) ) |
35 |
|
fvprc |
|- ( -. G e. _V -> ( Base ` G ) = (/) ) |
36 |
1 35
|
eqtrid |
|- ( -. G e. _V -> B = (/) ) |
37 |
36
|
mpteq1d |
|- ( -. G e. _V -> ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) = ( x e. (/) |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) ) |
38 |
34 37
|
eqtr4d |
|- ( -. G e. _V -> ( invg ` G ) = ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) ) |
39 |
31 38
|
pm2.61i |
|- ( invg ` G ) = ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) |
40 |
4 39
|
eqtri |
|- N = ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) |