| Step | Hyp | Ref
| Expression |
| 1 | | eff 16117 |
. . . . . 6
⊢
exp:ℂ⟶ℂ |
| 2 | 1 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) →
exp:ℂ⟶ℂ) |
| 3 | | efabl.3 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) |
| 5 | | efabl.4 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈
(SubGrp‘ℂfld)) |
| 6 | | cnfldbas 21368 |
. . . . . . . . 9
⊢ ℂ =
(Base‘ℂfld) |
| 7 | 6 | subgss 19145 |
. . . . . . . 8
⊢ (𝑋 ∈
(SubGrp‘ℂfld) → 𝑋 ⊆ ℂ) |
| 8 | 5, 7 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
| 9 | 8 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℂ) |
| 10 | 4, 9 | mulcld 11281 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐴 · 𝑥) ∈ ℂ) |
| 11 | 2, 10 | ffvelcdmd 7105 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (exp‘(𝐴 · 𝑥)) ∈ ℂ) |
| 12 | 11 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (exp‘(𝐴 · 𝑥)) ∈ ℂ) |
| 13 | | efabl.1 |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ (exp‘(𝐴 · 𝑥))) |
| 14 | 13 | rnmptss 7143 |
. . 3
⊢
(∀𝑥 ∈
𝑋 (exp‘(𝐴 · 𝑥)) ∈ ℂ → ran 𝐹 ⊆
ℂ) |
| 15 | 12, 14 | syl 17 |
. 2
⊢ (𝜑 → ran 𝐹 ⊆ ℂ) |
| 16 | 3 | mul01d 11460 |
. . . . 5
⊢ (𝜑 → (𝐴 · 0) = 0) |
| 17 | 16 | fveq2d 6910 |
. . . 4
⊢ (𝜑 → (exp‘(𝐴 · 0)) =
(exp‘0)) |
| 18 | | ef0 16127 |
. . . 4
⊢
(exp‘0) = 1 |
| 19 | 17, 18 | eqtrdi 2793 |
. . 3
⊢ (𝜑 → (exp‘(𝐴 · 0)) =
1) |
| 20 | | cnfld0 21405 |
. . . . . 6
⊢ 0 =
(0g‘ℂfld) |
| 21 | 20 | subg0cl 19152 |
. . . . 5
⊢ (𝑋 ∈
(SubGrp‘ℂfld) → 0 ∈ 𝑋) |
| 22 | 5, 21 | syl 17 |
. . . 4
⊢ (𝜑 → 0 ∈ 𝑋) |
| 23 | | fvex 6919 |
. . . 4
⊢
(exp‘(𝐴
· 0)) ∈ V |
| 24 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = 0 → (𝐴 · 𝑥) = (𝐴 · 0)) |
| 25 | 24 | fveq2d 6910 |
. . . . 5
⊢ (𝑥 = 0 → (exp‘(𝐴 · 𝑥)) = (exp‘(𝐴 · 0))) |
| 26 | 13, 25 | elrnmpt1s 5970 |
. . . 4
⊢ ((0
∈ 𝑋 ∧
(exp‘(𝐴 · 0))
∈ V) → (exp‘(𝐴 · 0)) ∈ ran 𝐹) |
| 27 | 22, 23, 26 | sylancl 586 |
. . 3
⊢ (𝜑 → (exp‘(𝐴 · 0)) ∈ ran 𝐹) |
| 28 | 19, 27 | eqeltrrd 2842 |
. 2
⊢ (𝜑 → 1 ∈ ran 𝐹) |
| 29 | | efabl.2 |
. . . . . . . . 9
⊢ 𝐺 =
((mulGrp‘ℂfld) ↾s ran 𝐹) |
| 30 | 13, 29, 3, 5 | efabl 26592 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Abel) |
| 31 | | ablgrp 19803 |
. . . . . . . 8
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
| 32 | 30, 31 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ Grp) |
| 33 | 32 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → 𝐺 ∈ Grp) |
| 34 | | simp2 1138 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → 𝑥 ∈ ran 𝐹) |
| 35 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
| 36 | 35, 6 | mgpbas 20142 |
. . . . . . . . . 10
⊢ ℂ =
(Base‘(mulGrp‘ℂfld)) |
| 37 | 29, 36 | ressbas2 17283 |
. . . . . . . . 9
⊢ (ran
𝐹 ⊆ ℂ →
ran 𝐹 = (Base‘𝐺)) |
| 38 | 15, 37 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐹 = (Base‘𝐺)) |
| 39 | 38 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → ran 𝐹 = (Base‘𝐺)) |
| 40 | 34, 39 | eleqtrd 2843 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → 𝑥 ∈ (Base‘𝐺)) |
| 41 | | simp3 1139 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ran 𝐹) |
| 42 | 41, 39 | eleqtrd 2843 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ (Base‘𝐺)) |
| 43 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 44 | | eqid 2737 |
. . . . . . 7
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 45 | 43, 44 | grpcl 18959 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
| 46 | 33, 40, 42, 45 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
| 47 | 5 | mptexd 7244 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (exp‘(𝐴 · 𝑥))) ∈ V) |
| 48 | 13, 47 | eqeltrid 2845 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ V) |
| 49 | | rnexg 7924 |
. . . . . . . 8
⊢ (𝐹 ∈ V → ran 𝐹 ∈ V) |
| 50 | | cnfldmul 21372 |
. . . . . . . . . 10
⊢ ·
= (.r‘ℂfld) |
| 51 | 35, 50 | mgpplusg 20141 |
. . . . . . . . 9
⊢ ·
= (+g‘(mulGrp‘ℂfld)) |
| 52 | 29, 51 | ressplusg 17334 |
. . . . . . . 8
⊢ (ran
𝐹 ∈ V → ·
= (+g‘𝐺)) |
| 53 | 48, 49, 52 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → · =
(+g‘𝐺)) |
| 54 | 53 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → · =
(+g‘𝐺)) |
| 55 | 54 | oveqd 7448 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → (𝑥 · 𝑦) = (𝑥(+g‘𝐺)𝑦)) |
| 56 | 46, 55, 39 | 3eltr4d 2856 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → (𝑥 · 𝑦) ∈ ran 𝐹) |
| 57 | 56 | 3expb 1121 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) → (𝑥 · 𝑦) ∈ ran 𝐹) |
| 58 | 57 | ralrimivva 3202 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 · 𝑦) ∈ ran 𝐹) |
| 59 | | cnring 21403 |
. . 3
⊢
ℂfld ∈ Ring |
| 60 | 35 | ringmgp 20236 |
. . 3
⊢
(ℂfld ∈ Ring →
(mulGrp‘ℂfld) ∈ Mnd) |
| 61 | | cnfld1 21406 |
. . . . 5
⊢ 1 =
(1r‘ℂfld) |
| 62 | 35, 61 | ringidval 20180 |
. . . 4
⊢ 1 =
(0g‘(mulGrp‘ℂfld)) |
| 63 | 36, 62, 51 | issubm 18816 |
. . 3
⊢
((mulGrp‘ℂfld) ∈ Mnd → (ran 𝐹 ∈
(SubMnd‘(mulGrp‘ℂfld)) ↔ (ran 𝐹 ⊆ ℂ ∧ 1 ∈
ran 𝐹 ∧ ∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 · 𝑦) ∈ ran 𝐹))) |
| 64 | 59, 60, 63 | mp2b 10 |
. 2
⊢ (ran
𝐹 ∈
(SubMnd‘(mulGrp‘ℂfld)) ↔ (ran 𝐹 ⊆ ℂ ∧ 1 ∈
ran 𝐹 ∧ ∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 · 𝑦) ∈ ran 𝐹)) |
| 65 | 15, 28, 58, 64 | syl3anbrc 1344 |
1
⊢ (𝜑 → ran 𝐹 ∈
(SubMnd‘(mulGrp‘ℂfld))) |