Theorem mgmidpfod

Description: The operation of a magma with identity as a function is an onto function. (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 22-Dec-2013) (Revised by AV, 16-Aug-2026)

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

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 5	mgmplusf	⊢ ( 𝐺 ∈ Mgm → ⨣ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
7	3 6	syl	⊢ ( 𝜑 → ⨣ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
8	1 2 5	plusfval	⊢ ( ( 𝑒 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑒 ⨣ 𝑥 ) = ( 𝑒 + 𝑥 ) )
9	8	adantll	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑒 ⨣ 𝑥 ) = ( 𝑒 + 𝑥 ) )
10	9	eqeq1d	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑒 ⨣ 𝑥 ) = 𝑥 ↔ ( 𝑒 + 𝑥 ) = 𝑥 ) )
11	10	anbi1d	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝑒 ⨣ 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ↔ ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
12	11	ralbidva	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 ⨣ 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
13	12	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 ⨣ 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ↔ ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
14	4 13	mpbird	⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 ⨣ 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
15		simpl	⊢ ( ( ( 𝑒 ⨣ 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) → ( 𝑒 ⨣ 𝑥 ) = 𝑥 )
16	15	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 ⨣ 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝐵 ( 𝑒 ⨣ 𝑥 ) = 𝑥 )
17		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝑒 ⨣ 𝑥 ) = ( 𝑒 ⨣ 𝑦 ) )
18		id	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
19	17 18	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑒 ⨣ 𝑥 ) = 𝑥 ↔ ( 𝑒 ⨣ 𝑦 ) = 𝑦 ) )
20	19	rspcv	⊢ ( 𝑦 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑒 ⨣ 𝑥 ) = 𝑥 → ( 𝑒 ⨣ 𝑦 ) = 𝑦 ) )
21		eqcom	⊢ ( 𝑦 = ( 𝑒 ⨣ 𝑥 ) ↔ ( 𝑒 ⨣ 𝑥 ) = 𝑦 )
22	17	eqeq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑒 ⨣ 𝑥 ) = 𝑦 ↔ ( 𝑒 ⨣ 𝑦 ) = 𝑦 ) )
23	21 22	bitrid	⊢ ( 𝑥 = 𝑦 → ( 𝑦 = ( 𝑒 ⨣ 𝑥 ) ↔ ( 𝑒 ⨣ 𝑦 ) = 𝑦 ) )
24	23	rspcev	⊢ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑒 ⨣ 𝑦 ) = 𝑦 ) → ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝑒 ⨣ 𝑥 ) )
25	24	ex	⊢ ( 𝑦 ∈ 𝐵 → ( ( 𝑒 ⨣ 𝑦 ) = 𝑦 → ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝑒 ⨣ 𝑥 ) ) )
26	20 25	syld	⊢ ( 𝑦 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑒 ⨣ 𝑥 ) = 𝑥 → ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝑒 ⨣ 𝑥 ) ) )
27	16 26	syl5	⊢ ( 𝑦 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 ⨣ 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) → ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝑒 ⨣ 𝑥 ) ) )
28	27	reximdv	⊢ ( 𝑦 ∈ 𝐵 → ( ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 ⨣ 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) → ∃ 𝑒 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝑒 ⨣ 𝑥 ) ) )
29	28	impcom	⊢ ( ( ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 ⨣ 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑒 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝑒 ⨣ 𝑥 ) )
30	29	ralrimiva	⊢ ( ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 ⨣ 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) → ∀ 𝑦 ∈ 𝐵 ∃ 𝑒 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝑒 ⨣ 𝑥 ) )
31	14 30	syl	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ∃ 𝑒 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝑒 ⨣ 𝑥 ) )
32		foov	⊢ ( ⨣ : ( 𝐵 × 𝐵 ) –onto→ 𝐵 ↔ ( ⨣ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑒 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝑒 ⨣ 𝑥 ) ) )
33	7 31 32	sylanbrc	⊢ ( 𝜑 → ⨣ : ( 𝐵 × 𝐵 ) –onto→ 𝐵 )