Metamath Proof Explorer

Theorem plusfreseq

Description: If the empty set is not contained in the range of the group addition function of an extensible structure (not necessarily a magma), the restriction of the addition operation to (the Cartesian square of) the base set is the functionalization of it. (Contributed by AV, 28-Jan-2020)

Ref Expression
Hypotheses plusfreseq.1 
|- B = ( Base ` M )
plusfreseq.2 
|- .+ = ( +g ` M )
plusfreseq.3 
|- .+^ = ( +f ` M )
Assertion plusfreseq 
|- ( (/) e/ ran .+^ -> ( .+ |` ( B X. B ) ) = .+^ )

Proof

Step Hyp Ref Expression
1 plusfreseq.1 
 |-  B = ( Base ` M )
2 plusfreseq.2 
 |-  .+ = ( +g ` M )
3 plusfreseq.3 
 |-  .+^ = ( +f ` M )
4 1 3 plusffn 
 |-  .+^ Fn ( B X. B )
5 fnfun 
 |-  ( .+^ Fn ( B X. B ) -> Fun .+^ )
6 4 5 ax-mp 
 |-  Fun .+^
7 6 a1i 
 |-  ( (/) e/ ran .+^ -> Fun .+^ )
8 id 
 |-  ( (/) e/ ran .+^ -> (/) e/ ran .+^ )
9 1 2 3 plusfval 
 |-  ( ( x e. B /\ y e. B ) -> ( x .+^ y ) = ( x .+ y ) )
10 9 eqcomd 
 |-  ( ( x e. B /\ y e. B ) -> ( x .+ y ) = ( x .+^ y ) )
11 10 rgen2 
 |-  A. x e. B A. y e. B ( x .+ y ) = ( x .+^ y )
12 11 a1i 
 |-  ( (/) e/ ran .+^ -> A. x e. B A. y e. B ( x .+ y ) = ( x .+^ y ) )
13 fveq2 
 |-  ( p = <. x , y >. -> ( .+ ` p ) = ( .+ ` <. x , y >. ) )
14 df-ov 
 |-  ( x .+ y ) = ( .+ ` <. x , y >. )
15 13 14 eqtr4di 
 |-  ( p = <. x , y >. -> ( .+ ` p ) = ( x .+ y ) )
16 fveq2 
 |-  ( p = <. x , y >. -> ( .+^ ` p ) = ( .+^ ` <. x , y >. ) )
17 df-ov 
 |-  ( x .+^ y ) = ( .+^ ` <. x , y >. )
18 16 17 eqtr4di 
 |-  ( p = <. x , y >. -> ( .+^ ` p ) = ( x .+^ y ) )
19 15 18 eqeq12d 
 |-  ( p = <. x , y >. -> ( ( .+ ` p ) = ( .+^ ` p ) <-> ( x .+ y ) = ( x .+^ y ) ) )
20 19 ralxp 
 |-  ( A. p e. ( B X. B ) ( .+ ` p ) = ( .+^ ` p ) <-> A. x e. B A. y e. B ( x .+ y ) = ( x .+^ y ) )
21 12 20 sylibr 
 |-  ( (/) e/ ran .+^ -> A. p e. ( B X. B ) ( .+ ` p ) = ( .+^ ` p ) )
22 fndm 
 |-  ( .+^ Fn ( B X. B ) -> dom .+^ = ( B X. B ) )
23 22 eqcomd 
 |-  ( .+^ Fn ( B X. B ) -> ( B X. B ) = dom .+^ )
24 4 23 ax-mp 
 |-  ( B X. B ) = dom .+^
25 24 fveqressseq 
 |-  ( ( Fun .+^ /\ (/) e/ ran .+^ /\ A. p e. ( B X. B ) ( .+ ` p ) = ( .+^ ` p ) ) -> ( .+ |` ( B X. B ) ) = .+^ )
26 7 8 21 25 syl3anc 
 |-  ( (/) e/ ran .+^ -> ( .+ |` ( B X. B ) ) = .+^ )