Step |
Hyp |
Ref |
Expression |
1 |
|
plusffval.1 |
|- B = ( Base ` G ) |
2 |
|
plusffval.2 |
|- .+ = ( +g ` G ) |
3 |
|
plusffval.3 |
|- .+^ = ( +f ` G ) |
4 |
|
fveq2 |
|- ( g = G -> ( Base ` g ) = ( Base ` G ) ) |
5 |
4 1
|
eqtr4di |
|- ( g = G -> ( Base ` g ) = B ) |
6 |
|
fveq2 |
|- ( g = G -> ( +g ` g ) = ( +g ` G ) ) |
7 |
6 2
|
eqtr4di |
|- ( g = G -> ( +g ` g ) = .+ ) |
8 |
7
|
oveqd |
|- ( g = G -> ( x ( +g ` g ) y ) = ( x .+ y ) ) |
9 |
5 5 8
|
mpoeq123dv |
|- ( g = G -> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) = ( x e. B , y e. B |-> ( x .+ y ) ) ) |
10 |
|
df-plusf |
|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) ) |
11 |
1
|
fvexi |
|- B e. _V |
12 |
2
|
fvexi |
|- .+ e. _V |
13 |
12
|
rnex |
|- ran .+ e. _V |
14 |
|
p0ex |
|- { (/) } e. _V |
15 |
13 14
|
unex |
|- ( ran .+ u. { (/) } ) e. _V |
16 |
|
df-ov |
|- ( x .+ y ) = ( .+ ` <. x , y >. ) |
17 |
|
fvrn0 |
|- ( .+ ` <. x , y >. ) e. ( ran .+ u. { (/) } ) |
18 |
16 17
|
eqeltri |
|- ( x .+ y ) e. ( ran .+ u. { (/) } ) |
19 |
18
|
rgen2w |
|- A. x e. B A. y e. B ( x .+ y ) e. ( ran .+ u. { (/) } ) |
20 |
11 11 15 19
|
mpoexw |
|- ( x e. B , y e. B |-> ( x .+ y ) ) e. _V |
21 |
9 10 20
|
fvmpt |
|- ( G e. _V -> ( +f ` G ) = ( x e. B , y e. B |-> ( x .+ y ) ) ) |
22 |
|
fvprc |
|- ( -. G e. _V -> ( +f ` G ) = (/) ) |
23 |
|
fvprc |
|- ( -. G e. _V -> ( Base ` G ) = (/) ) |
24 |
1 23
|
eqtrid |
|- ( -. G e. _V -> B = (/) ) |
25 |
24
|
olcd |
|- ( -. G e. _V -> ( B = (/) \/ B = (/) ) ) |
26 |
|
0mpo0 |
|- ( ( B = (/) \/ B = (/) ) -> ( x e. B , y e. B |-> ( x .+ y ) ) = (/) ) |
27 |
25 26
|
syl |
|- ( -. G e. _V -> ( x e. B , y e. B |-> ( x .+ y ) ) = (/) ) |
28 |
22 27
|
eqtr4d |
|- ( -. G e. _V -> ( +f ` G ) = ( x e. B , y e. B |-> ( x .+ y ) ) ) |
29 |
21 28
|
pm2.61i |
|- ( +f ` G ) = ( x e. B , y e. B |-> ( x .+ y ) ) |
30 |
3 29
|
eqtri |
|- .+^ = ( x e. B , y e. B |-> ( x .+ y ) ) |