Metamath Proof Explorer

Theorem imasgim

Description: A relabeling of the elements of a group induces an isomorphism to the relabeled group.MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015) (Revised by Mario Carneiro, 11-Aug-2015)

Ref Expression
Hypotheses imasgim.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
imasgim.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
imasgim.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
imasgim.r ⊢ ( 𝜑 → 𝑅 ∈ Grp )
Assertion imasgim ( 𝜑 → 𝐹 ∈ ( 𝑅 GrpIso 𝑈 ) )

Proof

Step Hyp Ref Expression
1 imasgim.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2 imasgim.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 imasgim.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
4 imasgim.r ⊢ ( 𝜑 → 𝑅 ∈ Grp )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
7 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
8 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
9 eqidd ⊢ ( 𝜑 → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) )
10 f1ofo ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → 𝐹 : 𝑉 –onto→ 𝐵 )
11 3 10 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
12 3 f1ocpbl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑐 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑑 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑐 ( +g ‘ 𝑅 ) 𝑑 ) ) ) )
13 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
14 1 2 9 11 12 4 13 imasgrp ⊢ ( 𝜑 → ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑈 ) ) )
15 14 simpld ⊢ ( 𝜑 → 𝑈 ∈ Grp )
16 1 2 11 4 imasbas ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑈 ) )
17 f1oeq3 ⊢ ( 𝐵 = ( Base ‘ 𝑈 ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 ↔ 𝐹 : 𝑉 –1-1-onto→ ( Base ‘ 𝑈 ) ) )
18 16 17 syl ⊢ ( 𝜑 → ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 ↔ 𝐹 : 𝑉 –1-1-onto→ ( Base ‘ 𝑈 ) ) )
19 3 18 mpbid ⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ ( Base ‘ 𝑈 ) )
20 2 f1oeq2d ⊢ ( 𝜑 → ( 𝐹 : 𝑉 –1-1-onto→ ( Base ‘ 𝑈 ) ↔ 𝐹 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑈 ) ) )
21 19 20 mpbid ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑈 ) )
22 f1of ⊢ ( 𝐹 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑈 ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑈 ) )
23 21 22 syl ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑈 ) )
24 2 eleq2d ⊢ ( 𝜑 → ( 𝑎 ∈ 𝑉 ↔ 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
25 2 eleq2d ⊢ ( 𝜑 → ( 𝑏 ∈ 𝑉 ↔ 𝑏 ∈ ( Base ‘ 𝑅 ) ) )
26 24 25 anbi12d ⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ↔ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) )
27 11 12 1 2 4 7 8 imasaddval ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑏 ) ) = ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) )
28 27 eqcomd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑏 ) ) )
29 28 3expib ⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑏 ) ) ) )
30 26 29 sylbird ⊢ ( 𝜑 → ( ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑏 ) ) ) )
31 30 imp ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑏 ) ) )
32 5 6 7 8 4 15 23 31 isghmd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 GrpHom 𝑈 ) )
33 5 6 isgim ⊢ ( 𝐹 ∈ ( 𝑅 GrpIso 𝑈 ) ↔ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑈 ) ∧ 𝐹 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑈 ) ) )
34 32 21 33 sylanbrc ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 GrpIso 𝑈 ) )