isgim

Description: An isomorphism of groups is a bijective homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015)

	Ref	Expression
Hypotheses	isgim.b	$⊢ B = {Base}_{R}$
	isgim.c	$⊢ C = {Base}_{S}$
Assertion	isgim	$⊢ F \in (R GrpIso S) \leftrightarrow (F \in (R GrpHom S) \land F : B \underset{1-1 onto}{⟶} C)$

Proof

Step	Hyp	Ref	Expression
1		isgim.b	$⊢ B = {Base}_{R}$
2		isgim.c	$⊢ C = {Base}_{S}$
3		df-3an	$⊢ (R \in Grp \land S \in Grp \land F \in \{c \in (R GrpHom S) \| c : B \underset{1-1 onto}{⟶} C\}) \leftrightarrow ((R \in Grp \land S \in Grp) \land F \in \{c \in (R GrpHom S) \| c : B \underset{1-1 onto}{⟶} C\})$
4		df-gim	$⊢ GrpIso = (a \in Grp, b \in Grp ⟼ \{c \in (a GrpHom b) \| c : {Base}_{a} \underset{1-1 onto}{⟶} {Base}_{b}\})$
5		ovex	$⊢ a GrpHom b \in V$
6	5	rabex	$⊢ \{c \in (a GrpHom b) \| c : {Base}_{a} \underset{1-1 onto}{⟶} {Base}_{b}\} \in V$
7		oveq12	$⊢ (a = R \land b = S) \to a GrpHom b = R GrpHom S$
8		fveq2	$⊢ a = R \to {Base}_{a} = {Base}_{R}$
9	8 1	eqtr4di	$⊢ a = R \to {Base}_{a} = B$
10		fveq2	$⊢ b = S \to {Base}_{b} = {Base}_{S}$
11	10 2	eqtr4di	$⊢ b = S \to {Base}_{b} = C$
12		f1oeq23	$⊢ ({Base}_{a} = B \land {Base}_{b} = C) \to (c : {Base}_{a} \underset{1-1 onto}{⟶} {Base}_{b} \leftrightarrow c : B \underset{1-1 onto}{⟶} C)$
13	9 11 12	syl2an	$⊢ (a = R \land b = S) \to (c : {Base}_{a} \underset{1-1 onto}{⟶} {Base}_{b} \leftrightarrow c : B \underset{1-1 onto}{⟶} C)$
14	7 13	rabeqbidv	$⊢ (a = R \land b = S) \to \{c \in (a GrpHom b) \| c : {Base}_{a} \underset{1-1 onto}{⟶} {Base}_{b}\} = \{c \in (R GrpHom S) \| c : B \underset{1-1 onto}{⟶} C\}$
15	4 6 14	elovmpo	$⊢ F \in (R GrpIso S) \leftrightarrow (R \in Grp \land S \in Grp \land F \in \{c \in (R GrpHom S) \| c : B \underset{1-1 onto}{⟶} C\})$
16		ghmgrp1	$⊢ F \in (R GrpHom S) \to R \in Grp$
17		ghmgrp2	$⊢ F \in (R GrpHom S) \to S \in Grp$
18	16 17	jca	$⊢ F \in (R GrpHom S) \to (R \in Grp \land S \in Grp)$
19	18	adantr	$⊢ (F \in (R GrpHom S) \land F : B \underset{1-1 onto}{⟶} C) \to (R \in Grp \land S \in Grp)$
20	19	pm4.71ri	$⊢ (F \in (R GrpHom S) \land F : B \underset{1-1 onto}{⟶} C) \leftrightarrow ((R \in Grp \land S \in Grp) \land (F \in (R GrpHom S) \land F : B \underset{1-1 onto}{⟶} C))$
21		f1oeq1	$⊢ c = F \to (c : B \underset{1-1 onto}{⟶} C \leftrightarrow F : B \underset{1-1 onto}{⟶} C)$
22	21	elrab	$⊢ F \in \{c \in (R GrpHom S) \| c : B \underset{1-1 onto}{⟶} C\} \leftrightarrow (F \in (R GrpHom S) \land F : B \underset{1-1 onto}{⟶} C)$
23	22	anbi2i	$⊢ ((R \in Grp \land S \in Grp) \land F \in \{c \in (R GrpHom S) \| c : B \underset{1-1 onto}{⟶} C\}) \leftrightarrow ((R \in Grp \land S \in Grp) \land (F \in (R GrpHom S) \land F : B \underset{1-1 onto}{⟶} C))$
24	20 23	bitr4i	$⊢ (F \in (R GrpHom S) \land F : B \underset{1-1 onto}{⟶} C) \leftrightarrow ((R \in Grp \land S \in Grp) \land F \in \{c \in (R GrpHom S) \| c : B \underset{1-1 onto}{⟶} C\})$
25	3 15 24	3bitr4i	$⊢ F \in (R GrpIso S) \leftrightarrow (F \in (R GrpHom S) \land F : B \underset{1-1 onto}{⟶} C)$

Metamath Proof Explorer

Theorem isgim

Proof