| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. 2
⊢
(Base‘(ℂfld ↾s 𝑋)) = (Base‘(ℂfld
↾s 𝑋)) |
| 2 | | eqid 2737 |
. 2
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 3 | | eqid 2737 |
. 2
⊢
(+g‘(ℂfld ↾s 𝑋)) =
(+g‘(ℂfld ↾s 𝑋)) |
| 4 | | eqid 2737 |
. 2
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 5 | | simp1 1137 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘(ℂfld
↾s 𝑋))
∧ 𝑦 ∈
(Base‘(ℂfld ↾s 𝑋))) → 𝜑) |
| 6 | | simp2 1138 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘(ℂfld
↾s 𝑋))
∧ 𝑦 ∈
(Base‘(ℂfld ↾s 𝑋))) → 𝑥 ∈ (Base‘(ℂfld
↾s 𝑋))) |
| 7 | | efabl.4 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈
(SubGrp‘ℂfld)) |
| 8 | | eqid 2737 |
. . . . . . 7
⊢
(ℂfld ↾s 𝑋) = (ℂfld
↾s 𝑋) |
| 9 | 8 | subgbas 19148 |
. . . . . 6
⊢ (𝑋 ∈
(SubGrp‘ℂfld) → 𝑋 = (Base‘(ℂfld
↾s 𝑋))) |
| 10 | 7, 9 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋 = (Base‘(ℂfld
↾s 𝑋))) |
| 11 | 10 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘(ℂfld
↾s 𝑋))
∧ 𝑦 ∈
(Base‘(ℂfld ↾s 𝑋))) → 𝑋 = (Base‘(ℂfld
↾s 𝑋))) |
| 12 | 6, 11 | eleqtrrd 2844 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘(ℂfld
↾s 𝑋))
∧ 𝑦 ∈
(Base‘(ℂfld ↾s 𝑋))) → 𝑥 ∈ 𝑋) |
| 13 | | simp3 1139 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘(ℂfld
↾s 𝑋))
∧ 𝑦 ∈
(Base‘(ℂfld ↾s 𝑋))) → 𝑦 ∈ (Base‘(ℂfld
↾s 𝑋))) |
| 14 | 13, 11 | eleqtrrd 2844 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘(ℂfld
↾s 𝑋))
∧ 𝑦 ∈
(Base‘(ℂfld ↾s 𝑋))) → 𝑦 ∈ 𝑋) |
| 15 | | efabl.3 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 16 | 15, 7 | jca 511 |
. . . . 5
⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld))) |
| 17 | | efabl.1 |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ (exp‘(𝐴 · 𝑥))) |
| 18 | 17 | efgh 26583 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦))) |
| 19 | 16, 18 | syl3an1 1164 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦))) |
| 20 | | cnfldadd 21370 |
. . . . . . . . 9
⊢ + =
(+g‘ℂfld) |
| 21 | 8, 20 | ressplusg 17334 |
. . . . . . . 8
⊢ (𝑋 ∈
(SubGrp‘ℂfld) → + =
(+g‘(ℂfld ↾s 𝑋))) |
| 22 | 7, 21 | syl 17 |
. . . . . . 7
⊢ (𝜑 → + =
(+g‘(ℂfld ↾s 𝑋))) |
| 23 | 22 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → + =
(+g‘(ℂfld ↾s 𝑋))) |
| 24 | 23 | oveqd 7448 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥 + 𝑦) = (𝑥(+g‘(ℂfld
↾s 𝑋))𝑦)) |
| 25 | 24 | fveq2d 6910 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = (𝐹‘(𝑥(+g‘(ℂfld
↾s 𝑋))𝑦))) |
| 26 | | mptexg 7241 |
. . . . . . . 8
⊢ (𝑋 ∈
(SubGrp‘ℂfld) → (𝑥 ∈ 𝑋 ↦ (exp‘(𝐴 · 𝑥))) ∈ V) |
| 27 | 17, 26 | eqeltrid 2845 |
. . . . . . 7
⊢ (𝑋 ∈
(SubGrp‘ℂfld) → 𝐹 ∈ V) |
| 28 | | rnexg 7924 |
. . . . . . 7
⊢ (𝐹 ∈ V → ran 𝐹 ∈ V) |
| 29 | | efabl.2 |
. . . . . . . 8
⊢ 𝐺 =
((mulGrp‘ℂfld) ↾s ran 𝐹) |
| 30 | | eqid 2737 |
. . . . . . . . 9
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
| 31 | | cnfldmul 21372 |
. . . . . . . . 9
⊢ ·
= (.r‘ℂfld) |
| 32 | 30, 31 | mgpplusg 20141 |
. . . . . . . 8
⊢ ·
= (+g‘(mulGrp‘ℂfld)) |
| 33 | 29, 32 | ressplusg 17334 |
. . . . . . 7
⊢ (ran
𝐹 ∈ V → ·
= (+g‘𝐺)) |
| 34 | 7, 27, 28, 33 | 4syl 19 |
. . . . . 6
⊢ (𝜑 → · =
(+g‘𝐺)) |
| 35 | 34 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → · =
(+g‘𝐺)) |
| 36 | 35 | oveqd 7448 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑥) · (𝐹‘𝑦)) = ((𝐹‘𝑥)(+g‘𝐺)(𝐹‘𝑦))) |
| 37 | 19, 25, 36 | 3eqtr3d 2785 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥(+g‘(ℂfld
↾s 𝑋))𝑦)) = ((𝐹‘𝑥)(+g‘𝐺)(𝐹‘𝑦))) |
| 38 | 5, 12, 14, 37 | syl3anc 1373 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘(ℂfld
↾s 𝑋))
∧ 𝑦 ∈
(Base‘(ℂfld ↾s 𝑋))) → (𝐹‘(𝑥(+g‘(ℂfld
↾s 𝑋))𝑦)) = ((𝐹‘𝑥)(+g‘𝐺)(𝐹‘𝑦))) |
| 39 | | fvex 6919 |
. . . . 5
⊢
(exp‘(𝐴
· 𝑥)) ∈
V |
| 40 | 39, 17 | fnmpti 6711 |
. . . 4
⊢ 𝐹 Fn 𝑋 |
| 41 | | dffn4 6826 |
. . . 4
⊢ (𝐹 Fn 𝑋 ↔ 𝐹:𝑋–onto→ran 𝐹) |
| 42 | 40, 41 | mpbi 230 |
. . 3
⊢ 𝐹:𝑋–onto→ran 𝐹 |
| 43 | | eqidd 2738 |
. . . 4
⊢ (𝜑 → 𝐹 = 𝐹) |
| 44 | | eff 16117 |
. . . . . . . 8
⊢
exp:ℂ⟶ℂ |
| 45 | 44 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) →
exp:ℂ⟶ℂ) |
| 46 | 15 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) |
| 47 | | cnfldbas 21368 |
. . . . . . . . . . 11
⊢ ℂ =
(Base‘ℂfld) |
| 48 | 47 | subgss 19145 |
. . . . . . . . . 10
⊢ (𝑋 ∈
(SubGrp‘ℂfld) → 𝑋 ⊆ ℂ) |
| 49 | 7, 48 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
| 50 | 49 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℂ) |
| 51 | 46, 50 | mulcld 11281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐴 · 𝑥) ∈ ℂ) |
| 52 | 45, 51 | ffvelcdmd 7105 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (exp‘(𝐴 · 𝑥)) ∈ ℂ) |
| 53 | 52 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (exp‘(𝐴 · 𝑥)) ∈ ℂ) |
| 54 | 17 | rnmptss 7143 |
. . . . 5
⊢
(∀𝑥 ∈
𝑋 (exp‘(𝐴 · 𝑥)) ∈ ℂ → ran 𝐹 ⊆
ℂ) |
| 55 | 30, 47 | mgpbas 20142 |
. . . . . 6
⊢ ℂ =
(Base‘(mulGrp‘ℂfld)) |
| 56 | 29, 55 | ressbas2 17283 |
. . . . 5
⊢ (ran
𝐹 ⊆ ℂ →
ran 𝐹 = (Base‘𝐺)) |
| 57 | 53, 54, 56 | 3syl 18 |
. . . 4
⊢ (𝜑 → ran 𝐹 = (Base‘𝐺)) |
| 58 | 43, 10, 57 | foeq123d 6841 |
. . 3
⊢ (𝜑 → (𝐹:𝑋–onto→ran 𝐹 ↔ 𝐹:(Base‘(ℂfld
↾s 𝑋))–onto→(Base‘𝐺))) |
| 59 | 42, 58 | mpbii 233 |
. 2
⊢ (𝜑 → 𝐹:(Base‘(ℂfld
↾s 𝑋))–onto→(Base‘𝐺)) |
| 60 | | cnring 21403 |
. . . 4
⊢
ℂfld ∈ Ring |
| 61 | | ringabl 20278 |
. . . 4
⊢
(ℂfld ∈ Ring → ℂfld ∈
Abel) |
| 62 | 60, 61 | ax-mp 5 |
. . 3
⊢
ℂfld ∈ Abel |
| 63 | 8 | subgabl 19854 |
. . 3
⊢
((ℂfld ∈ Abel ∧ 𝑋 ∈
(SubGrp‘ℂfld)) → (ℂfld
↾s 𝑋)
∈ Abel) |
| 64 | 62, 7, 63 | sylancr 587 |
. 2
⊢ (𝜑 → (ℂfld
↾s 𝑋)
∈ Abel) |
| 65 | 1, 2, 3, 4, 38, 59, 64 | ghmabl 19850 |
1
⊢ (𝜑 → 𝐺 ∈ Abel) |