Step | Hyp | Ref
| Expression |
1 | | simp1l 1078 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → 𝐴 ∈ ℂ) |
2 | | simp1r 1079 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → 𝑋 ∈
(SubGrp‘ℂfld)) |
3 | | cnfldbas 19571 |
. . . . . . . 8
⊢ ℂ =
(Base‘ℂfld) |
4 | 3 | subgss 17418 |
. . . . . . 7
⊢ (𝑋 ∈
(SubGrp‘ℂfld) → 𝑋 ⊆ ℂ) |
5 | 2, 4 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → 𝑋 ⊆ ℂ) |
6 | | simp2 1055 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → 𝐵 ∈ 𝑋) |
7 | 5, 6 | sseldd 3569 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → 𝐵 ∈ ℂ) |
8 | | simp3 1056 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ 𝑋) |
9 | 5, 8 | sseldd 3569 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ ℂ) |
10 | 1, 7, 9 | adddid 9943 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
11 | 10 | fveq2d 6107 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (exp‘(𝐴 · (𝐵 + 𝐶))) = (exp‘((𝐴 · 𝐵) + (𝐴 · 𝐶)))) |
12 | 1, 7 | mulcld 9939 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴 · 𝐵) ∈ ℂ) |
13 | 1, 9 | mulcld 9939 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴 · 𝐶) ∈ ℂ) |
14 | | efadd 14663 |
. . . 4
⊢ (((𝐴 · 𝐵) ∈ ℂ ∧ (𝐴 · 𝐶) ∈ ℂ) → (exp‘((𝐴 · 𝐵) + (𝐴 · 𝐶))) = ((exp‘(𝐴 · 𝐵)) · (exp‘(𝐴 · 𝐶)))) |
15 | 12, 13, 14 | syl2anc 691 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (exp‘((𝐴 · 𝐵) + (𝐴 · 𝐶))) = ((exp‘(𝐴 · 𝐵)) · (exp‘(𝐴 · 𝐶)))) |
16 | 11, 15 | eqtrd 2644 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (exp‘(𝐴 · (𝐵 + 𝐶))) = ((exp‘(𝐴 · 𝐵)) · (exp‘(𝐴 · 𝐶)))) |
17 | | efgh.1 |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ (exp‘(𝐴 · 𝑥))) |
18 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐴 · 𝑥) = (𝐴 · 𝑦)) |
19 | 18 | fveq2d 6107 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (exp‘(𝐴 · 𝑥)) = (exp‘(𝐴 · 𝑦))) |
20 | 19 | cbvmptv 4678 |
. . . . 5
⊢ (𝑥 ∈ 𝑋 ↦ (exp‘(𝐴 · 𝑥))) = (𝑦 ∈ 𝑋 ↦ (exp‘(𝐴 · 𝑦))) |
21 | 17, 20 | eqtri 2632 |
. . . 4
⊢ 𝐹 = (𝑦 ∈ 𝑋 ↦ (exp‘(𝐴 · 𝑦))) |
22 | 21 | a1i 11 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → 𝐹 = (𝑦 ∈ 𝑋 ↦ (exp‘(𝐴 · 𝑦)))) |
23 | | oveq2 6557 |
. . . . 5
⊢ (𝑦 = (𝐵 + 𝐶) → (𝐴 · 𝑦) = (𝐴 · (𝐵 + 𝐶))) |
24 | 23 | fveq2d 6107 |
. . . 4
⊢ (𝑦 = (𝐵 + 𝐶) → (exp‘(𝐴 · 𝑦)) = (exp‘(𝐴 · (𝐵 + 𝐶)))) |
25 | 24 | adantl 481 |
. . 3
⊢ ((((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) ∧ 𝑦 = (𝐵 + 𝐶)) → (exp‘(𝐴 · 𝑦)) = (exp‘(𝐴 · (𝐵 + 𝐶)))) |
26 | | cnfldadd 19572 |
. . . . 5
⊢ + =
(+g‘ℂfld) |
27 | 26 | subgcl 17427 |
. . . 4
⊢ ((𝑋 ∈
(SubGrp‘ℂfld) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐵 + 𝐶) ∈ 𝑋) |
28 | 27 | 3adant1l 1310 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐵 + 𝐶) ∈ 𝑋) |
29 | | fvex 6113 |
. . . 4
⊢
(exp‘(𝐴
· (𝐵 + 𝐶))) ∈ V |
30 | 29 | a1i 11 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (exp‘(𝐴 · (𝐵 + 𝐶))) ∈ V) |
31 | 22, 25, 28, 30 | fvmptd 6197 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐹‘(𝐵 + 𝐶)) = (exp‘(𝐴 · (𝐵 + 𝐶)))) |
32 | | oveq2 6557 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝐴 · 𝑦) = (𝐴 · 𝐵)) |
33 | 32 | fveq2d 6107 |
. . . . 5
⊢ (𝑦 = 𝐵 → (exp‘(𝐴 · 𝑦)) = (exp‘(𝐴 · 𝐵))) |
34 | 33 | adantl 481 |
. . . 4
⊢ ((((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) ∧ 𝑦 = 𝐵) → (exp‘(𝐴 · 𝑦)) = (exp‘(𝐴 · 𝐵))) |
35 | | fvex 6113 |
. . . . 5
⊢
(exp‘(𝐴
· 𝐵)) ∈
V |
36 | 35 | a1i 11 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (exp‘(𝐴 · 𝐵)) ∈ V) |
37 | 22, 34, 6, 36 | fvmptd 6197 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐹‘𝐵) = (exp‘(𝐴 · 𝐵))) |
38 | | oveq2 6557 |
. . . . . 6
⊢ (𝑦 = 𝐶 → (𝐴 · 𝑦) = (𝐴 · 𝐶)) |
39 | 38 | fveq2d 6107 |
. . . . 5
⊢ (𝑦 = 𝐶 → (exp‘(𝐴 · 𝑦)) = (exp‘(𝐴 · 𝐶))) |
40 | 39 | adantl 481 |
. . . 4
⊢ ((((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) ∧ 𝑦 = 𝐶) → (exp‘(𝐴 · 𝑦)) = (exp‘(𝐴 · 𝐶))) |
41 | | fvex 6113 |
. . . . 5
⊢
(exp‘(𝐴
· 𝐶)) ∈
V |
42 | 41 | a1i 11 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (exp‘(𝐴 · 𝐶)) ∈ V) |
43 | 22, 40, 8, 42 | fvmptd 6197 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐹‘𝐶) = (exp‘(𝐴 · 𝐶))) |
44 | 37, 43 | oveq12d 6567 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐹‘𝐵) · (𝐹‘𝐶)) = ((exp‘(𝐴 · 𝐵)) · (exp‘(𝐴 · 𝐶)))) |
45 | 16, 31, 44 | 3eqtr4d 2654 |
1
⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈
(SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐹‘(𝐵 + 𝐶)) = ((𝐹‘𝐵) · (𝐹‘𝐶))) |