imasmndf1

Description: The image of a monoid under an injection is a monoid. (Contributed by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Hypotheses	imasmndf1.u	$⊢ U = F “_{𝑠} R$
	imasmndf1.v	$⊢ V = {Base}_{R}$
Assertion	imasmndf1	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Mnd) \to U \in Mnd$

Step	Hyp	Ref	Expression
1		imasmndf1.u	$⊢ U = F “_{𝑠} R$
2		imasmndf1.v	$⊢ V = {Base}_{R}$
3	1	a1i	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Mnd) \to U = F “_{𝑠} R$
4	2	a1i	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Mnd) \to V = {Base}_{R}$
5		eqid	$⊢ +_{R} = +_{R}$
6		f1f1orn	$⊢ F : V \underset{1-1}{⟶} B \to F : V \underset{1-1 onto}{⟶} ran F$
7	6	adantr	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Mnd) \to F : V \underset{1-1 onto}{⟶} ran F$
8		f1ofo	$⊢ F : V \underset{1-1 onto}{⟶} ran F \to F : V \underset{onto}{⟶} ran F$
9	7 8	syl	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Mnd) \to F : V \underset{onto}{⟶} ran F$
10	7	f1ocpbl	$⊢ ((F : V \underset{1-1}{⟶} B \land R \in Mnd) \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a +_{R} b) = F (p +_{R} q))$
11		simpr	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Mnd) \to R \in Mnd$
12		eqid	$⊢ 0_{R} = 0_{R}$
13	3 4 5 9 10 11 12	imasmnd	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Mnd) \to (U \in Mnd \land F (0_{R}) = 0_{U})$
14	13	simpld	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Mnd) \to U \in Mnd$

Metamath Proof Explorer