Metamath Proof Explorer

Theorem ghmf1o

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

Ref Expression
Hypotheses ghmf1o.x ⊢ 𝑋 = ( Base ‘ 𝑆 )
ghmf1o.y ⊢ 𝑌 = ( Base ‘ 𝑇 )
Assertion ghmf1o ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ↔ ◡ 𝐹 ∈ ( 𝑇 GrpHom 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 ghmf1o.x ⊢ 𝑋 = ( Base ‘ 𝑆 )
2 ghmf1o.y ⊢ 𝑌 = ( Base ‘ 𝑇 )
3 ghmgrp2 ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑇 ∈ Grp )
4 ghmgrp1 ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑆 ∈ Grp )
5 3 4 jca ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝑇 ∈ Grp ∧ 𝑆 ∈ Grp ) )
6 5 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝑇 ∈ Grp ∧ 𝑆 ∈ Grp ) )
7 f1ocnv ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 )
8 7 adantl ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 )
9 f1of ⊢ ( ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
10 8 9 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
11 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
12 10 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
13 simprl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → 𝑥 ∈ 𝑌 )
14 12 13 ffvelcdmd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 )
15 simprr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → 𝑦 ∈ 𝑌 )
16 12 15 ffvelcdmd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑋 )
17 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
18 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
19 1 17 18 ghmlin ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑋 ) → ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑦 ) ) ) )
20 11 14 16 19 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑦 ) ) ) )
21 simplr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
22 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
23 21 13 22 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
24 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑦 ) ) = 𝑦 )
25 21 15 24 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑦 ) ) = 𝑦 )
26 23 25 oveq12d ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) )
27 20 26 eqtrd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) )
28 11 4 syl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → 𝑆 ∈ Grp )
29 1 17 grpcl ⊢ ( ( 𝑆 ∈ Grp ∧ ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑋 ) → ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ∈ 𝑋 )
30 28 14 16 29 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ∈ 𝑋 )
31 f1ocnvfv ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ∈ 𝑋 ) → ( ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) → ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) )
32 21 30 31 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) → ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) )
33 27 32 mpd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑦 ) ) )
34 33 ralrimivva ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑦 ) ) )
35 10 34 jca ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( ◡ 𝐹 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) )
36 2 1 18 17 isghm ⊢ ( ◡ 𝐹 ∈ ( 𝑇 GrpHom 𝑆 ) ↔ ( ( 𝑇 ∈ Grp ∧ 𝑆 ∈ Grp ) ∧ ( ◡ 𝐹 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) ) )
37 6 35 36 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ◡ 𝐹 ∈ ( 𝑇 GrpHom 𝑆 ) )
38 1 2 ghmf ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 : 𝑋 ⟶ 𝑌 )
39 38 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ◡ 𝐹 ∈ ( 𝑇 GrpHom 𝑆 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
40 39 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ◡ 𝐹 ∈ ( 𝑇 GrpHom 𝑆 ) ) → 𝐹 Fn 𝑋 )
41 2 1 ghmf ⊢ ( ◡ 𝐹 ∈ ( 𝑇 GrpHom 𝑆 ) → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
42 41 adantl ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ◡ 𝐹 ∈ ( 𝑇 GrpHom 𝑆 ) ) → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
43 42 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ◡ 𝐹 ∈ ( 𝑇 GrpHom 𝑆 ) ) → ◡ 𝐹 Fn 𝑌 )
44 dff1o4 ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ↔ ( 𝐹 Fn 𝑋 ∧ ◡ 𝐹 Fn 𝑌 ) )
45 40 43 44 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ◡ 𝐹 ∈ ( 𝑇 GrpHom 𝑆 ) ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
46 37 45 impbida ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ↔ ◡ 𝐹 ∈ ( 𝑇 GrpHom 𝑆 ) ) )