Theorem mgmidprnd

Description: Range of an operation with a left and right identity element. (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	⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
	mgmidpfod.f	⊢ ⨣ = ( +𝑓 ‘ 𝐺 )
Assertion	mgmidprnd	⊢ ( 𝜑 → ran ⨣ = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mgmidpfod.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mgmidpfod.p	⊢ + = ( +g ‘ 𝐺 )
3		mgmidpfod.g	⊢ ( 𝜑 → 𝐺 ∈ Mgm )
4		mgmidpfod.e	⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
5		mgmidpfod.f	⊢ ⨣ = ( +𝑓 ‘ 𝐺 )
6	1 2 3 4 5	mgmidpfod	⊢ ( 𝜑 → ⨣ : ( 𝐵 × 𝐵 ) –onto→ 𝐵 )
7		forn	⊢ ( ⨣ : ( 𝐵 × 𝐵 ) –onto→ 𝐵 → ran ⨣ = 𝐵 )
8	6 7	syl	⊢ ( 𝜑 → ran ⨣ = 𝐵 )