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

Proof

Step Hyp Ref Expression
1 mgmn0plusgf.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mgmn0plusgf.p ⊢ + = ( +g ‘ 𝐺 )
3 mgmn0plusgf.g ⊢ ( 𝜑 → 𝐺 ∈ Mgm )
4 mgmn0plusgf.0 ⊢ ( 𝜑 → ∅ ∉ 𝐵 )
5 mgmn0plusgplusf.p ⊢ ⨣ = ( +𝑓 ‘ 𝐺 )
6 1 5 mgmplusf ⊢ ( 𝐺 ∈ Mgm → ⨣ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
7 3 6 syl ⊢ ( 𝜑 → ⨣ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
8 7 ffnd ⊢ ( 𝜑 → ⨣ Fn ( 𝐵 × 𝐵 ) )
9 eqid ⊢ ( + ↾ ( 𝐵 × 𝐵 ) ) = ( + ↾ ( 𝐵 × 𝐵 ) )
10 1 2 3 4 9 mgmn0plusgf ⊢ ( 𝜑 → ( + ↾ ( 𝐵 × 𝐵 ) ) : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
11 10 ffnd ⊢ ( 𝜑 → ( + ↾ ( 𝐵 × 𝐵 ) ) Fn ( 𝐵 × 𝐵 ) )
12 elxp ⊢ ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
13 df-ov ⊢ ( 𝑥 + 𝑦 ) = ( + ‘ ⟨ 𝑥 , 𝑦 ⟩ )
14 1 2 5 plusfval ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ⨣ 𝑦 ) = ( 𝑥 + 𝑦 ) )
15 14 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑥 ⨣ 𝑦 ) = ( 𝑥 + 𝑦 ) )
16 opelxpi ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) )
17 16 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) )
18 17 fvresd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( + ↾ ( 𝐵 × 𝐵 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( + ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
19 13 15 18 3eqtr4a ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑥 ⨣ 𝑦 ) = ( ( + ↾ ( 𝐵 × 𝐵 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
20 fveq2 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ⨣ ‘ 𝑧 ) = ( ⨣ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
21 df-ov ⊢ ( 𝑥 ⨣ 𝑦 ) = ( ⨣ ‘ ⟨ 𝑥 , 𝑦 ⟩ )
22 20 21 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ⨣ ‘ 𝑧 ) = ( 𝑥 ⨣ 𝑦 ) )
23 fveq2 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( + ↾ ( 𝐵 × 𝐵 ) ) ‘ 𝑧 ) = ( ( + ↾ ( 𝐵 × 𝐵 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
24 22 23 eqeq12d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ⨣ ‘ 𝑧 ) = ( ( + ↾ ( 𝐵 × 𝐵 ) ) ‘ 𝑧 ) ↔ ( 𝑥 ⨣ 𝑦 ) = ( ( + ↾ ( 𝐵 × 𝐵 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
25 24 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( ⨣ ‘ 𝑧 ) = ( ( + ↾ ( 𝐵 × 𝐵 ) ) ‘ 𝑧 ) ↔ ( 𝑥 ⨣ 𝑦 ) = ( ( + ↾ ( 𝐵 × 𝐵 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
26 19 25 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ⨣ ‘ 𝑧 ) = ( ( + ↾ ( 𝐵 × 𝐵 ) ) ‘ 𝑧 ) )
27 26 exp31 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ⨣ ‘ 𝑧 ) = ( ( + ↾ ( 𝐵 × 𝐵 ) ) ‘ 𝑧 ) ) ) )
28 27 impcomd ⊢ ( 𝜑 → ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ⨣ ‘ 𝑧 ) = ( ( + ↾ ( 𝐵 × 𝐵 ) ) ‘ 𝑧 ) ) )
29 28 exlimdvv ⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ⨣ ‘ 𝑧 ) = ( ( + ↾ ( 𝐵 × 𝐵 ) ) ‘ 𝑧 ) ) )
30 12 29 biimtrid ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐵 × 𝐵 ) → ( ⨣ ‘ 𝑧 ) = ( ( + ↾ ( 𝐵 × 𝐵 ) ) ‘ 𝑧 ) ) )
31 30 imp ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐵 × 𝐵 ) ) → ( ⨣ ‘ 𝑧 ) = ( ( + ↾ ( 𝐵 × 𝐵 ) ) ‘ 𝑧 ) )
32 8 11 31 eqfnfvd ⊢ ( 𝜑 → ⨣ = ( + ↾ ( 𝐵 × 𝐵 ) ) )