giclcl

Description: Isomorphism implies the left side is a group. (Contributed by Stefan O'Rear, 25-Jan-2015)

		Ref	Expression
	Assertion	giclcl	$⊢ R ≃_{𝑔} S \to R \in Grp$

Step	Hyp	Ref	Expression
1		brgic	$⊢ R ≃_{𝑔} S \leftrightarrow R GrpIso S \neq \emptyset$
2		n0	$⊢ R GrpIso S \neq \emptyset \leftrightarrow \exists f f \in (R GrpIso S)$
3	1 2	bitri	$⊢ R ≃_{𝑔} S \leftrightarrow \exists f f \in (R GrpIso S)$
4		gimghm	$⊢ f \in (R GrpIso S) \to f \in (R GrpHom S)$
5		ghmgrp1	$⊢ f \in (R GrpHom S) \to R \in Grp$
6	4 5	syl	$⊢ f \in (R GrpIso S) \to R \in Grp$
7	6	exlimiv	$⊢ \exists f f \in (R GrpIso S) \to R \in Grp$
8	3 7	sylbi	$⊢ R ≃_{𝑔} S \to R \in Grp$

Metamath Proof Explorer