Metamath Proof Explorer

Theorem plusffval

Description: The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015) (Proof shortened by AV, 2-Mar-2024)

Ref Expression
Hypotheses plusffval.1 
|- B = ( Base ` G )
plusffval.2 
|- .+ = ( +g ` G )
plusffval.3 
|- .+^ = ( +f ` G )
Assertion plusffval 
|- .+^ = ( x e. B , y e. B |-> ( x .+ y ) )

Proof

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 ) )