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	$⊢ \underset{˙}{+} = +_{G}$
	mgmn0plusgf.g	$⊢ φ \to G \in Mgm$
	mgmn0plusgf.0	$⊢ φ \to \emptyset \notin B$
	mgmn0plusgf.r	$⊢ P = {\underset{˙}{+} ↾}_{(B \times B)}$
Assertion	mgmn0plusgf	$⊢ φ \to P : B \times B ⟶ B$

Proof

Step	Hyp	Ref	Expression
1		mgmn0plusgf.b	$⊢ B = {Base}_{G}$
2		mgmn0plusgf.p	$⊢ \underset{˙}{+} = +_{G}$
3		mgmn0plusgf.g	$⊢ φ \to G \in Mgm$
4		mgmn0plusgf.0	$⊢ φ \to \emptyset \notin B$
5		mgmn0plusgf.r	$⊢ P = {\underset{˙}{+} ↾}_{(B \times B)}$
6	1 2	mgmcl	$⊢ (G \in Mgm \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
7	3 6	syl3an1	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
8	7	3expb	$⊢ (φ \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
9		df-nel	$⊢ \emptyset \notin B \leftrightarrow \neg \emptyset \in B$
10		nelelne	$⊢ \neg \emptyset \in B \to (x \underset{˙}{+} y \in B \to x \underset{˙}{+} y \neq \emptyset)$
11	9 10	sylbi	$⊢ \emptyset \notin B \to (x \underset{˙}{+} y \in B \to x \underset{˙}{+} y \neq \emptyset)$
12	4 11	syl	$⊢ φ \to (x \underset{˙}{+} y \in B \to x \underset{˙}{+} y \neq \emptyset)$
13	12	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to (x \underset{˙}{+} y \in B \to x \underset{˙}{+} y \neq \emptyset)$
14	8 13	mpd	$⊢ (φ \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \neq \emptyset$
15	14	ralrimivva	$⊢ φ \to \forall x \in B \forall y \in B x \underset{˙}{+} y \neq \emptyset$
16		ovn0ssdmfun	$⊢ \forall x \in B \forall y \in B x \underset{˙}{+} y \neq \emptyset \to (B \times B \subseteq dom \underset{˙}{+} \land Fun ({\underset{˙}{+} ↾}_{(B \times B)}))$
17	15 16	syl	$⊢ φ \to (B \times B \subseteq dom \underset{˙}{+} \land Fun ({\underset{˙}{+} ↾}_{(B \times B)}))$
18	5	eqcomi	$⊢ {\underset{˙}{+} ↾}_{(B \times B)} = P$
19	18	funeqi	$⊢ Fun ({\underset{˙}{+} ↾}_{(B \times B)}) \leftrightarrow Fun P$
20		simpr	$⊢ ((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \to Fun P$
21	5	dmeqi	$⊢ dom P = dom ({\underset{˙}{+} ↾}_{(B \times B)})$
22		simpr	$⊢ (φ \land B \times B \subseteq dom \underset{˙}{+}) \to B \times B \subseteq dom \underset{˙}{+}$
23	22	adantr	$⊢ ((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \to B \times B \subseteq dom \underset{˙}{+}$
24		ssdmres	$⊢ B \times B \subseteq dom \underset{˙}{+} \leftrightarrow dom ({\underset{˙}{+} ↾}_{(B \times B)}) = B \times B$
25	23 24	sylib	$⊢ ((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \to dom ({\underset{˙}{+} ↾}_{(B \times B)}) = B \times B$
26	21 25	eqtrid	$⊢ ((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \to dom P = B \times B$
27		df-fn	$⊢ P Fn (B \times B) \leftrightarrow (Fun P \land dom P = B \times B)$
28	20 26 27	sylanbrc	$⊢ ((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \to P Fn (B \times B)$
29	22 24	sylib	$⊢ (φ \land B \times B \subseteq dom \underset{˙}{+}) \to dom ({\underset{˙}{+} ↾}_{(B \times B)}) = B \times B$
30	21 29	eqtrid	$⊢ (φ \land B \times B \subseteq dom \underset{˙}{+}) \to dom P = B \times B$
31	30	anim1ci	$⊢ ((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \to (Fun P \land dom P = B \times B)$
32	31 27	sylibr	$⊢ ((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \to P Fn (B \times B)$
33		elxp	$⊢ z \in (B \times B) \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land (x \in B \land y \in B))$
34	5	oveqi	$⊢ x P y = x ({\underset{˙}{+} ↾}_{(B \times B)}) y$
35		simprrl	$⊢ (((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \land (z = ⟨x, y⟩ \land (x \in B \land y \in B))) \to x \in B$
36		simprrr	$⊢ (((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \land (z = ⟨x, y⟩ \land (x \in B \land y \in B))) \to y \in B$
37	35 36	ovresd	$⊢ (((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \land (z = ⟨x, y⟩ \land (x \in B \land y \in B))) \to x ({\underset{˙}{+} ↾}_{(B \times B)}) y = x \underset{˙}{+} y$
38	34 37	eqtrid	$⊢ (((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \land (z = ⟨x, y⟩ \land (x \in B \land y \in B))) \to x P y = x \underset{˙}{+} y$
39	8	ex	$⊢ φ \to ((x \in B \land y \in B) \to x \underset{˙}{+} y \in B)$
40	39	adantr	$⊢ (φ \land B \times B \subseteq dom \underset{˙}{+}) \to ((x \in B \land y \in B) \to x \underset{˙}{+} y \in B)$
41	40	adantr	$⊢ ((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \to ((x \in B \land y \in B) \to x \underset{˙}{+} y \in B)$
42	41	a1d	$⊢ ((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \to (z = ⟨x, y⟩ \to ((x \in B \land y \in B) \to x \underset{˙}{+} y \in B))$
43	42	imp32	$⊢ (((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \land (z = ⟨x, y⟩ \land (x \in B \land y \in B))) \to x \underset{˙}{+} y \in B$
44	38 43	eqeltrd	$⊢ (((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \land (z = ⟨x, y⟩ \land (x \in B \land y \in B))) \to x P y \in B$
45		fveq2	$⊢ z = ⟨x, y⟩ \to P (z) = P (⟨x, y⟩)$
46		df-ov	$⊢ x P y = P (⟨x, y⟩)$
47	45 46	eqtr4di	$⊢ z = ⟨x, y⟩ \to P (z) = x P y$
48	47	eleq1d	$⊢ z = ⟨x, y⟩ \to (P (z) \in B \leftrightarrow x P y \in B)$
49	48	adantr	$⊢ (z = ⟨x, y⟩ \land (x \in B \land y \in B)) \to (P (z) \in B \leftrightarrow x P y \in B)$
50	49	adantl	$⊢ (((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \land (z = ⟨x, y⟩ \land (x \in B \land y \in B))) \to (P (z) \in B \leftrightarrow x P y \in B)$
51	44 50	mpbird	$⊢ (((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \land (z = ⟨x, y⟩ \land (x \in B \land y \in B))) \to P (z) \in B$
52	51	ex	$⊢ ((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \to ((z = ⟨x, y⟩ \land (x \in B \land y \in B)) \to P (z) \in B)$
53	52	exlimdvv	$⊢ ((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \to (\exists x \exists y (z = ⟨x, y⟩ \land (x \in B \land y \in B)) \to P (z) \in B)$
54	33 53	biimtrid	$⊢ ((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \to (z \in (B \times B) \to P (z) \in B)$
55	54	ralrimiv	$⊢ ((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \to \forall z \in (B \times B) P (z) \in B$
56		fnfvrnss	$⊢ (P Fn (B \times B) \land \forall z \in (B \times B) P (z) \in B) \to ran P \subseteq B$
57	32 55 56	syl2anc	$⊢ ((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \to ran P \subseteq B$
58		df-f	$⊢ P : B \times B ⟶ B \leftrightarrow (P Fn (B \times B) \land ran P \subseteq B)$
59	28 57 58	sylanbrc	$⊢ ((φ \land B \times B \subseteq dom \underset{˙}{+}) \land Fun P) \to P : B \times B ⟶ B$
60	59	ex	$⊢ (φ \land B \times B \subseteq dom \underset{˙}{+}) \to (Fun P \to P : B \times B ⟶ B)$
61	19 60	biimtrid	$⊢ (φ \land B \times B \subseteq dom \underset{˙}{+}) \to (Fun ({\underset{˙}{+} ↾}_{(B \times B)}) \to P : B \times B ⟶ B)$
62	61	expimpd	$⊢ φ \to ((B \times B \subseteq dom \underset{˙}{+} \land Fun ({\underset{˙}{+} ↾}_{(B \times B)})) \to P : B \times B ⟶ B)$
63	17 62	mpd	$⊢ φ \to P : B \times B ⟶ B$

Metamath Proof Explorer

Theorem mgmn0plusgf

Proof