This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
isgim.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
Assertion isgim ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 isgim.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 isgim.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
3 df-3an ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑆 ∈ Grp ∧ 𝐹 ∈ { 𝑐 ∈ ( 𝑅 GrpHom 𝑆 ) ∣ 𝑐 : 𝐵 –1-1-onto→ 𝐶 } ) ↔ ( ( 𝑅 ∈ Grp ∧ 𝑆 ∈ Grp ) ∧ 𝐹 ∈ { 𝑐 ∈ ( 𝑅 GrpHom 𝑆 ) ∣ 𝑐 : 𝐵 –1-1-onto→ 𝐶 } ) )
4 df-gim ⊢ GrpIso = ( 𝑎 ∈ Grp , 𝑏 ∈ Grp ↦ { 𝑐 ∈ ( 𝑎 GrpHom 𝑏 ) ∣ 𝑐 : ( Base ‘ 𝑎 ) –1-1-onto→ ( Base ‘ 𝑏 ) } )
5 ovex ⊢ ( 𝑎 GrpHom 𝑏 ) ∈ V
6 5 rabex ⊢ { 𝑐 ∈ ( 𝑎 GrpHom 𝑏 ) ∣ 𝑐 : ( Base ‘ 𝑎 ) –1-1-onto→ ( Base ‘ 𝑏 ) } ∈ V
7 oveq12 ⊢ ( ( 𝑎 = 𝑅 ∧ 𝑏 = 𝑆 ) → ( 𝑎 GrpHom 𝑏 ) = ( 𝑅 GrpHom 𝑆 ) )
8 fveq2 ⊢ ( 𝑎 = 𝑅 → ( Base ‘ 𝑎 ) = ( Base ‘ 𝑅 ) )
9 8 1 eqtr4di ⊢ ( 𝑎 = 𝑅 → ( Base ‘ 𝑎 ) = 𝐵 )
10 fveq2 ⊢ ( 𝑏 = 𝑆 → ( Base ‘ 𝑏 ) = ( Base ‘ 𝑆 ) )
11 10 2 eqtr4di ⊢ ( 𝑏 = 𝑆 → ( Base ‘ 𝑏 ) = 𝐶 )
12 f1oeq23 ⊢ ( ( ( Base ‘ 𝑎 ) = 𝐵 ∧ ( Base ‘ 𝑏 ) = 𝐶 ) → ( 𝑐 : ( Base ‘ 𝑎 ) –1-1-onto→ ( Base ‘ 𝑏 ) ↔ 𝑐 : 𝐵 –1-1-onto→ 𝐶 ) )
13 9 11 12 syl2an ⊢ ( ( 𝑎 = 𝑅 ∧ 𝑏 = 𝑆 ) → ( 𝑐 : ( Base ‘ 𝑎 ) –1-1-onto→ ( Base ‘ 𝑏 ) ↔ 𝑐 : 𝐵 –1-1-onto→ 𝐶 ) )
14 7 13 rabeqbidv ⊢ ( ( 𝑎 = 𝑅 ∧ 𝑏 = 𝑆 ) → { 𝑐 ∈ ( 𝑎 GrpHom 𝑏 ) ∣ 𝑐 : ( Base ‘ 𝑎 ) –1-1-onto→ ( Base ‘ 𝑏 ) } = { 𝑐 ∈ ( 𝑅 GrpHom 𝑆 ) ∣ 𝑐 : 𝐵 –1-1-onto→ 𝐶 } )
15 4 6 14 elovmpo ⊢ ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) ↔ ( 𝑅 ∈ Grp ∧ 𝑆 ∈ Grp ∧ 𝐹 ∈ { 𝑐 ∈ ( 𝑅 GrpHom 𝑆 ) ∣ 𝑐 : 𝐵 –1-1-onto→ 𝐶 } ) )
16 ghmgrp1 ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝑅 ∈ Grp )
17 ghmgrp2 ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝑆 ∈ Grp )
18 16 17 jca ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝑅 ∈ Grp ∧ 𝑆 ∈ Grp ) )
19 18 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( 𝑅 ∈ Grp ∧ 𝑆 ∈ Grp ) )
20 19 pm4.71ri ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ↔ ( ( 𝑅 ∈ Grp ∧ 𝑆 ∈ Grp ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ) )
21 f1oeq1 ⊢ ( 𝑐 = 𝐹 → ( 𝑐 : 𝐵 –1-1-onto→ 𝐶 ↔ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) )
22 21 elrab ⊢ ( 𝐹 ∈ { 𝑐 ∈ ( 𝑅 GrpHom 𝑆 ) ∣ 𝑐 : 𝐵 –1-1-onto→ 𝐶 } ↔ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) )
23 22 anbi2i ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝑆 ∈ Grp ) ∧ 𝐹 ∈ { 𝑐 ∈ ( 𝑅 GrpHom 𝑆 ) ∣ 𝑐 : 𝐵 –1-1-onto→ 𝐶 } ) ↔ ( ( 𝑅 ∈ Grp ∧ 𝑆 ∈ Grp ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ) )
24 20 23 bitr4i ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ↔ ( ( 𝑅 ∈ Grp ∧ 𝑆 ∈ Grp ) ∧ 𝐹 ∈ { 𝑐 ∈ ( 𝑅 GrpHom 𝑆 ) ∣ 𝑐 : 𝐵 –1-1-onto→ 𝐶 } ) )
25 3 15 24 3bitr4i ⊢ ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) )