Theorem mgmn0plusgf 18731

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 7605 and ndmovrcl 7606). (Contributed by AV, 16-Aug-2026.)

Hypotheses

Ref	Expression
mgmn0plusgf.b	⊢ 𝐵 = (Base‘𝐺)
mgmn0plusgf.p	⊢ + = (+g‘𝐺)
mgmn0plusgf.g	⊢ (𝜑 → 𝐺 ∈ Mgm)
mgmn0plusgf.0	⊢ (𝜑 → ∅ ∉ 𝐵)
mgmn0plusgf.r	⊢ 𝑃 = ( + ↾ (𝐵 × 𝐵))

Assertion

Ref	Expression
mgmn0plusgf	⊢ (𝜑 → 𝑃:(𝐵 × 𝐵)⟶𝐵)

Proof of Theorem mgmn0plusgf

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mgmn0plusgf.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ Mgm)
2		mgmn0plusgf.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝐺)
3		mgmn0plusgf.p	. . . . . . . 8 ⊢ + = (+g‘𝐺)
4	2, 3	mgmcl 18723	. . . . . . 7 ⊢ ((𝐺 ∈ Mgm ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
5	1, 4	syl3an1 1181	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
6	5	3expb 1138	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
7		mgmn0plusgf.0	. . . . . . 7 ⊢ (𝜑 → ∅ ∉ 𝐵)
8		df-nel 3067	. . . . . . . 8 ⊢ (∅ ∉ 𝐵 ↔ ¬ ∅ ∈ 𝐵)
9		nelelne 3061	. . . . . . . 8 ⊢ (¬ ∅ ∈ 𝐵 → ((𝑥 + 𝑦) ∈ 𝐵 → (𝑥 + 𝑦) ≠ ∅))
10	8, 9	sylbi 220	. . . . . . 7 ⊢ (∅ ∉ 𝐵 → ((𝑥 + 𝑦) ∈ 𝐵 → (𝑥 + 𝑦) ≠ ∅))
11	7, 10	syl 18	. . . . . 6 ⊢ (𝜑 → ((𝑥 + 𝑦) ∈ 𝐵 → (𝑥 + 𝑦) ≠ ∅))
12	11	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑥 + 𝑦) ∈ 𝐵 → (𝑥 + 𝑦) ≠ ∅))
13	6, 12	mpd 16	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ≠ ∅)
14	13	ralrimivva 3210	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) ≠ ∅)
15		ovn0ssdmfun 7588	. . 3 ⊢ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) ≠ ∅ → ((𝐵 × 𝐵) ⊆ dom + ∧ Fun ( + ↾ (𝐵 × 𝐵))))
16	14, 15	syl 18	. 2 ⊢ (𝜑 → ((𝐵 × 𝐵) ⊆ dom + ∧ Fun ( + ↾ (𝐵 × 𝐵))))
17		mgmn0plusgf.r	. . . . . 6 ⊢ 𝑃 = ( + ↾ (𝐵 × 𝐵))
18	17	eqcomi 2774	. . . . 5 ⊢ ( + ↾ (𝐵 × 𝐵)) = 𝑃
19	18	funeqi 6561	. . . 4 ⊢ (Fun ( + ↾ (𝐵 × 𝐵)) ↔ Fun 𝑃)
20		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) → Fun 𝑃)
21	17	dmeqi 5896	. . . . . . . 8 ⊢ dom 𝑃 = dom ( + ↾ (𝐵 × 𝐵))
22		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) → (𝐵 × 𝐵) ⊆ dom + )
23	22	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) → (𝐵 × 𝐵) ⊆ dom + )
24		ssdmres 6014	. . . . . . . . 9 ⊢ ((𝐵 × 𝐵) ⊆ dom + ↔ dom ( + ↾ (𝐵 × 𝐵)) = (𝐵 × 𝐵))
25	23, 24	sylib 221	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) → dom ( + ↾ (𝐵 × 𝐵)) = (𝐵 × 𝐵))
26	21, 25	eqtrid 2812	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) → dom 𝑃 = (𝐵 × 𝐵))
27		df-fn 6543	. . . . . . 7 ⊢ (𝑃 Fn (𝐵 × 𝐵) ↔ (Fun 𝑃 ∧ dom 𝑃 = (𝐵 × 𝐵)))
28	20, 26, 27	sylanbrc 595	. . . . . 6 ⊢ (((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) → 𝑃 Fn (𝐵 × 𝐵))
29	22, 24	sylib 221	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) → dom ( + ↾ (𝐵 × 𝐵)) = (𝐵 × 𝐵))
30	21, 29	eqtrid 2812	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) → dom 𝑃 = (𝐵 × 𝐵))
31	30	anim1ci 628	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) → (Fun 𝑃 ∧ dom 𝑃 = (𝐵 × 𝐵)))
32	31, 27	sylibr 237	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) → 𝑃 Fn (𝐵 × 𝐵))
33		elxp 5686	. . . . . . . . 9 ⊢ (𝑧 ∈ (𝐵 × 𝐵) ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)))
34	17	oveqi 7432	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑃𝑦) = (𝑥( + ↾ (𝐵 × 𝐵))𝑦)
35		simprrl 793	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) → 𝑥 ∈ 𝐵)
36		simprrr 794	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) → 𝑦 ∈ 𝐵)
37	35, 36	ovresd 7586	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) → (𝑥( + ↾ (𝐵 × 𝐵))𝑦) = (𝑥 + 𝑦))
38	34, 37	eqtrid 2812	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) → (𝑥𝑃𝑦) = (𝑥 + 𝑦))
39	6	ex 418	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵))
40	39	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵))
41	40	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵))
42	41	a1d 26	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) → (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)))
43	42	imp32 424	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) → (𝑥 + 𝑦) ∈ 𝐵)
44	38, 43	eqeltrd 2865	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) → (𝑥𝑃𝑦) ∈ 𝐵)
45		fveq2 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑃‘𝑧) = (𝑃‘⟨𝑥, 𝑦⟩))
46		df-ov 7422	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑃𝑦) = (𝑃‘⟨𝑥, 𝑦⟩)
47	45, 46	eqtr4di 2818	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑃‘𝑧) = (𝑥𝑃𝑦))
48	47	eleq1d 2850	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝑃‘𝑧) ∈ 𝐵 ↔ (𝑥𝑃𝑦) ∈ 𝐵))
49	48	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑃‘𝑧) ∈ 𝐵 ↔ (𝑥𝑃𝑦) ∈ 𝐵))
50	49	adantl 487	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) → ((𝑃‘𝑧) ∈ 𝐵 ↔ (𝑥𝑃𝑦) ∈ 𝐵))
51	44, 50	mpbird 260	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) → (𝑃‘𝑧) ∈ 𝐵)
52	51	ex 418	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) → ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑃‘𝑧) ∈ 𝐵))
53	52	exlimdvv 1967	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) → (∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑃‘𝑧) ∈ 𝐵))
54	33, 53	biimtrid 245	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) → (𝑧 ∈ (𝐵 × 𝐵) → (𝑃‘𝑧) ∈ 𝐵))
55	54	ralrimiv 3158	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) → ∀𝑧 ∈ (𝐵 × 𝐵)(𝑃‘𝑧) ∈ 𝐵)
56		fnfvrnss 7120	. . . . . . 7 ⊢ ((𝑃 Fn (𝐵 × 𝐵) ∧ ∀𝑧 ∈ (𝐵 × 𝐵)(𝑃‘𝑧) ∈ 𝐵) → ran 𝑃 ⊆ 𝐵)
57	32, 55, 56	syl2anc 596	. . . . . 6 ⊢ (((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) → ran 𝑃 ⊆ 𝐵)
58		df-f 6544	. . . . . 6 ⊢ (𝑃:(𝐵 × 𝐵)⟶𝐵 ↔ (𝑃 Fn (𝐵 × 𝐵) ∧ ran 𝑃 ⊆ 𝐵))
59	28, 57, 58	sylanbrc 595	. . . . 5 ⊢ (((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) ∧ Fun 𝑃) → 𝑃:(𝐵 × 𝐵)⟶𝐵)
60	59	ex 418	. . . 4 ⊢ ((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) → (Fun 𝑃 → 𝑃:(𝐵 × 𝐵)⟶𝐵))
61	19, 60	biimtrid 245	. . 3 ⊢ ((𝜑 ∧ (𝐵 × 𝐵) ⊆ dom + ) → (Fun ( + ↾ (𝐵 × 𝐵)) → 𝑃:(𝐵 × 𝐵)⟶𝐵))
62	61	expimpd 459	. 2 ⊢ (𝜑 → (((𝐵 × 𝐵) ⊆ dom + ∧ Fun ( + ↾ (𝐵 × 𝐵))) → 𝑃:(𝐵 × 𝐵)⟶𝐵))
63	16, 62	mpd 16	1 ⊢ (𝜑 → 𝑃:(𝐵 × 𝐵)⟶𝐵)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2146   ≠ wne 2960   ∉ wnel 3066  ∀wral 3081   ⊆ wss 3906  ∅c0 4286  ⟨cop 4597   × cxp 5661  dom cdm 5663  ran crn 5664   ↾ cres 5665  Fun wfun 6534   Fn wfn 6535  ⟶wf 6536  ‘cfv 6540  (class class class)co 7419  Basecbs 17291  +_gcplusg 17332  Mgmcmgm 18718

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7422  df-mgm 18720

This theorem is used by:  mgmn0plusgplusf  18732