Metamath Proof Explorer

Theorem 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 ∈ R GrpIso S ↔ F ∈ R GrpHom S ∧ F : B ⟶ 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 ∈ Grp ∧ S ∈ Grp ∧ F ∈ c ∈ R GrpHom S | c : B ⟶ 1-1 onto C ↔ R ∈ Grp ∧ S ∈ Grp ∧ F ∈ c ∈ R GrpHom S | c : B ⟶ 1-1 onto C
4 df-gim ⊢ GrpIso = a ∈ Grp , b ∈ Grp ⟼ c ∈ a GrpHom b | c : Base a ⟶ 1-1 onto Base b
5 ovex ⊢ a GrpHom b ∈ V
6 5 rabex ⊢ c ∈ a GrpHom b | c : Base a ⟶ 1-1 onto Base b ∈ V
7 oveq12 ⊢ a = R ∧ b = S → a GrpHom b = R GrpHom S
8 fveq2 ⊢ a = R → Base a = Base R
9 8 1 eqtr4di ⊢ a = R → Base a = B
10 fveq2 ⊢ b = S → Base b = Base S
11 10 2 eqtr4di ⊢ b = S → Base b = C
12 f1oeq23 ⊢ Base a = B ∧ Base b = C → c : Base a ⟶ 1-1 onto Base b ↔ c : B ⟶ 1-1 onto C
13 9 11 12 syl2an ⊢ a = R ∧ b = S → c : Base a ⟶ 1-1 onto Base b ↔ c : B ⟶ 1-1 onto C
14 7 13 rabeqbidv ⊢ a = R ∧ b = S → c ∈ a GrpHom b | c : Base a ⟶ 1-1 onto Base b = c ∈ R GrpHom S | c : B ⟶ 1-1 onto C
15 4 6 14 elovmpo ⊢ F ∈ R GrpIso S ↔ R ∈ Grp ∧ S ∈ Grp ∧ F ∈ c ∈ R GrpHom S | c : B ⟶ 1-1 onto C
16 ghmgrp1 ⊢ F ∈ R GrpHom S → R ∈ Grp
17 ghmgrp2 ⊢ F ∈ R GrpHom S → S ∈ Grp
18 16 17 jca ⊢ F ∈ R GrpHom S → R ∈ Grp ∧ S ∈ Grp
19 18 adantr ⊢ F ∈ R GrpHom S ∧ F : B ⟶ 1-1 onto C → R ∈ Grp ∧ S ∈ Grp
20 19 pm4.71ri ⊢ F ∈ R GrpHom S ∧ F : B ⟶ 1-1 onto C ↔ R ∈ Grp ∧ S ∈ Grp ∧ F ∈ R GrpHom S ∧ F : B ⟶ 1-1 onto C
21 f1oeq1 ⊢ c = F → c : B ⟶ 1-1 onto C ↔ F : B ⟶ 1-1 onto C
22 21 elrab ⊢ F ∈ c ∈ R GrpHom S | c : B ⟶ 1-1 onto C ↔ F ∈ R GrpHom S ∧ F : B ⟶ 1-1 onto C
23 22 anbi2i ⊢ R ∈ Grp ∧ S ∈ Grp ∧ F ∈ c ∈ R GrpHom S | c : B ⟶ 1-1 onto C ↔ R ∈ Grp ∧ S ∈ Grp ∧ F ∈ R GrpHom S ∧ F : B ⟶ 1-1 onto C
24 20 23 bitr4i ⊢ F ∈ R GrpHom S ∧ F : B ⟶ 1-1 onto C ↔ R ∈ Grp ∧ S ∈ Grp ∧ F ∈ c ∈ R GrpHom S | c : B ⟶ 1-1 onto C
25 3 15 24 3bitr4i ⊢ F ∈ R GrpIso S ↔ F ∈ R GrpHom S ∧ F : B ⟶ 1-1 onto C