This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mndfo

Description: The addition operation of a monoid is an onto function (assuming it is a function). (Contributed by Mario Carneiro, 11-Oct-2013) (Proof shortened by AV, 23-Jan-2020)

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

Proof

Step	Hyp	Ref	Expression
1		mndfo.b	$⊢ B = {Base}_{G}$
2		mndfo.p	$⊢ \underset{˙}{+} = +_{G}$
3		eqid	$⊢ +_{𝑓} (G) = +_{𝑓} (G)$
4	1 3	mndpfo	$⊢ G \in Mnd \to +_{𝑓} (G) : B \times B \underset{onto}{⟶} B$
5	4	adantr	$⊢ (G \in Mnd \land \underset{˙}{+} Fn (B \times B)) \to +_{𝑓} (G) : B \times B \underset{onto}{⟶} B$
6	1 2 3	plusfeq	$⊢ \underset{˙}{+} Fn (B \times B) \to +_{𝑓} (G) = \underset{˙}{+}$
7	6	eqcomd	$⊢ \underset{˙}{+} Fn (B \times B) \to \underset{˙}{+} = +_{𝑓} (G)$
8	7	adantl	$⊢ (G \in Mnd \land \underset{˙}{+} Fn (B \times B)) \to \underset{˙}{+} = +_{𝑓} (G)$
9		foeq1	$⊢ \underset{˙}{+} = +_{𝑓} (G) \to (\underset{˙}{+} : B \times B \underset{onto}{⟶} B \leftrightarrow +_{𝑓} (G) : B \times B \underset{onto}{⟶} B)$
10	8 9	syl	$⊢ (G \in Mnd \land \underset{˙}{+} Fn (B \times B)) \to (\underset{˙}{+} : B \times B \underset{onto}{⟶} B \leftrightarrow +_{𝑓} (G) : B \times B \underset{onto}{⟶} B)$
11	5 10	mpbird	$⊢ (G \in Mnd \land \underset{˙}{+} Fn (B \times B)) \to \underset{˙}{+} : B \times B \underset{onto}{⟶} B$