ghmf1o

Description: A bijective group homomorphism is an isomorphism. (Contributed by Mario Carneiro, 13-Jan-2015)

	Ref	Expression
Hypotheses	ghmf1o.x	$⊢ X = {Base}_{S}$
	ghmf1o.y	$⊢ Y = {Base}_{T}$
Assertion	ghmf1o	$⊢ F \in (S GrpHom T) \to (F : X \underset{1-1 onto}{⟶} Y \leftrightarrow F^{-1} \in (T GrpHom S))$

Proof

Step	Hyp	Ref	Expression
1		ghmf1o.x	$⊢ X = {Base}_{S}$
2		ghmf1o.y	$⊢ Y = {Base}_{T}$
3		ghmgrp2	$⊢ F \in (S GrpHom T) \to T \in Grp$
4		ghmgrp1	$⊢ F \in (S GrpHom T) \to S \in Grp$
5	3 4	jca	$⊢ F \in (S GrpHom T) \to (T \in Grp \land S \in Grp)$
6	5	adantr	$⊢ (F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \to (T \in Grp \land S \in Grp)$
7		f1ocnv	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F^{-1} : Y \underset{1-1 onto}{⟶} X$
8	7	adantl	$⊢ (F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \to F^{-1} : Y \underset{1-1 onto}{⟶} X$
9		f1of	$⊢ F^{-1} : Y \underset{1-1 onto}{⟶} X \to F^{-1} : Y ⟶ X$
10	8 9	syl	$⊢ (F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \to F^{-1} : Y ⟶ X$
11		simpll	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \land (x \in Y \land y \in Y)) \to F \in (S GrpHom T)$
12	10	adantr	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \land (x \in Y \land y \in Y)) \to F^{-1} : Y ⟶ X$
13		simprl	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \land (x \in Y \land y \in Y)) \to x \in Y$
14	12 13	ffvelrnd	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \land (x \in Y \land y \in Y)) \to F^{-1} (x) \in X$
15		simprr	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \land (x \in Y \land y \in Y)) \to y \in Y$
16	12 15	ffvelrnd	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \land (x \in Y \land y \in Y)) \to F^{-1} (y) \in X$
17		eqid	$⊢ +_{S} = +_{S}$
18		eqid	$⊢ +_{T} = +_{T}$
19	1 17 18	ghmlin	$⊢ (F \in (S GrpHom T) \land F^{-1} (x) \in X \land F^{-1} (y) \in X) \to F (F^{-1} (x) +_{S} F^{-1} (y)) = F (F^{-1} (x)) +_{T} F (F^{-1} (y))$
20	11 14 16 19	syl3anc	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \land (x \in Y \land y \in Y)) \to F (F^{-1} (x) +_{S} F^{-1} (y)) = F (F^{-1} (x)) +_{T} F (F^{-1} (y))$
21		simplr	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \land (x \in Y \land y \in Y)) \to F : X \underset{1-1 onto}{⟶} Y$
22		f1ocnvfv2	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land x \in Y) \to F (F^{-1} (x)) = x$
23	21 13 22	syl2anc	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \land (x \in Y \land y \in Y)) \to F (F^{-1} (x)) = x$
24		f1ocnvfv2	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land y \in Y) \to F (F^{-1} (y)) = y$
25	21 15 24	syl2anc	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \land (x \in Y \land y \in Y)) \to F (F^{-1} (y)) = y$
26	23 25	oveq12d	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \land (x \in Y \land y \in Y)) \to F (F^{-1} (x)) +_{T} F (F^{-1} (y)) = x +_{T} y$
27	20 26	eqtrd	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \land (x \in Y \land y \in Y)) \to F (F^{-1} (x) +_{S} F^{-1} (y)) = x +_{T} y$
28	11 4	syl	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \land (x \in Y \land y \in Y)) \to S \in Grp$
29	1 17	grpcl	$⊢ (S \in Grp \land F^{-1} (x) \in X \land F^{-1} (y) \in X) \to F^{-1} (x) +_{S} F^{-1} (y) \in X$
30	28 14 16 29	syl3anc	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \land (x \in Y \land y \in Y)) \to F^{-1} (x) +_{S} F^{-1} (y) \in X$
31		f1ocnvfv	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land F^{-1} (x) +_{S} F^{-1} (y) \in X) \to (F (F^{-1} (x) +_{S} F^{-1} (y)) = x +_{T} y \to F^{-1} (x +_{T} y) = F^{-1} (x) +_{S} F^{-1} (y))$
32	21 30 31	syl2anc	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \land (x \in Y \land y \in Y)) \to (F (F^{-1} (x) +_{S} F^{-1} (y)) = x +_{T} y \to F^{-1} (x +_{T} y) = F^{-1} (x) +_{S} F^{-1} (y))$
33	27 32	mpd	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \land (x \in Y \land y \in Y)) \to F^{-1} (x +_{T} y) = F^{-1} (x) +_{S} F^{-1} (y)$
34	33	ralrimivva	$⊢ (F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \to \forall x \in Y \forall y \in Y F^{-1} (x +_{T} y) = F^{-1} (x) +_{S} F^{-1} (y)$
35	10 34	jca	$⊢ (F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \to (F^{-1} : Y ⟶ X \land \forall x \in Y \forall y \in Y F^{-1} (x +_{T} y) = F^{-1} (x) +_{S} F^{-1} (y))$
36	2 1 18 17	isghm	$⊢ F^{-1} \in (T GrpHom S) \leftrightarrow ((T \in Grp \land S \in Grp) \land (F^{-1} : Y ⟶ X \land \forall x \in Y \forall y \in Y F^{-1} (x +_{T} y) = F^{-1} (x) +_{S} F^{-1} (y)))$
37	6 35 36	sylanbrc	$⊢ (F \in (S GrpHom T) \land F : X \underset{1-1 onto}{⟶} Y) \to F^{-1} \in (T GrpHom S)$
38	1 2	ghmf	$⊢ F \in (S GrpHom T) \to F : X ⟶ Y$
39	38	adantr	$⊢ (F \in (S GrpHom T) \land F^{-1} \in (T GrpHom S)) \to F : X ⟶ Y$
40	39	ffnd	$⊢ (F \in (S GrpHom T) \land F^{-1} \in (T GrpHom S)) \to F Fn X$
41	2 1	ghmf	$⊢ F^{-1} \in (T GrpHom S) \to F^{-1} : Y ⟶ X$
42	41	adantl	$⊢ (F \in (S GrpHom T) \land F^{-1} \in (T GrpHom S)) \to F^{-1} : Y ⟶ X$
43	42	ffnd	$⊢ (F \in (S GrpHom T) \land F^{-1} \in (T GrpHom S)) \to F^{-1} Fn Y$
44		dff1o4	$⊢ F : X \underset{1-1 onto}{⟶} Y \leftrightarrow (F Fn X \land F^{-1} Fn Y)$
45	40 43 44	sylanbrc	$⊢ (F \in (S GrpHom T) \land F^{-1} \in (T GrpHom S)) \to F : X \underset{1-1 onto}{⟶} Y$
46	37 45	impbida	$⊢ F \in (S GrpHom T) \to (F : X \underset{1-1 onto}{⟶} Y \leftrightarrow F^{-1} \in (T GrpHom S))$

Metamath Proof Explorer

Theorem ghmf1o

Proof