Theorem mgmn0plusgf

Description: The restriction of the group operation of a magma to its base set is a function if the base set does not contain the empty set. Excluding the empty set from the base set is necessary because of the specific definition of an undefined operation value (see also ndmovcl and ndmovrcl ). (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 )
	mgmn0plusgf.r	|- P = ( .+ |` ( B X. B ) )
Assertion	mgmn0plusgf	|- ( ph -> P : ( B X. B ) --> 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		mgmn0plusgf.r	|- P = ( .+ |` ( B X. B ) )
6	1 2	mgmcl	|- ( ( G e. Mgm /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
7	3 6	syl3an1	|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
8	7	3expb	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
9		df-nel	|- ( (/) e/ B <-> -. (/) e. B )
10		nelelne	|- ( -. (/) e. B -> ( ( x .+ y ) e. B -> ( x .+ y ) =/= (/) ) )
11	9 10	sylbi	|- ( (/) e/ B -> ( ( x .+ y ) e. B -> ( x .+ y ) =/= (/) ) )
12	4 11	syl	|- ( ph -> ( ( x .+ y ) e. B -> ( x .+ y ) =/= (/) ) )
13	12	adantr	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( x .+ y ) e. B -> ( x .+ y ) =/= (/) ) )
14	8 13	mpd	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) =/= (/) )
15	14	ralrimivva	|- ( ph -> A. x e. B A. y e. B ( x .+ y ) =/= (/) )
16		ovn0ssdmfun	|- ( A. x e. B A. y e. B ( x .+ y ) =/= (/) -> ( ( B X. B ) C_ dom .+ /\ Fun ( .+ |` ( B X. B ) ) ) )
17	15 16	syl	|- ( ph -> ( ( B X. B ) C_ dom .+ /\ Fun ( .+ |` ( B X. B ) ) ) )
18	5	eqcomi	|- ( .+ |` ( B X. B ) ) = P
19	18	funeqi	|- ( Fun ( .+ |` ( B X. B ) ) <-> Fun P )
20		simpr	|- ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) -> Fun P )
21	5	dmeqi	|- dom P = dom ( .+ |` ( B X. B ) )
22		simpr	|- ( ( ph /\ ( B X. B ) C_ dom .+ ) -> ( B X. B ) C_ dom .+ )
23	22	adantr	|- ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) -> ( B X. B ) C_ dom .+ )
24		ssdmres	|- ( ( B X. B ) C_ dom .+ <-> dom ( .+ |` ( B X. B ) ) = ( B X. B ) )
25	23 24	sylib	|- ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) -> dom ( .+ |` ( B X. B ) ) = ( B X. B ) )
26	21 25	eqtrid	|- ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) -> dom P = ( B X. B ) )
27		df-fn	|- ( P Fn ( B X. B ) <-> ( Fun P /\ dom P = ( B X. B ) ) )
28	20 26 27	sylanbrc	|- ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) -> P Fn ( B X. B ) )
29	22 24	sylib	|- ( ( ph /\ ( B X. B ) C_ dom .+ ) -> dom ( .+ |` ( B X. B ) ) = ( B X. B ) )
30	21 29	eqtrid	|- ( ( ph /\ ( B X. B ) C_ dom .+ ) -> dom P = ( B X. B ) )
31	30	anim1ci	|- ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) -> ( Fun P /\ dom P = ( B X. B ) ) )
32	31 27	sylibr	|- ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) -> P Fn ( B X. B ) )
33		elxp	|- ( z e. ( B X. B ) <-> E. x E. y ( z = <. x , y >. /\ ( x e. B /\ y e. B ) ) )
34	5	oveqi	|- ( x P y ) = ( x ( .+ |` ( B X. B ) ) y )
35		simprrl	|- ( ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) /\ ( z = <. x , y >. /\ ( x e. B /\ y e. B ) ) ) -> x e. B )
36		simprrr	|- ( ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) /\ ( z = <. x , y >. /\ ( x e. B /\ y e. B ) ) ) -> y e. B )
37	35 36	ovresd	|- ( ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) /\ ( z = <. x , y >. /\ ( x e. B /\ y e. B ) ) ) -> ( x ( .+ |` ( B X. B ) ) y ) = ( x .+ y ) )
38	34 37	eqtrid	|- ( ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) /\ ( z = <. x , y >. /\ ( x e. B /\ y e. B ) ) ) -> ( x P y ) = ( x .+ y ) )
39	8	ex	|- ( ph -> ( ( x e. B /\ y e. B ) -> ( x .+ y ) e. B ) )
40	39	adantr	|- ( ( ph /\ ( B X. B ) C_ dom .+ ) -> ( ( x e. B /\ y e. B ) -> ( x .+ y ) e. B ) )
41	40	adantr	|- ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) -> ( ( x e. B /\ y e. B ) -> ( x .+ y ) e. B ) )
42	41	a1d	|- ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) -> ( z = <. x , y >. -> ( ( x e. B /\ y e. B ) -> ( x .+ y ) e. B ) ) )
43	42	imp32	|- ( ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) /\ ( z = <. x , y >. /\ ( x e. B /\ y e. B ) ) ) -> ( x .+ y ) e. B )
44	38 43	eqeltrd	|- ( ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) /\ ( z = <. x , y >. /\ ( x e. B /\ y e. B ) ) ) -> ( x P y ) e. B )
45		fveq2	|- ( z = <. x , y >. -> ( P ` z ) = ( P ` <. x , y >. ) )
46		df-ov	|- ( x P y ) = ( P ` <. x , y >. )
47	45 46	eqtr4di	|- ( z = <. x , y >. -> ( P ` z ) = ( x P y ) )
48	47	eleq1d	|- ( z = <. x , y >. -> ( ( P ` z ) e. B <-> ( x P y ) e. B ) )
49	48	adantr	|- ( ( z = <. x , y >. /\ ( x e. B /\ y e. B ) ) -> ( ( P ` z ) e. B <-> ( x P y ) e. B ) )
50	49	adantl	|- ( ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) /\ ( z = <. x , y >. /\ ( x e. B /\ y e. B ) ) ) -> ( ( P ` z ) e. B <-> ( x P y ) e. B ) )
51	44 50	mpbird	|- ( ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) /\ ( z = <. x , y >. /\ ( x e. B /\ y e. B ) ) ) -> ( P ` z ) e. B )
52	51	ex	|- ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) -> ( ( z = <. x , y >. /\ ( x e. B /\ y e. B ) ) -> ( P ` z ) e. B ) )
53	52	exlimdvv	|- ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) -> ( E. x E. y ( z = <. x , y >. /\ ( x e. B /\ y e. B ) ) -> ( P ` z ) e. B ) )
54	33 53	biimtrid	|- ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) -> ( z e. ( B X. B ) -> ( P ` z ) e. B ) )
55	54	ralrimiv	|- ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) -> A. z e. ( B X. B ) ( P ` z ) e. B )
56		fnfvrnss	|- ( ( P Fn ( B X. B ) /\ A. z e. ( B X. B ) ( P ` z ) e. B ) -> ran P C_ B )
57	32 55 56	syl2anc	|- ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) -> ran P C_ B )
58		df-f	|- ( P : ( B X. B ) --> B <-> ( P Fn ( B X. B ) /\ ran P C_ B ) )
59	28 57 58	sylanbrc	|- ( ( ( ph /\ ( B X. B ) C_ dom .+ ) /\ Fun P ) -> P : ( B X. B ) --> B )
60	59	ex	|- ( ( ph /\ ( B X. B ) C_ dom .+ ) -> ( Fun P -> P : ( B X. B ) --> B ) )
61	19 60	biimtrid	|- ( ( ph /\ ( B X. B ) C_ dom .+ ) -> ( Fun ( .+ |` ( B X. B ) ) -> P : ( B X. B ) --> B ) )
62	61	expimpd	|- ( ph -> ( ( ( B X. B ) C_ dom .+ /\ Fun ( .+ |` ( B X. B ) ) ) -> P : ( B X. B ) --> B ) )
63	17 62	mpd	|- ( ph -> P : ( B X. B ) --> B )