Metamath Proof Explorer

Theorem mndpfo

Description: The addition operation of a monoid as a function is an onto function. (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 11-Oct-2013) (Revised by AV, 23-Jan-2020)

		Ref	Expression
	Hypotheses	mndpf.b	$⊢ B = {Base}_{G}$
		mndpf.p	$⊢ \underset{˙}{⨣} = +_{𝑓} (G)$
	Assertion	mndpfo	$⊢ G \in Mnd \to \underset{˙}{⨣} : B \times B \underset{onto}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		mndpf.b	$⊢ B = {Base}_{G}$
2		mndpf.p	$⊢ \underset{˙}{⨣} = +_{𝑓} (G)$
3	1 2	mndplusf	$⊢ G \in Mnd \to \underset{˙}{⨣} : B \times B ⟶ B$
4		simpr	$⊢ (G \in Mnd \land x \in B) \to x \in B$
5		eqid	$⊢ 0_{G} = 0_{G}$
6	1 5	mndidcl	$⊢ G \in Mnd \to 0_{G} \in B$
7	6	adantr	$⊢ (G \in Mnd \land x \in B) \to 0_{G} \in B$
8		eqid	$⊢ +_{G} = +_{G}$
9	1 8 5	mndrid	$⊢ (G \in Mnd \land x \in B) \to x +_{G} 0_{G} = x$
10	9	eqcomd	$⊢ (G \in Mnd \land x \in B) \to x = x +_{G} 0_{G}$
11		rspceov	$⊢ (x \in B \land 0_{G} \in B \land x = x +_{G} 0_{G}) \to \exists y \in B \exists z \in B x = y +_{G} z$
12	4 7 10 11	syl3anc	$⊢ (G \in Mnd \land x \in B) \to \exists y \in B \exists z \in B x = y +_{G} z$
13	1 8 2	plusfval	$⊢ (y \in B \land z \in B) \to y \underset{˙}{⨣} z = y +_{G} z$
14	13	eqeq2d	$⊢ (y \in B \land z \in B) \to (x = y \underset{˙}{⨣} z \leftrightarrow x = y +_{G} z)$
15	14	2rexbiia	$⊢ \exists y \in B \exists z \in B x = y \underset{˙}{⨣} z \leftrightarrow \exists y \in B \exists z \in B x = y +_{G} z$
16	12 15	sylibr	$⊢ (G \in Mnd \land x \in B) \to \exists y \in B \exists z \in B x = y \underset{˙}{⨣} z$
17	16	ralrimiva	$⊢ G \in Mnd \to \forall x \in B \exists y \in B \exists z \in B x = y \underset{˙}{⨣} z$
18		foov	$⊢ \underset{˙}{⨣} : B \times B \underset{onto}{⟶} B \leftrightarrow (\underset{˙}{⨣} : B \times B ⟶ B \land \forall x \in B \exists y \in B \exists z \in B x = y \underset{˙}{⨣} z)$
19	3 17 18	sylanbrc	$⊢ G \in Mnd \to \underset{˙}{⨣} : B \times B \underset{onto}{⟶} B$