Theorem mgmfod

Description: The operation of a magma with identity is an onto function (assuming it is a function). (Contributed by FL, 2-Nov-2009) (Revised by AV, 16-Aug-2026)

	Ref	Expression
Hypotheses	mgmidpfod.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	mgmidpfod.p	⊢ + = ( +g ‘ 𝐺 )
	mgmidpfod.g	⊢ ( 𝜑 → 𝐺 ∈ Mgm )
	mgmidpfod.e	⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
	mgmfod.f	⊢ ( 𝜑 → + Fn ( 𝐵 × 𝐵 ) )
Assertion	mgmfod	⊢ ( 𝜑 → + : ( 𝐵 × 𝐵 ) –onto→ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mgmidpfod.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mgmidpfod.p	⊢ + = ( +g ‘ 𝐺 )
3		mgmidpfod.g	⊢ ( 𝜑 → 𝐺 ∈ Mgm )
4		mgmidpfod.e	⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
5		mgmfod.f	⊢ ( 𝜑 → + Fn ( 𝐵 × 𝐵 ) )
6		eqid	⊢ ( +𝑓 ‘ 𝐺 ) = ( +𝑓 ‘ 𝐺 )
7	1 2 3 4 6	mgmidpfod	⊢ ( 𝜑 → ( +𝑓 ‘ 𝐺 ) : ( 𝐵 × 𝐵 ) –onto→ 𝐵 )
8	1 2 6	plusfeq	⊢ ( + Fn ( 𝐵 × 𝐵 ) → ( +𝑓 ‘ 𝐺 ) = + )
9	5 8	syl	⊢ ( 𝜑 → ( +𝑓 ‘ 𝐺 ) = + )
10	9	eqcomd	⊢ ( 𝜑 → + = ( +𝑓 ‘ 𝐺 ) )
11		foeq1	⊢ ( + = ( +𝑓 ‘ 𝐺 ) → ( + : ( 𝐵 × 𝐵 ) –onto→ 𝐵 ↔ ( +𝑓 ‘ 𝐺 ) : ( 𝐵 × 𝐵 ) –onto→ 𝐵 ) )
12	10 11	syl	⊢ ( 𝜑 → ( + : ( 𝐵 × 𝐵 ) –onto→ 𝐵 ↔ ( +𝑓 ‘ 𝐺 ) : ( 𝐵 × 𝐵 ) –onto→ 𝐵 ) )
13	7 12	mpbird	⊢ ( 𝜑 → + : ( 𝐵 × 𝐵 ) –onto→ 𝐵 )