Step | Hyp | Ref
| Expression |
1 | | eff 14812 |
. . . . . 6
⊢
exp:ℂ⟶ℂ |
2 | 1 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) →
exp:ℂ⟶ℂ) |
3 | | efabl.3 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) |
4 | 3 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) |
5 | | efabl.4 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈
(SubGrp‘ℂfld)) |
6 | | cnfldbas 19750 |
. . . . . . . . 9
⊢ ℂ =
(Base‘ℂfld) |
7 | 6 | subgss 17595 |
. . . . . . . 8
⊢ (𝑋 ∈
(SubGrp‘ℂfld) → 𝑋 ⊆ ℂ) |
8 | 5, 7 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
9 | 8 | sselda 3603 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℂ) |
10 | 4, 9 | mulcld 10060 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐴 · 𝑥) ∈ ℂ) |
11 | 2, 10 | ffvelrnd 6360 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (exp‘(𝐴 · 𝑥)) ∈ ℂ) |
12 | 11 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (exp‘(𝐴 · 𝑥)) ∈ ℂ) |
13 | | efabl.1 |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ (exp‘(𝐴 · 𝑥))) |
14 | 13 | rnmptss 6392 |
. . 3
⊢
(∀𝑥 ∈
𝑋 (exp‘(𝐴 · 𝑥)) ∈ ℂ → ran 𝐹 ⊆
ℂ) |
15 | 12, 14 | syl 17 |
. 2
⊢ (𝜑 → ran 𝐹 ⊆ ℂ) |
16 | 3 | mul01d 10235 |
. . . . 5
⊢ (𝜑 → (𝐴 · 0) = 0) |
17 | 16 | fveq2d 6195 |
. . . 4
⊢ (𝜑 → (exp‘(𝐴 · 0)) =
(exp‘0)) |
18 | | ef0 14821 |
. . . 4
⊢
(exp‘0) = 1 |
19 | 17, 18 | syl6eq 2672 |
. . 3
⊢ (𝜑 → (exp‘(𝐴 · 0)) =
1) |
20 | | cnfld0 19770 |
. . . . . 6
⊢ 0 =
(0g‘ℂfld) |
21 | 20 | subg0cl 17602 |
. . . . 5
⊢ (𝑋 ∈
(SubGrp‘ℂfld) → 0 ∈ 𝑋) |
22 | 5, 21 | syl 17 |
. . . 4
⊢ (𝜑 → 0 ∈ 𝑋) |
23 | | fvex 6201 |
. . . 4
⊢
(exp‘(𝐴
· 0)) ∈ V |
24 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = 0 → (𝐴 · 𝑥) = (𝐴 · 0)) |
25 | 24 | fveq2d 6195 |
. . . . 5
⊢ (𝑥 = 0 → (exp‘(𝐴 · 𝑥)) = (exp‘(𝐴 · 0))) |
26 | 13, 25 | elrnmpt1s 5373 |
. . . 4
⊢ ((0
∈ 𝑋 ∧
(exp‘(𝐴 · 0))
∈ V) → (exp‘(𝐴 · 0)) ∈ ran 𝐹) |
27 | 22, 23, 26 | sylancl 694 |
. . 3
⊢ (𝜑 → (exp‘(𝐴 · 0)) ∈ ran 𝐹) |
28 | 19, 27 | eqeltrrd 2702 |
. 2
⊢ (𝜑 → 1 ∈ ran 𝐹) |
29 | | efabl.2 |
. . . . . . . . 9
⊢ 𝐺 =
((mulGrp‘ℂfld) ↾s ran 𝐹) |
30 | 13, 29, 3, 5 | efabl 24296 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Abel) |
31 | | ablgrp 18198 |
. . . . . . . 8
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
32 | 30, 31 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ Grp) |
33 | 32 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → 𝐺 ∈ Grp) |
34 | | simp2 1062 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → 𝑥 ∈ ran 𝐹) |
35 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
36 | 35, 6 | mgpbas 18495 |
. . . . . . . . . 10
⊢ ℂ =
(Base‘(mulGrp‘ℂfld)) |
37 | 29, 36 | ressbas2 15931 |
. . . . . . . . 9
⊢ (ran
𝐹 ⊆ ℂ →
ran 𝐹 = (Base‘𝐺)) |
38 | 15, 37 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐹 = (Base‘𝐺)) |
39 | 38 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → ran 𝐹 = (Base‘𝐺)) |
40 | 34, 39 | eleqtrd 2703 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → 𝑥 ∈ (Base‘𝐺)) |
41 | | simp3 1063 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ran 𝐹) |
42 | 41, 39 | eleqtrd 2703 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ (Base‘𝐺)) |
43 | | eqid 2622 |
. . . . . . 7
⊢
(Base‘𝐺) =
(Base‘𝐺) |
44 | | eqid 2622 |
. . . . . . 7
⊢
(+g‘𝐺) = (+g‘𝐺) |
45 | 43, 44 | grpcl 17430 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
46 | 33, 40, 42, 45 | syl3anc 1326 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
47 | | mptexg 6484 |
. . . . . . . . . 10
⊢ (𝑋 ∈
(SubGrp‘ℂfld) → (𝑥 ∈ 𝑋 ↦ (exp‘(𝐴 · 𝑥))) ∈ V) |
48 | 5, 47 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (exp‘(𝐴 · 𝑥))) ∈ V) |
49 | 13, 48 | syl5eqel 2705 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ V) |
50 | | rnexg 7098 |
. . . . . . . 8
⊢ (𝐹 ∈ V → ran 𝐹 ∈ V) |
51 | | cnfldmul 19752 |
. . . . . . . . . 10
⊢ ·
= (.r‘ℂfld) |
52 | 35, 51 | mgpplusg 18493 |
. . . . . . . . 9
⊢ ·
= (+g‘(mulGrp‘ℂfld)) |
53 | 29, 52 | ressplusg 15993 |
. . . . . . . 8
⊢ (ran
𝐹 ∈ V → ·
= (+g‘𝐺)) |
54 | 49, 50, 53 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → · =
(+g‘𝐺)) |
55 | 54 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → · =
(+g‘𝐺)) |
56 | 55 | oveqd 6667 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → (𝑥 · 𝑦) = (𝑥(+g‘𝐺)𝑦)) |
57 | 46, 56, 39 | 3eltr4d 2716 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → (𝑥 · 𝑦) ∈ ran 𝐹) |
58 | 57 | 3expb 1266 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) → (𝑥 · 𝑦) ∈ ran 𝐹) |
59 | 58 | ralrimivva 2971 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 · 𝑦) ∈ ran 𝐹) |
60 | | cnring 19768 |
. . 3
⊢
ℂfld ∈ Ring |
61 | 35 | ringmgp 18553 |
. . 3
⊢
(ℂfld ∈ Ring →
(mulGrp‘ℂfld) ∈ Mnd) |
62 | | cnfld1 19771 |
. . . . 5
⊢ 1 =
(1r‘ℂfld) |
63 | 35, 62 | ringidval 18503 |
. . . 4
⊢ 1 =
(0g‘(mulGrp‘ℂfld)) |
64 | 36, 63, 52 | issubm 17347 |
. . 3
⊢
((mulGrp‘ℂfld) ∈ Mnd → (ran 𝐹 ∈
(SubMnd‘(mulGrp‘ℂfld)) ↔ (ran 𝐹 ⊆ ℂ ∧ 1 ∈
ran 𝐹 ∧ ∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 · 𝑦) ∈ ran 𝐹))) |
65 | 60, 61, 64 | mp2b 10 |
. 2
⊢ (ran
𝐹 ∈
(SubMnd‘(mulGrp‘ℂfld)) ↔ (ran 𝐹 ⊆ ℂ ∧ 1 ∈
ran 𝐹 ∧ ∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 · 𝑦) ∈ ran 𝐹)) |
66 | 15, 28, 59, 65 | syl3anbrc 1246 |
1
⊢ (𝜑 → ran 𝐹 ∈
(SubMnd‘(mulGrp‘ℂfld))) |