imasgrpf1

Description: The image of a group under an injection is a group. (Contributed by Mario Carneiro, 20-Aug-2015)

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

Step	Hyp	Ref	Expression
1		imasgrpf1.u	$⊢ U = F “_{𝑠} R$
2		imasgrpf1.v	$⊢ V = {Base}_{R}$
3	1	a1i	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Grp) \to U = F “_{𝑠} R$
4	2	a1i	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Grp) \to V = {Base}_{R}$
5		eqidd	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Grp) \to +_{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 Grp) \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 Grp) \to F : V \underset{onto}{⟶} ran F$
10	7	f1ocpbl	$⊢ ((F : V \underset{1-1}{⟶} B \land R \in Grp) \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 Grp) \to R \in Grp$
12		eqid	$⊢ 0_{R} = 0_{R}$
13	3 4 5 9 10 11 12	imasgrp	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Grp) \to (U \in Grp \land F (0_{R}) = 0_{U})$
14	13	simpld	$⊢ (F : V \underset{1-1}{⟶} B \land R \in Grp) \to U \in Grp$

Metamath Proof Explorer