| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . 4
⊢
(Base‘𝑌) =
(Base‘𝑌) | 
| 2 |  | cygzn.b | . . . 4
⊢ 𝐵 = (Base‘𝐺) | 
| 3 |  | eqid 2736 | . . . 4
⊢
(+g‘𝑌) = (+g‘𝑌) | 
| 4 |  | eqid 2736 | . . . 4
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 5 |  | cygzn.n | . . . . . 6
⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0) | 
| 6 |  | hashcl 14396 | . . . . . . . 8
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℕ0) | 
| 7 | 6 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ Fin) → (♯‘𝐵) ∈
ℕ0) | 
| 8 |  | 0nn0 12543 | . . . . . . . 8
⊢ 0 ∈
ℕ0 | 
| 9 | 8 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐵 ∈ Fin) → 0 ∈
ℕ0) | 
| 10 | 7, 9 | ifclda 4560 | . . . . . 6
⊢ (𝜑 → if(𝐵 ∈ Fin, (♯‘𝐵), 0) ∈
ℕ0) | 
| 11 | 5, 10 | eqeltrid 2844 | . . . . 5
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 12 |  | cygzn.y | . . . . . 6
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) | 
| 13 | 12 | zncrng 21564 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ 𝑌 ∈
CRing) | 
| 14 |  | crngring 20243 | . . . . 5
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) | 
| 15 |  | ringgrp 20236 | . . . . 5
⊢ (𝑌 ∈ Ring → 𝑌 ∈ Grp) | 
| 16 | 11, 13, 14, 15 | 4syl 19 | . . . 4
⊢ (𝜑 → 𝑌 ∈ Grp) | 
| 17 |  | cygzn.g | . . . . 5
⊢ (𝜑 → 𝐺 ∈ CycGrp) | 
| 18 |  | cyggrp 19909 | . . . . 5
⊢ (𝐺 ∈ CycGrp → 𝐺 ∈ Grp) | 
| 19 | 17, 18 | syl 17 | . . . 4
⊢ (𝜑 → 𝐺 ∈ Grp) | 
| 20 |  | cygzn.m | . . . . 5
⊢  · =
(.g‘𝐺) | 
| 21 |  | cygzn.l | . . . . 5
⊢ 𝐿 = (ℤRHom‘𝑌) | 
| 22 |  | cygzn.e | . . . . 5
⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} | 
| 23 |  | cygzn.x | . . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐸) | 
| 24 |  | cygzn.f | . . . . 5
⊢ 𝐹 = ran (𝑚 ∈ ℤ ↦ 〈(𝐿‘𝑚), (𝑚 · 𝑋)〉) | 
| 25 | 2, 5, 12, 20, 21, 22, 17, 23, 24 | cygznlem2a 21587 | . . . 4
⊢ (𝜑 → 𝐹:(Base‘𝑌)⟶𝐵) | 
| 26 | 12, 1, 21 | znzrhfo 21567 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝐿:ℤ–onto→(Base‘𝑌)) | 
| 27 | 11, 26 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐿:ℤ–onto→(Base‘𝑌)) | 
| 28 |  | foelrn 7126 | . . . . . . 7
⊢ ((𝐿:ℤ–onto→(Base‘𝑌) ∧ 𝑎 ∈ (Base‘𝑌)) → ∃𝑖 ∈ ℤ 𝑎 = (𝐿‘𝑖)) | 
| 29 | 27, 28 | sylan 580 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → ∃𝑖 ∈ ℤ 𝑎 = (𝐿‘𝑖)) | 
| 30 |  | foelrn 7126 | . . . . . . 7
⊢ ((𝐿:ℤ–onto→(Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌)) → ∃𝑗 ∈ ℤ 𝑏 = (𝐿‘𝑗)) | 
| 31 | 27, 30 | sylan 580 | . . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (Base‘𝑌)) → ∃𝑗 ∈ ℤ 𝑏 = (𝐿‘𝑗)) | 
| 32 | 29, 31 | anim12dan 619 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌))) → (∃𝑖 ∈ ℤ 𝑎 = (𝐿‘𝑖) ∧ ∃𝑗 ∈ ℤ 𝑏 = (𝐿‘𝑗))) | 
| 33 |  | reeanv 3228 | . . . . . . 7
⊢
(∃𝑖 ∈
ℤ ∃𝑗 ∈
ℤ (𝑎 = (𝐿‘𝑖) ∧ 𝑏 = (𝐿‘𝑗)) ↔ (∃𝑖 ∈ ℤ 𝑎 = (𝐿‘𝑖) ∧ ∃𝑗 ∈ ℤ 𝑏 = (𝐿‘𝑗))) | 
| 34 | 19 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → 𝐺 ∈ Grp) | 
| 35 |  | simprl 770 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → 𝑖 ∈ ℤ) | 
| 36 |  | simprr 772 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → 𝑗 ∈ ℤ) | 
| 37 | 2, 20, 22 | iscyggen 19899 | . . . . . . . . . . . . . 14
⊢ (𝑋 ∈ 𝐸 ↔ (𝑋 ∈ 𝐵 ∧ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) = 𝐵)) | 
| 38 | 37 | simplbi 497 | . . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝐸 → 𝑋 ∈ 𝐵) | 
| 39 | 23, 38 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ 𝐵) | 
| 40 | 39 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → 𝑋 ∈ 𝐵) | 
| 41 | 2, 20, 4 | mulgdir 19125 | . . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑖 + 𝑗) · 𝑋) = ((𝑖 · 𝑋)(+g‘𝐺)(𝑗 · 𝑋))) | 
| 42 | 34, 35, 36, 40, 41 | syl13anc 1373 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → ((𝑖 + 𝑗) · 𝑋) = ((𝑖 · 𝑋)(+g‘𝐺)(𝑗 · 𝑋))) | 
| 43 | 11, 13 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌 ∈ CRing) | 
| 44 | 21 | zrhrhm 21523 | . . . . . . . . . . . . . . 15
⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑌)) | 
| 45 |  | rhmghm 20485 | . . . . . . . . . . . . . . 15
⊢ (𝐿 ∈ (ℤring
RingHom 𝑌) → 𝐿 ∈ (ℤring
GrpHom 𝑌)) | 
| 46 | 43, 14, 44, 45 | 4syl 19 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ∈ (ℤring GrpHom 𝑌)) | 
| 47 | 46 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → 𝐿 ∈ (ℤring GrpHom 𝑌)) | 
| 48 |  | zringbas 21465 | . . . . . . . . . . . . . 14
⊢ ℤ =
(Base‘ℤring) | 
| 49 |  | zringplusg 21466 | . . . . . . . . . . . . . 14
⊢  + =
(+g‘ℤring) | 
| 50 | 48, 49, 3 | ghmlin 19240 | . . . . . . . . . . . . 13
⊢ ((𝐿 ∈ (ℤring
GrpHom 𝑌) ∧ 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝐿‘(𝑖 + 𝑗)) = ((𝐿‘𝑖)(+g‘𝑌)(𝐿‘𝑗))) | 
| 51 | 47, 35, 36, 50 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → (𝐿‘(𝑖 + 𝑗)) = ((𝐿‘𝑖)(+g‘𝑌)(𝐿‘𝑗))) | 
| 52 | 51 | fveq2d 6909 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → (𝐹‘(𝐿‘(𝑖 + 𝑗))) = (𝐹‘((𝐿‘𝑖)(+g‘𝑌)(𝐿‘𝑗)))) | 
| 53 |  | zaddcl 12659 | . . . . . . . . . . . 12
⊢ ((𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑖 + 𝑗) ∈ ℤ) | 
| 54 | 2, 5, 12, 20, 21, 22, 17, 23, 24 | cygznlem2 21588 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 + 𝑗) ∈ ℤ) → (𝐹‘(𝐿‘(𝑖 + 𝑗))) = ((𝑖 + 𝑗) · 𝑋)) | 
| 55 | 53, 54 | sylan2 593 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → (𝐹‘(𝐿‘(𝑖 + 𝑗))) = ((𝑖 + 𝑗) · 𝑋)) | 
| 56 | 52, 55 | eqtr3d 2778 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → (𝐹‘((𝐿‘𝑖)(+g‘𝑌)(𝐿‘𝑗))) = ((𝑖 + 𝑗) · 𝑋)) | 
| 57 | 2, 5, 12, 20, 21, 22, 17, 23, 24 | cygznlem2 21588 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ℤ) → (𝐹‘(𝐿‘𝑖)) = (𝑖 · 𝑋)) | 
| 58 | 57 | adantrr 717 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → (𝐹‘(𝐿‘𝑖)) = (𝑖 · 𝑋)) | 
| 59 | 2, 5, 12, 20, 21, 22, 17, 23, 24 | cygznlem2 21588 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℤ) → (𝐹‘(𝐿‘𝑗)) = (𝑗 · 𝑋)) | 
| 60 | 59 | adantrl 716 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → (𝐹‘(𝐿‘𝑗)) = (𝑗 · 𝑋)) | 
| 61 | 58, 60 | oveq12d 7450 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → ((𝐹‘(𝐿‘𝑖))(+g‘𝐺)(𝐹‘(𝐿‘𝑗))) = ((𝑖 · 𝑋)(+g‘𝐺)(𝑗 · 𝑋))) | 
| 62 | 42, 56, 61 | 3eqtr4d 2786 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → (𝐹‘((𝐿‘𝑖)(+g‘𝑌)(𝐿‘𝑗))) = ((𝐹‘(𝐿‘𝑖))(+g‘𝐺)(𝐹‘(𝐿‘𝑗)))) | 
| 63 |  | oveq12 7441 | . . . . . . . . . . 11
⊢ ((𝑎 = (𝐿‘𝑖) ∧ 𝑏 = (𝐿‘𝑗)) → (𝑎(+g‘𝑌)𝑏) = ((𝐿‘𝑖)(+g‘𝑌)(𝐿‘𝑗))) | 
| 64 | 63 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝑎 = (𝐿‘𝑖) ∧ 𝑏 = (𝐿‘𝑗)) → (𝐹‘(𝑎(+g‘𝑌)𝑏)) = (𝐹‘((𝐿‘𝑖)(+g‘𝑌)(𝐿‘𝑗)))) | 
| 65 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑎 = (𝐿‘𝑖) → (𝐹‘𝑎) = (𝐹‘(𝐿‘𝑖))) | 
| 66 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑏 = (𝐿‘𝑗) → (𝐹‘𝑏) = (𝐹‘(𝐿‘𝑗))) | 
| 67 | 65, 66 | oveqan12d 7451 | . . . . . . . . . 10
⊢ ((𝑎 = (𝐿‘𝑖) ∧ 𝑏 = (𝐿‘𝑗)) → ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏)) = ((𝐹‘(𝐿‘𝑖))(+g‘𝐺)(𝐹‘(𝐿‘𝑗)))) | 
| 68 | 64, 67 | eqeq12d 2752 | . . . . . . . . 9
⊢ ((𝑎 = (𝐿‘𝑖) ∧ 𝑏 = (𝐿‘𝑗)) → ((𝐹‘(𝑎(+g‘𝑌)𝑏)) = ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏)) ↔ (𝐹‘((𝐿‘𝑖)(+g‘𝑌)(𝐿‘𝑗))) = ((𝐹‘(𝐿‘𝑖))(+g‘𝐺)(𝐹‘(𝐿‘𝑗))))) | 
| 69 | 62, 68 | syl5ibrcom 247 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → ((𝑎 = (𝐿‘𝑖) ∧ 𝑏 = (𝐿‘𝑗)) → (𝐹‘(𝑎(+g‘𝑌)𝑏)) = ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏)))) | 
| 70 | 69 | rexlimdvva 3212 | . . . . . . 7
⊢ (𝜑 → (∃𝑖 ∈ ℤ ∃𝑗 ∈ ℤ (𝑎 = (𝐿‘𝑖) ∧ 𝑏 = (𝐿‘𝑗)) → (𝐹‘(𝑎(+g‘𝑌)𝑏)) = ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏)))) | 
| 71 | 33, 70 | biimtrrid 243 | . . . . . 6
⊢ (𝜑 → ((∃𝑖 ∈ ℤ 𝑎 = (𝐿‘𝑖) ∧ ∃𝑗 ∈ ℤ 𝑏 = (𝐿‘𝑗)) → (𝐹‘(𝑎(+g‘𝑌)𝑏)) = ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏)))) | 
| 72 | 71 | imp 406 | . . . . 5
⊢ ((𝜑 ∧ (∃𝑖 ∈ ℤ 𝑎 = (𝐿‘𝑖) ∧ ∃𝑗 ∈ ℤ 𝑏 = (𝐿‘𝑗))) → (𝐹‘(𝑎(+g‘𝑌)𝑏)) = ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏))) | 
| 73 | 32, 72 | syldan 591 | . . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌))) → (𝐹‘(𝑎(+g‘𝑌)𝑏)) = ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏))) | 
| 74 | 1, 2, 3, 4, 16, 19, 25, 73 | isghmd 19244 | . . 3
⊢ (𝜑 → 𝐹 ∈ (𝑌 GrpHom 𝐺)) | 
| 75 | 58, 60 | eqeq12d 2752 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → ((𝐹‘(𝐿‘𝑖)) = (𝐹‘(𝐿‘𝑗)) ↔ (𝑖 · 𝑋) = (𝑗 · 𝑋))) | 
| 76 | 2, 5, 12, 20, 21, 22, 17, 23 | cygznlem1 21586 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → ((𝐿‘𝑖) = (𝐿‘𝑗) ↔ (𝑖 · 𝑋) = (𝑗 · 𝑋))) | 
| 77 | 75, 76 | bitr4d 282 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → ((𝐹‘(𝐿‘𝑖)) = (𝐹‘(𝐿‘𝑗)) ↔ (𝐿‘𝑖) = (𝐿‘𝑗))) | 
| 78 | 77 | biimpd 229 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → ((𝐹‘(𝐿‘𝑖)) = (𝐹‘(𝐿‘𝑗)) → (𝐿‘𝑖) = (𝐿‘𝑗))) | 
| 79 | 65, 66 | eqeqan12d 2750 | . . . . . . . . . . . 12
⊢ ((𝑎 = (𝐿‘𝑖) ∧ 𝑏 = (𝐿‘𝑗)) → ((𝐹‘𝑎) = (𝐹‘𝑏) ↔ (𝐹‘(𝐿‘𝑖)) = (𝐹‘(𝐿‘𝑗)))) | 
| 80 |  | eqeq12 2753 | . . . . . . . . . . . 12
⊢ ((𝑎 = (𝐿‘𝑖) ∧ 𝑏 = (𝐿‘𝑗)) → (𝑎 = 𝑏 ↔ (𝐿‘𝑖) = (𝐿‘𝑗))) | 
| 81 | 79, 80 | imbi12d 344 | . . . . . . . . . . 11
⊢ ((𝑎 = (𝐿‘𝑖) ∧ 𝑏 = (𝐿‘𝑗)) → (((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏) ↔ ((𝐹‘(𝐿‘𝑖)) = (𝐹‘(𝐿‘𝑗)) → (𝐿‘𝑖) = (𝐿‘𝑗)))) | 
| 82 | 78, 81 | syl5ibrcom 247 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → ((𝑎 = (𝐿‘𝑖) ∧ 𝑏 = (𝐿‘𝑗)) → ((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏))) | 
| 83 | 82 | rexlimdvva 3212 | . . . . . . . . 9
⊢ (𝜑 → (∃𝑖 ∈ ℤ ∃𝑗 ∈ ℤ (𝑎 = (𝐿‘𝑖) ∧ 𝑏 = (𝐿‘𝑗)) → ((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏))) | 
| 84 | 33, 83 | biimtrrid 243 | . . . . . . . 8
⊢ (𝜑 → ((∃𝑖 ∈ ℤ 𝑎 = (𝐿‘𝑖) ∧ ∃𝑗 ∈ ℤ 𝑏 = (𝐿‘𝑗)) → ((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏))) | 
| 85 | 84 | imp 406 | . . . . . . 7
⊢ ((𝜑 ∧ (∃𝑖 ∈ ℤ 𝑎 = (𝐿‘𝑖) ∧ ∃𝑗 ∈ ℤ 𝑏 = (𝐿‘𝑗))) → ((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏)) | 
| 86 | 32, 85 | syldan 591 | . . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌))) → ((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏)) | 
| 87 | 86 | ralrimivva 3201 | . . . . 5
⊢ (𝜑 → ∀𝑎 ∈ (Base‘𝑌)∀𝑏 ∈ (Base‘𝑌)((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏)) | 
| 88 |  | dff13 7276 | . . . . 5
⊢ (𝐹:(Base‘𝑌)–1-1→𝐵 ↔ (𝐹:(Base‘𝑌)⟶𝐵 ∧ ∀𝑎 ∈ (Base‘𝑌)∀𝑏 ∈ (Base‘𝑌)((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏))) | 
| 89 | 25, 87, 88 | sylanbrc 583 | . . . 4
⊢ (𝜑 → 𝐹:(Base‘𝑌)–1-1→𝐵) | 
| 90 | 2, 20, 22 | iscyggen2 19900 | . . . . . . . . 9
⊢ (𝐺 ∈ Grp → (𝑋 ∈ 𝐸 ↔ (𝑋 ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ∃𝑛 ∈ ℤ 𝑧 = (𝑛 · 𝑋)))) | 
| 91 | 19, 90 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (𝑋 ∈ 𝐸 ↔ (𝑋 ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ∃𝑛 ∈ ℤ 𝑧 = (𝑛 · 𝑋)))) | 
| 92 | 23, 91 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ∃𝑛 ∈ ℤ 𝑧 = (𝑛 · 𝑋))) | 
| 93 | 92 | simprd 495 | . . . . . 6
⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∃𝑛 ∈ ℤ 𝑧 = (𝑛 · 𝑋)) | 
| 94 |  | oveq1 7439 | . . . . . . . . . 10
⊢ (𝑛 = 𝑗 → (𝑛 · 𝑋) = (𝑗 · 𝑋)) | 
| 95 | 94 | eqeq2d 2747 | . . . . . . . . 9
⊢ (𝑛 = 𝑗 → (𝑧 = (𝑛 · 𝑋) ↔ 𝑧 = (𝑗 · 𝑋))) | 
| 96 | 95 | cbvrexvw 3237 | . . . . . . . 8
⊢
(∃𝑛 ∈
ℤ 𝑧 = (𝑛 · 𝑋) ↔ ∃𝑗 ∈ ℤ 𝑧 = (𝑗 · 𝑋)) | 
| 97 | 27 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐿:ℤ–onto→(Base‘𝑌)) | 
| 98 |  | fof 6819 | . . . . . . . . . . . . 13
⊢ (𝐿:ℤ–onto→(Base‘𝑌) → 𝐿:ℤ⟶(Base‘𝑌)) | 
| 99 | 97, 98 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐿:ℤ⟶(Base‘𝑌)) | 
| 100 | 99 | ffvelcdmda 7103 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑗 ∈ ℤ) → (𝐿‘𝑗) ∈ (Base‘𝑌)) | 
| 101 | 59 | adantlr 715 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑗 ∈ ℤ) → (𝐹‘(𝐿‘𝑗)) = (𝑗 · 𝑋)) | 
| 102 | 101 | eqcomd 2742 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑗 ∈ ℤ) → (𝑗 · 𝑋) = (𝐹‘(𝐿‘𝑗))) | 
| 103 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑎 = (𝐿‘𝑗) → (𝐹‘𝑎) = (𝐹‘(𝐿‘𝑗))) | 
| 104 | 103 | rspceeqv 3644 | . . . . . . . . . . 11
⊢ (((𝐿‘𝑗) ∈ (Base‘𝑌) ∧ (𝑗 · 𝑋) = (𝐹‘(𝐿‘𝑗))) → ∃𝑎 ∈ (Base‘𝑌)(𝑗 · 𝑋) = (𝐹‘𝑎)) | 
| 105 | 100, 102,
104 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑗 ∈ ℤ) → ∃𝑎 ∈ (Base‘𝑌)(𝑗 · 𝑋) = (𝐹‘𝑎)) | 
| 106 |  | eqeq1 2740 | . . . . . . . . . . 11
⊢ (𝑧 = (𝑗 · 𝑋) → (𝑧 = (𝐹‘𝑎) ↔ (𝑗 · 𝑋) = (𝐹‘𝑎))) | 
| 107 | 106 | rexbidv 3178 | . . . . . . . . . 10
⊢ (𝑧 = (𝑗 · 𝑋) → (∃𝑎 ∈ (Base‘𝑌)𝑧 = (𝐹‘𝑎) ↔ ∃𝑎 ∈ (Base‘𝑌)(𝑗 · 𝑋) = (𝐹‘𝑎))) | 
| 108 | 105, 107 | syl5ibrcom 247 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑗 ∈ ℤ) → (𝑧 = (𝑗 · 𝑋) → ∃𝑎 ∈ (Base‘𝑌)𝑧 = (𝐹‘𝑎))) | 
| 109 | 108 | rexlimdva 3154 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (∃𝑗 ∈ ℤ 𝑧 = (𝑗 · 𝑋) → ∃𝑎 ∈ (Base‘𝑌)𝑧 = (𝐹‘𝑎))) | 
| 110 | 96, 109 | biimtrid 242 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (∃𝑛 ∈ ℤ 𝑧 = (𝑛 · 𝑋) → ∃𝑎 ∈ (Base‘𝑌)𝑧 = (𝐹‘𝑎))) | 
| 111 | 110 | ralimdva 3166 | . . . . . 6
⊢ (𝜑 → (∀𝑧 ∈ 𝐵 ∃𝑛 ∈ ℤ 𝑧 = (𝑛 · 𝑋) → ∀𝑧 ∈ 𝐵 ∃𝑎 ∈ (Base‘𝑌)𝑧 = (𝐹‘𝑎))) | 
| 112 | 93, 111 | mpd 15 | . . . . 5
⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∃𝑎 ∈ (Base‘𝑌)𝑧 = (𝐹‘𝑎)) | 
| 113 |  | dffo3 7121 | . . . . 5
⊢ (𝐹:(Base‘𝑌)–onto→𝐵 ↔ (𝐹:(Base‘𝑌)⟶𝐵 ∧ ∀𝑧 ∈ 𝐵 ∃𝑎 ∈ (Base‘𝑌)𝑧 = (𝐹‘𝑎))) | 
| 114 | 25, 112, 113 | sylanbrc 583 | . . . 4
⊢ (𝜑 → 𝐹:(Base‘𝑌)–onto→𝐵) | 
| 115 |  | df-f1o 6567 | . . . 4
⊢ (𝐹:(Base‘𝑌)–1-1-onto→𝐵 ↔ (𝐹:(Base‘𝑌)–1-1→𝐵 ∧ 𝐹:(Base‘𝑌)–onto→𝐵)) | 
| 116 | 89, 114, 115 | sylanbrc 583 | . . 3
⊢ (𝜑 → 𝐹:(Base‘𝑌)–1-1-onto→𝐵) | 
| 117 | 1, 2 | isgim 19281 | . . 3
⊢ (𝐹 ∈ (𝑌 GrpIso 𝐺) ↔ (𝐹 ∈ (𝑌 GrpHom 𝐺) ∧ 𝐹:(Base‘𝑌)–1-1-onto→𝐵)) | 
| 118 | 74, 116, 117 | sylanbrc 583 | . 2
⊢ (𝜑 → 𝐹 ∈ (𝑌 GrpIso 𝐺)) | 
| 119 |  | brgici 19290 | . 2
⊢ (𝐹 ∈ (𝑌 GrpIso 𝐺) → 𝑌 ≃𝑔 𝐺) | 
| 120 |  | gicsym 19294 | . 2
⊢ (𝑌 ≃𝑔
𝐺 → 𝐺 ≃𝑔 𝑌) | 
| 121 | 118, 119,
120 | 3syl 18 | 1
⊢ (𝜑 → 𝐺 ≃𝑔 𝑌) |