Metamath Proof Explorer

Theorem cygznlem3

Description: A cyclic group with n elements is isomorphic to ZZ / n ZZ . (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses cygzn.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
cygzn.n ⊢ 𝑁 = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 )
cygzn.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
cygzn.m ⊢ · = ( .g ‘ 𝐺 )
cygzn.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
cygzn.e ⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 }
cygzn.g ⊢ ( 𝜑 → 𝐺 ∈ CycGrp )
cygzn.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
cygzn.f ⊢ 𝐹 = ran ( 𝑚 ∈ ℤ ↦ ⟨ ( 𝐿 ‘ 𝑚 ) , ( 𝑚 · 𝑋 ) ⟩ )
Assertion cygznlem3 ( 𝜑 → 𝐺 ≃𝑔 𝑌 )

Proof

Step Hyp Ref Expression
1 cygzn.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 cygzn.n ⊢ 𝑁 = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 )
3 cygzn.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
4 cygzn.m ⊢ · = ( .g ‘ 𝐺 )
5 cygzn.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
6 cygzn.e ⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 }
7 cygzn.g ⊢ ( 𝜑 → 𝐺 ∈ CycGrp )
8 cygzn.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
9 cygzn.f ⊢ 𝐹 = ran ( 𝑚 ∈ ℤ ↦ ⟨ ( 𝐿 ‘ 𝑚 ) , ( 𝑚 · 𝑋 ) ⟩ )
10 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
11 eqid ⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
12 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
13 hashcl ⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
15 0nn0 ⊢ 0 ∈ ℕ0
16 15 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ Fin ) → 0 ∈ ℕ0 )
17 14 16 ifclda ⊢ ( 𝜑 → if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ∈ ℕ0 )
18 2 17 eqeltrid ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
19 3 zncrng ⊢ ( 𝑁 ∈ ℕ0 → 𝑌 ∈ CRing )
20 crngring ⊢ ( 𝑌 ∈ CRing → 𝑌 ∈ Ring )
21 ringgrp ⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Grp )
22 18 19 20 21 4syl ⊢ ( 𝜑 → 𝑌 ∈ Grp )
23 cyggrp ⊢ ( 𝐺 ∈ CycGrp → 𝐺 ∈ Grp )
24 7 23 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
25 1 2 3 4 5 6 7 8 9 cygznlem2a ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑌 ) ⟶ 𝐵 )
26 3 10 5 znzrhfo ⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑌 ) )
27 18 26 syl ⊢ ( 𝜑 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑌 ) )
28 foelrn ⊢ ( ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑌 ) ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → ∃ 𝑖 ∈ ℤ 𝑎 = ( 𝐿 ‘ 𝑖 ) )
29 27 28 sylan ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → ∃ 𝑖 ∈ ℤ 𝑎 = ( 𝐿 ‘ 𝑖 ) )
30 foelrn ⊢ ( ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) → ∃ 𝑗 ∈ ℤ 𝑏 = ( 𝐿 ‘ 𝑗 ) )
31 27 30 sylan ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) → ∃ 𝑗 ∈ ℤ 𝑏 = ( 𝐿 ‘ 𝑗 ) )
32 29 31 anim12dan ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → ( ∃ 𝑖 ∈ ℤ 𝑎 = ( 𝐿 ‘ 𝑖 ) ∧ ∃ 𝑗 ∈ ℤ 𝑏 = ( 𝐿 ‘ 𝑗 ) ) )
33 reeanv ⊢ ( ∃ 𝑖 ∈ ℤ ∃ 𝑗 ∈ ℤ ( 𝑎 = ( 𝐿 ‘ 𝑖 ) ∧ 𝑏 = ( 𝐿 ‘ 𝑗 ) ) ↔ ( ∃ 𝑖 ∈ ℤ 𝑎 = ( 𝐿 ‘ 𝑖 ) ∧ ∃ 𝑗 ∈ ℤ 𝑏 = ( 𝐿 ‘ 𝑗 ) ) )
34 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → 𝐺 ∈ Grp )
35 simprl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → 𝑖 ∈ ℤ )
36 simprr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → 𝑗 ∈ ℤ )
37 1 4 6 iscyggen ⊢ ( 𝑋 ∈ 𝐸 ↔ ( 𝑋 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 ) )
38 37 simplbi ⊢ ( 𝑋 ∈ 𝐸 → 𝑋 ∈ 𝐵 )
39 8 38 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
40 39 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → 𝑋 ∈ 𝐵 )
41 1 4 12 mulgdir ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑖 + 𝑗 ) · 𝑋 ) = ( ( 𝑖 · 𝑋 ) ( +g ‘ 𝐺 ) ( 𝑗 · 𝑋 ) ) )
42 34 35 36 40 41 syl13anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( ( 𝑖 + 𝑗 ) · 𝑋 ) = ( ( 𝑖 · 𝑋 ) ( +g ‘ 𝐺 ) ( 𝑗 · 𝑋 ) ) )
43 18 19 syl ⊢ ( 𝜑 → 𝑌 ∈ CRing )
44 5 zrhrhm ⊢ ( 𝑌 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑌 ) )
45 rhmghm ⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑌 ) → 𝐿 ∈ ( ℤring GrpHom 𝑌 ) )
46 43 20 44 45 4syl ⊢ ( 𝜑 → 𝐿 ∈ ( ℤring GrpHom 𝑌 ) )
47 46 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → 𝐿 ∈ ( ℤring GrpHom 𝑌 ) )
48 zringbas ⊢ ℤ = ( Base ‘ ℤring )
49 zringplusg ⊢ + = ( +g ‘ ℤring )
50 48 49 11 ghmlin ⊢ ( ( 𝐿 ∈ ( ℤring GrpHom 𝑌 ) ∧ 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 𝐿 ‘ ( 𝑖 + 𝑗 ) ) = ( ( 𝐿 ‘ 𝑖 ) ( +g ‘ 𝑌 ) ( 𝐿 ‘ 𝑗 ) ) )
51 47 35 36 50 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( 𝐿 ‘ ( 𝑖 + 𝑗 ) ) = ( ( 𝐿 ‘ 𝑖 ) ( +g ‘ 𝑌 ) ( 𝐿 ‘ 𝑗 ) ) )
52 51 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( 𝐹 ‘ ( 𝐿 ‘ ( 𝑖 + 𝑗 ) ) ) = ( 𝐹 ‘ ( ( 𝐿 ‘ 𝑖 ) ( +g ‘ 𝑌 ) ( 𝐿 ‘ 𝑗 ) ) ) )
53 zaddcl ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 𝑖 + 𝑗 ) ∈ ℤ )
54 1 2 3 4 5 6 7 8 9 cygznlem2 ⊢ ( ( 𝜑 ∧ ( 𝑖 + 𝑗 ) ∈ ℤ ) → ( 𝐹 ‘ ( 𝐿 ‘ ( 𝑖 + 𝑗 ) ) ) = ( ( 𝑖 + 𝑗 ) · 𝑋 ) )
55 53 54 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( 𝐹 ‘ ( 𝐿 ‘ ( 𝑖 + 𝑗 ) ) ) = ( ( 𝑖 + 𝑗 ) · 𝑋 ) )
56 52 55 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( 𝐹 ‘ ( ( 𝐿 ‘ 𝑖 ) ( +g ‘ 𝑌 ) ( 𝐿 ‘ 𝑗 ) ) ) = ( ( 𝑖 + 𝑗 ) · 𝑋 ) )
57 1 2 3 4 5 6 7 8 9 cygznlem2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℤ ) → ( 𝐹 ‘ ( 𝐿 ‘ 𝑖 ) ) = ( 𝑖 · 𝑋 ) )
58 57 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( 𝐹 ‘ ( 𝐿 ‘ 𝑖 ) ) = ( 𝑖 · 𝑋 ) )
59 1 2 3 4 5 6 7 8 9 cygznlem2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) → ( 𝐹 ‘ ( 𝐿 ‘ 𝑗 ) ) = ( 𝑗 · 𝑋 ) )
60 59 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( 𝐹 ‘ ( 𝐿 ‘ 𝑗 ) ) = ( 𝑗 · 𝑋 ) )
61 58 60 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( ( 𝐹 ‘ ( 𝐿 ‘ 𝑖 ) ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ ( 𝐿 ‘ 𝑗 ) ) ) = ( ( 𝑖 · 𝑋 ) ( +g ‘ 𝐺 ) ( 𝑗 · 𝑋 ) ) )
62 42 56 61 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( 𝐹 ‘ ( ( 𝐿 ‘ 𝑖 ) ( +g ‘ 𝑌 ) ( 𝐿 ‘ 𝑗 ) ) ) = ( ( 𝐹 ‘ ( 𝐿 ‘ 𝑖 ) ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ ( 𝐿 ‘ 𝑗 ) ) ) )
63 oveq12 ⊢ ( ( 𝑎 = ( 𝐿 ‘ 𝑖 ) ∧ 𝑏 = ( 𝐿 ‘ 𝑗 ) ) → ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) = ( ( 𝐿 ‘ 𝑖 ) ( +g ‘ 𝑌 ) ( 𝐿 ‘ 𝑗 ) ) )
64 63 fveq2d ⊢ ( ( 𝑎 = ( 𝐿 ‘ 𝑖 ) ∧ 𝑏 = ( 𝐿 ‘ 𝑗 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ) = ( 𝐹 ‘ ( ( 𝐿 ‘ 𝑖 ) ( +g ‘ 𝑌 ) ( 𝐿 ‘ 𝑗 ) ) ) )
65 fveq2 ⊢ ( 𝑎 = ( 𝐿 ‘ 𝑖 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝐿 ‘ 𝑖 ) ) )
66 fveq2 ⊢ ( 𝑏 = ( 𝐿 ‘ 𝑗 ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ ( 𝐿 ‘ 𝑗 ) ) )
67 65 66 oveqan12d ⊢ ( ( 𝑎 = ( 𝐿 ‘ 𝑖 ) ∧ 𝑏 = ( 𝐿 ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ ( 𝐿 ‘ 𝑖 ) ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ ( 𝐿 ‘ 𝑗 ) ) ) )
68 64 67 eqeq12d ⊢ ( ( 𝑎 = ( 𝐿 ‘ 𝑖 ) ∧ 𝑏 = ( 𝐿 ‘ 𝑗 ) ) → ( ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑏 ) ) ↔ ( 𝐹 ‘ ( ( 𝐿 ‘ 𝑖 ) ( +g ‘ 𝑌 ) ( 𝐿 ‘ 𝑗 ) ) ) = ( ( 𝐹 ‘ ( 𝐿 ‘ 𝑖 ) ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ ( 𝐿 ‘ 𝑗 ) ) ) ) )
69 62 68 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( ( 𝑎 = ( 𝐿 ‘ 𝑖 ) ∧ 𝑏 = ( 𝐿 ‘ 𝑗 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑏 ) ) ) )
70 69 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ℤ ∃ 𝑗 ∈ ℤ ( 𝑎 = ( 𝐿 ‘ 𝑖 ) ∧ 𝑏 = ( 𝐿 ‘ 𝑗 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑏 ) ) ) )
71 33 70 biimtrrid ⊢ ( 𝜑 → ( ( ∃ 𝑖 ∈ ℤ 𝑎 = ( 𝐿 ‘ 𝑖 ) ∧ ∃ 𝑗 ∈ ℤ 𝑏 = ( 𝐿 ‘ 𝑗 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑏 ) ) ) )
72 71 imp ⊢ ( ( 𝜑 ∧ ( ∃ 𝑖 ∈ ℤ 𝑎 = ( 𝐿 ‘ 𝑖 ) ∧ ∃ 𝑗 ∈ ℤ 𝑏 = ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑏 ) ) )
73 32 72 syldan ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑏 ) ) )
74 10 1 11 12 22 24 25 73 isghmd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑌 GrpHom 𝐺 ) )
75 58 60 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( ( 𝐹 ‘ ( 𝐿 ‘ 𝑖 ) ) = ( 𝐹 ‘ ( 𝐿 ‘ 𝑗 ) ) ↔ ( 𝑖 · 𝑋 ) = ( 𝑗 · 𝑋 ) ) )
76 1 2 3 4 5 6 7 8 cygznlem1 ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( ( 𝐿 ‘ 𝑖 ) = ( 𝐿 ‘ 𝑗 ) ↔ ( 𝑖 · 𝑋 ) = ( 𝑗 · 𝑋 ) ) )
77 75 76 bitr4d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( ( 𝐹 ‘ ( 𝐿 ‘ 𝑖 ) ) = ( 𝐹 ‘ ( 𝐿 ‘ 𝑗 ) ) ↔ ( 𝐿 ‘ 𝑖 ) = ( 𝐿 ‘ 𝑗 ) ) )
78 77 biimpd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( ( 𝐹 ‘ ( 𝐿 ‘ 𝑖 ) ) = ( 𝐹 ‘ ( 𝐿 ‘ 𝑗 ) ) → ( 𝐿 ‘ 𝑖 ) = ( 𝐿 ‘ 𝑗 ) ) )
79 65 66 eqeqan12d ⊢ ( ( 𝑎 = ( 𝐿 ‘ 𝑖 ) ∧ 𝑏 = ( 𝐿 ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ↔ ( 𝐹 ‘ ( 𝐿 ‘ 𝑖 ) ) = ( 𝐹 ‘ ( 𝐿 ‘ 𝑗 ) ) ) )
80 eqeq12 ⊢ ( ( 𝑎 = ( 𝐿 ‘ 𝑖 ) ∧ 𝑏 = ( 𝐿 ‘ 𝑗 ) ) → ( 𝑎 = 𝑏 ↔ ( 𝐿 ‘ 𝑖 ) = ( 𝐿 ‘ 𝑗 ) ) )
81 79 80 imbi12d ⊢ ( ( 𝑎 = ( 𝐿 ‘ 𝑖 ) ∧ 𝑏 = ( 𝐿 ‘ 𝑗 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ↔ ( ( 𝐹 ‘ ( 𝐿 ‘ 𝑖 ) ) = ( 𝐹 ‘ ( 𝐿 ‘ 𝑗 ) ) → ( 𝐿 ‘ 𝑖 ) = ( 𝐿 ‘ 𝑗 ) ) ) )
82 78 81 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( ( 𝑎 = ( 𝐿 ‘ 𝑖 ) ∧ 𝑏 = ( 𝐿 ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
83 82 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ℤ ∃ 𝑗 ∈ ℤ ( 𝑎 = ( 𝐿 ‘ 𝑖 ) ∧ 𝑏 = ( 𝐿 ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
84 33 83 biimtrrid ⊢ ( 𝜑 → ( ( ∃ 𝑖 ∈ ℤ 𝑎 = ( 𝐿 ‘ 𝑖 ) ∧ ∃ 𝑗 ∈ ℤ 𝑏 = ( 𝐿 ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
85 84 imp ⊢ ( ( 𝜑 ∧ ( ∃ 𝑖 ∈ ℤ 𝑎 = ( 𝐿 ‘ 𝑖 ) ∧ ∃ 𝑗 ∈ ℤ 𝑏 = ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
86 32 85 syldan ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
87 86 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( Base ‘ 𝑌 ) ∀ 𝑏 ∈ ( Base ‘ 𝑌 ) ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
88 dff13 ⊢ ( 𝐹 : ( Base ‘ 𝑌 ) –1-1→ 𝐵 ↔ ( 𝐹 : ( Base ‘ 𝑌 ) ⟶ 𝐵 ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑌 ) ∀ 𝑏 ∈ ( Base ‘ 𝑌 ) ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
89 25 87 88 sylanbrc ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑌 ) –1-1→ 𝐵 )
90 1 4 6 iscyggen2 ⊢ ( 𝐺 ∈ Grp → ( 𝑋 ∈ 𝐸 ↔ ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑧 = ( 𝑛 · 𝑋 ) ) ) )
91 24 90 syl ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐸 ↔ ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑧 = ( 𝑛 · 𝑋 ) ) ) )
92 8 91 mpbid ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑧 = ( 𝑛 · 𝑋 ) ) )
93 92 simprd ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑧 = ( 𝑛 · 𝑋 ) )
94 oveq1 ⊢ ( 𝑛 = 𝑗 → ( 𝑛 · 𝑋 ) = ( 𝑗 · 𝑋 ) )
95 94 eqeq2d ⊢ ( 𝑛 = 𝑗 → ( 𝑧 = ( 𝑛 · 𝑋 ) ↔ 𝑧 = ( 𝑗 · 𝑋 ) ) )
96 95 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ℤ 𝑧 = ( 𝑛 · 𝑋 ) ↔ ∃ 𝑗 ∈ ℤ 𝑧 = ( 𝑗 · 𝑋 ) )
97 27 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝐿 : ℤ –onto→ ( Base ‘ 𝑌 ) )
98 fof ⊢ ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑌 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
99 97 98 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
100 99 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑗 ∈ ℤ ) → ( 𝐿 ‘ 𝑗 ) ∈ ( Base ‘ 𝑌 ) )
101 59 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑗 ∈ ℤ ) → ( 𝐹 ‘ ( 𝐿 ‘ 𝑗 ) ) = ( 𝑗 · 𝑋 ) )
102 101 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑗 ∈ ℤ ) → ( 𝑗 · 𝑋 ) = ( 𝐹 ‘ ( 𝐿 ‘ 𝑗 ) ) )
103 fveq2 ⊢ ( 𝑎 = ( 𝐿 ‘ 𝑗 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝐿 ‘ 𝑗 ) ) )
104 103 rspceeqv ⊢ ( ( ( 𝐿 ‘ 𝑗 ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑗 · 𝑋 ) = ( 𝐹 ‘ ( 𝐿 ‘ 𝑗 ) ) ) → ∃ 𝑎 ∈ ( Base ‘ 𝑌 ) ( 𝑗 · 𝑋 ) = ( 𝐹 ‘ 𝑎 ) )
105 100 102 104 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑗 ∈ ℤ ) → ∃ 𝑎 ∈ ( Base ‘ 𝑌 ) ( 𝑗 · 𝑋 ) = ( 𝐹 ‘ 𝑎 ) )
106 eqeq1 ⊢ ( 𝑧 = ( 𝑗 · 𝑋 ) → ( 𝑧 = ( 𝐹 ‘ 𝑎 ) ↔ ( 𝑗 · 𝑋 ) = ( 𝐹 ‘ 𝑎 ) ) )
107 106 rexbidv ⊢ ( 𝑧 = ( 𝑗 · 𝑋 ) → ( ∃ 𝑎 ∈ ( Base ‘ 𝑌 ) 𝑧 = ( 𝐹 ‘ 𝑎 ) ↔ ∃ 𝑎 ∈ ( Base ‘ 𝑌 ) ( 𝑗 · 𝑋 ) = ( 𝐹 ‘ 𝑎 ) ) )
108 105 107 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑗 ∈ ℤ ) → ( 𝑧 = ( 𝑗 · 𝑋 ) → ∃ 𝑎 ∈ ( Base ‘ 𝑌 ) 𝑧 = ( 𝐹 ‘ 𝑎 ) ) )
109 108 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ∃ 𝑗 ∈ ℤ 𝑧 = ( 𝑗 · 𝑋 ) → ∃ 𝑎 ∈ ( Base ‘ 𝑌 ) 𝑧 = ( 𝐹 ‘ 𝑎 ) ) )
110 96 109 biimtrid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ∃ 𝑛 ∈ ℤ 𝑧 = ( 𝑛 · 𝑋 ) → ∃ 𝑎 ∈ ( Base ‘ 𝑌 ) 𝑧 = ( 𝐹 ‘ 𝑎 ) ) )
111 110 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑧 = ( 𝑛 · 𝑋 ) → ∀ 𝑧 ∈ 𝐵 ∃ 𝑎 ∈ ( Base ‘ 𝑌 ) 𝑧 = ( 𝐹 ‘ 𝑎 ) ) )
112 93 111 mpd ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∃ 𝑎 ∈ ( Base ‘ 𝑌 ) 𝑧 = ( 𝐹 ‘ 𝑎 ) )
113 dffo3 ⊢ ( 𝐹 : ( Base ‘ 𝑌 ) –onto→ 𝐵 ↔ ( 𝐹 : ( Base ‘ 𝑌 ) ⟶ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑎 ∈ ( Base ‘ 𝑌 ) 𝑧 = ( 𝐹 ‘ 𝑎 ) ) )
114 25 112 113 sylanbrc ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑌 ) –onto→ 𝐵 )
115 df-f1o ⊢ ( 𝐹 : ( Base ‘ 𝑌 ) –1-1-onto→ 𝐵 ↔ ( 𝐹 : ( Base ‘ 𝑌 ) –1-1→ 𝐵 ∧ 𝐹 : ( Base ‘ 𝑌 ) –onto→ 𝐵 ) )
116 89 114 115 sylanbrc ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑌 ) –1-1-onto→ 𝐵 )
117 10 1 isgim ⊢ ( 𝐹 ∈ ( 𝑌 GrpIso 𝐺 ) ↔ ( 𝐹 ∈ ( 𝑌 GrpHom 𝐺 ) ∧ 𝐹 : ( Base ‘ 𝑌 ) –1-1-onto→ 𝐵 ) )
118 74 116 117 sylanbrc ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑌 GrpIso 𝐺 ) )
119 brgici ⊢ ( 𝐹 ∈ ( 𝑌 GrpIso 𝐺 ) → 𝑌 ≃𝑔 𝐺 )
120 gicsym ⊢ ( 𝑌 ≃𝑔 𝐺 → 𝐺 ≃𝑔 𝑌 )
121 118 119 120 3syl ⊢ ( 𝜑 → 𝐺 ≃𝑔 𝑌 )