Metamath Proof Explorer

Theorem mgmn0plusgplusf

Description: The group addition function of a magma is the restriction of its group operation to its base set if the base set does not contain the empty set. (Contributed by AV, 16-Aug-2026)

Ref Expression
Hypotheses mgmn0plusgf.b 
|- B = ( Base ` G )
mgmn0plusgf.p 
|- .+ = ( +g ` G )
mgmn0plusgf.g 
|- ( ph -> G e. Mgm )
mgmn0plusgf.0 
|- ( ph -> (/) e/ B )
mgmn0plusgplusf.p 
|- .+^ = ( +f ` G )
Assertion mgmn0plusgplusf 
|- ( ph -> .+^ = ( .+ |` ( B X. B ) ) )

Proof

Step Hyp Ref Expression
1 mgmn0plusgf.b 
 |-  B = ( Base ` G )
2 mgmn0plusgf.p 
 |-  .+ = ( +g ` G )
3 mgmn0plusgf.g 
 |-  ( ph -> G e. Mgm )
4 mgmn0plusgf.0 
 |-  ( ph -> (/) e/ B )
5 mgmn0plusgplusf.p 
 |-  .+^ = ( +f ` G )
6 1 5 mgmplusf 
 |-  ( G e. Mgm -> .+^ : ( B X. B ) --> B )
7 3 6 syl 
 |-  ( ph -> .+^ : ( B X. B ) --> B )
8 7 ffnd 
 |-  ( ph -> .+^ Fn ( B X. B ) )
9 eqid 
 |-  ( .+ |` ( B X. B ) ) = ( .+ |` ( B X. B ) )
10 1 2 3 4 9 mgmn0plusgf 
 |-  ( ph -> ( .+ |` ( B X. B ) ) : ( B X. B ) --> B )
11 10 ffnd 
 |-  ( ph -> ( .+ |` ( B X. B ) ) Fn ( B X. B ) )
12 elxp 
 |-  ( z e. ( B X. B ) <-> E. x E. y ( z = <. x , y >. /\ ( x e. B /\ y e. B ) ) )
13 df-ov 
 |-  ( x .+ y ) = ( .+ ` <. x , y >. )
14 1 2 5 plusfval 
 |-  ( ( x e. B /\ y e. B ) -> ( x .+^ y ) = ( x .+ y ) )
15 14 ad2antlr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ z = <. x , y >. ) -> ( x .+^ y ) = ( x .+ y ) )
16 opelxpi 
 |-  ( ( x e. B /\ y e. B ) -> <. x , y >. e. ( B X. B ) )
17 16 ad2antlr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ z = <. x , y >. ) -> <. x , y >. e. ( B X. B ) )
18 17 fvresd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ z = <. x , y >. ) -> ( ( .+ |` ( B X. B ) ) ` <. x , y >. ) = ( .+ ` <. x , y >. ) )
19 13 15 18 3eqtr4a 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ z = <. x , y >. ) -> ( x .+^ y ) = ( ( .+ |` ( B X. B ) ) ` <. x , y >. ) )
20 fveq2 
 |-  ( z = <. x , y >. -> ( .+^ ` z ) = ( .+^ ` <. x , y >. ) )
21 df-ov 
 |-  ( x .+^ y ) = ( .+^ ` <. x , y >. )
22 20 21 eqtr4di 
 |-  ( z = <. x , y >. -> ( .+^ ` z ) = ( x .+^ y ) )
23 fveq2 
 |-  ( z = <. x , y >. -> ( ( .+ |` ( B X. B ) ) ` z ) = ( ( .+ |` ( B X. B ) ) ` <. x , y >. ) )
24 22 23 eqeq12d 
 |-  ( z = <. x , y >. -> ( ( .+^ ` z ) = ( ( .+ |` ( B X. B ) ) ` z ) <-> ( x .+^ y ) = ( ( .+ |` ( B X. B ) ) ` <. x , y >. ) ) )
25 24 adantl 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ z = <. x , y >. ) -> ( ( .+^ ` z ) = ( ( .+ |` ( B X. B ) ) ` z ) <-> ( x .+^ y ) = ( ( .+ |` ( B X. B ) ) ` <. x , y >. ) ) )
26 19 25 mpbird 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ z = <. x , y >. ) -> ( .+^ ` z ) = ( ( .+ |` ( B X. B ) ) ` z ) )
27 26 exp31 
 |-  ( ph -> ( ( x e. B /\ y e. B ) -> ( z = <. x , y >. -> ( .+^ ` z ) = ( ( .+ |` ( B X. B ) ) ` z ) ) ) )
28 27 impcomd 
 |-  ( ph -> ( ( z = <. x , y >. /\ ( x e. B /\ y e. B ) ) -> ( .+^ ` z ) = ( ( .+ |` ( B X. B ) ) ` z ) ) )
29 28 exlimdvv 
 |-  ( ph -> ( E. x E. y ( z = <. x , y >. /\ ( x e. B /\ y e. B ) ) -> ( .+^ ` z ) = ( ( .+ |` ( B X. B ) ) ` z ) ) )
30 12 29 biimtrid 
 |-  ( ph -> ( z e. ( B X. B ) -> ( .+^ ` z ) = ( ( .+ |` ( B X. B ) ) ` z ) ) )
31 30 imp 
 |-  ( ( ph /\ z e. ( B X. B ) ) -> ( .+^ ` z ) = ( ( .+ |` ( B X. B ) ) ` z ) )
32 8 11 31 eqfnfvd 
 |-  ( ph -> .+^ = ( .+ |` ( B X. B ) ) )