Metamath Proof Explorer

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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
mgmn0plusgf.p ⊢ + = ( +g ‘ 𝐺 )
mgmn0plusgf.g ⊢ ( 𝜑 → 𝐺 ∈ Mgm )
mgmn0plusgf.0 ⊢ ( 𝜑 → ∅ ∉ 𝐵 )
mgmn0plusgf.r ⊢ 𝑃 = ( + ↾ ( 𝐵 × 𝐵 ) )
Assertion mgmn0plusgf ( 𝜑 → 𝑃 : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 mgmn0plusgf.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mgmn0plusgf.p ⊢ + = ( +g ‘ 𝐺 )
3 mgmn0plusgf.g ⊢ ( 𝜑 → 𝐺 ∈ Mgm )
4 mgmn0plusgf.0 ⊢ ( 𝜑 → ∅ ∉ 𝐵 )
5 mgmn0plusgf.r ⊢ 𝑃 = ( + ↾ ( 𝐵 × 𝐵 ) )
6 1 2 mgmcl ⊢ ( ( 𝐺 ∈ Mgm ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
7 3 6 syl3an1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
8 7 3expb ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
9 df-nel ⊢ ( ∅ ∉ 𝐵 ↔ ¬ ∅ ∈ 𝐵 )
10 nelelne ⊢ ( ¬ ∅ ∈ 𝐵 → ( ( 𝑥 + 𝑦 ) ∈ 𝐵 → ( 𝑥 + 𝑦 ) ≠ ∅ ) )
11 9 10 sylbi ⊢ ( ∅ ∉ 𝐵 → ( ( 𝑥 + 𝑦 ) ∈ 𝐵 → ( 𝑥 + 𝑦 ) ≠ ∅ ) )
12 4 11 syl ⊢ ( 𝜑 → ( ( 𝑥 + 𝑦 ) ∈ 𝐵 → ( 𝑥 + 𝑦 ) ≠ ∅ ) )
13 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) ∈ 𝐵 → ( 𝑥 + 𝑦 ) ≠ ∅ ) )
14 8 13 mpd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ≠ ∅ )
15 14 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) ≠ ∅ )
16 ovn0ssdmfun ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) ≠ ∅ → ( ( 𝐵 × 𝐵 ) ⊆ dom + ∧ Fun ( + ↾ ( 𝐵 × 𝐵 ) ) ) )
17 15 16 syl ⊢ ( 𝜑 → ( ( 𝐵 × 𝐵 ) ⊆ dom + ∧ Fun ( + ↾ ( 𝐵 × 𝐵 ) ) ) )
18 5 eqcomi ⊢ ( + ↾ ( 𝐵 × 𝐵 ) ) = 𝑃
19 18 funeqi ⊢ ( Fun ( + ↾ ( 𝐵 × 𝐵 ) ) ↔ Fun 𝑃 )
20 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) → Fun 𝑃 )
21 5 dmeqi ⊢ dom 𝑃 = dom ( + ↾ ( 𝐵 × 𝐵 ) )
22 simpr ⊢ ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) → ( 𝐵 × 𝐵 ) ⊆ dom + )
23 22 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) → ( 𝐵 × 𝐵 ) ⊆ dom + )
24 ssdmres ⊢ ( ( 𝐵 × 𝐵 ) ⊆ dom + ↔ dom ( + ↾ ( 𝐵 × 𝐵 ) ) = ( 𝐵 × 𝐵 ) )
25 23 24 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) → dom ( + ↾ ( 𝐵 × 𝐵 ) ) = ( 𝐵 × 𝐵 ) )
26 21 25 eqtrid ⊢ ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) → dom 𝑃 = ( 𝐵 × 𝐵 ) )
27 df-fn ⊢ ( 𝑃 Fn ( 𝐵 × 𝐵 ) ↔ ( Fun 𝑃 ∧ dom 𝑃 = ( 𝐵 × 𝐵 ) ) )
28 20 26 27 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) → 𝑃 Fn ( 𝐵 × 𝐵 ) )
29 22 24 sylib ⊢ ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) → dom ( + ↾ ( 𝐵 × 𝐵 ) ) = ( 𝐵 × 𝐵 ) )
30 21 29 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) → dom 𝑃 = ( 𝐵 × 𝐵 ) )
31 30 anim1ci ⊢ ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) → ( Fun 𝑃 ∧ dom 𝑃 = ( 𝐵 × 𝐵 ) ) )
32 31 27 sylibr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) → 𝑃 Fn ( 𝐵 × 𝐵 ) )
33 elxp ⊢ ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
34 5 oveqi ⊢ ( 𝑥 𝑃 𝑦 ) = ( 𝑥 ( + ↾ ( 𝐵 × 𝐵 ) ) 𝑦 )
35 simprrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) → 𝑥 ∈ 𝐵 )
36 simprrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) → 𝑦 ∈ 𝐵 )
37 35 36 ovresd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) → ( 𝑥 ( + ↾ ( 𝐵 × 𝐵 ) ) 𝑦 ) = ( 𝑥 + 𝑦 ) )
38 34 37 eqtrid ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) → ( 𝑥 𝑃 𝑦 ) = ( 𝑥 + 𝑦 ) )
39 8 ex ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 ) )
40 39 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 ) )
41 40 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 ) )
42 41 a1d ⊢ ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 ) ) )
43 42 imp32 ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
44 38 43 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) → ( 𝑥 𝑃 𝑦 ) ∈ 𝐵 )
45 fveq2 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑃 ‘ 𝑧 ) = ( 𝑃 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
46 df-ov ⊢ ( 𝑥 𝑃 𝑦 ) = ( 𝑃 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
47 45 46 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑃 ‘ 𝑧 ) = ( 𝑥 𝑃 𝑦 ) )
48 47 eleq1d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑃 ‘ 𝑧 ) ∈ 𝐵 ↔ ( 𝑥 𝑃 𝑦 ) ∈ 𝐵 ) )
49 48 adantr ⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑃 ‘ 𝑧 ) ∈ 𝐵 ↔ ( 𝑥 𝑃 𝑦 ) ∈ 𝐵 ) )
50 49 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) → ( ( 𝑃 ‘ 𝑧 ) ∈ 𝐵 ↔ ( 𝑥 𝑃 𝑦 ) ∈ 𝐵 ) )
51 44 50 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) → ( 𝑃 ‘ 𝑧 ) ∈ 𝐵 )
52 51 ex ⊢ ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) → ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑃 ‘ 𝑧 ) ∈ 𝐵 ) )
53 52 exlimdvv ⊢ ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑃 ‘ 𝑧 ) ∈ 𝐵 ) )
54 33 53 biimtrid ⊢ ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) → ( 𝑧 ∈ ( 𝐵 × 𝐵 ) → ( 𝑃 ‘ 𝑧 ) ∈ 𝐵 ) )
55 54 ralrimiv ⊢ ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) → ∀ 𝑧 ∈ ( 𝐵 × 𝐵 ) ( 𝑃 ‘ 𝑧 ) ∈ 𝐵 )
56 fnfvrnss ⊢ ( ( 𝑃 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑧 ∈ ( 𝐵 × 𝐵 ) ( 𝑃 ‘ 𝑧 ) ∈ 𝐵 ) → ran 𝑃 ⊆ 𝐵 )
57 32 55 56 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) → ran 𝑃 ⊆ 𝐵 )
58 df-f ⊢ ( 𝑃 : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ↔ ( 𝑃 Fn ( 𝐵 × 𝐵 ) ∧ ran 𝑃 ⊆ 𝐵 ) )
59 28 57 58 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) ∧ Fun 𝑃 ) → 𝑃 : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
60 59 ex ⊢ ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) → ( Fun 𝑃 → 𝑃 : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ) )
61 19 60 biimtrid ⊢ ( ( 𝜑 ∧ ( 𝐵 × 𝐵 ) ⊆ dom + ) → ( Fun ( + ↾ ( 𝐵 × 𝐵 ) ) → 𝑃 : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ) )
62 61 expimpd ⊢ ( 𝜑 → ( ( ( 𝐵 × 𝐵 ) ⊆ dom + ∧ Fun ( + ↾ ( 𝐵 × 𝐵 ) ) ) → 𝑃 : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ) )
63 17 62 mpd ⊢ ( 𝜑 → 𝑃 : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )