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