Step | Hyp | Ref
| Expression |
1 | | recn 10819 |
. . 3
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
2 | | hmopf 29955 |
. . 3
⊢ (𝑇 ∈ HrmOp → 𝑇: ℋ⟶
ℋ) |
3 | | homulcl 29840 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ (𝐴
·op 𝑇): ℋ⟶ ℋ) |
4 | 1, 2, 3 | syl2an 599 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp) → (𝐴 ·op
𝑇): ℋ⟶
ℋ) |
5 | | cjre 14702 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(∗‘𝐴) = 𝐴) |
6 | | hmop 30003 |
. . . . . . 7
⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥
·ih (𝑇‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦)) |
7 | 6 | 3expb 1122 |
. . . . . 6
⊢ ((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥
·ih (𝑇‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦)) |
8 | 5, 7 | oveqan12d 7232 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ))) →
((∗‘𝐴)
· (𝑥
·ih (𝑇‘𝑦))) = (𝐴 · ((𝑇‘𝑥) ·ih 𝑦))) |
9 | 8 | anassrs 471 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) →
((∗‘𝐴)
· (𝑥
·ih (𝑇‘𝑦))) = (𝐴 · ((𝑇‘𝑥) ·ih 𝑦))) |
10 | 1, 2 | anim12i 616 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp) → (𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶
ℋ)) |
11 | | homval 29822 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) →
((𝐴
·op 𝑇)‘𝑦) = (𝐴 ·ℎ (𝑇‘𝑦))) |
12 | 11 | 3expa 1120 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑦 ∈ ℋ) →
((𝐴
·op 𝑇)‘𝑦) = (𝐴 ·ℎ (𝑇‘𝑦))) |
13 | 12 | adantrl 716 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
((𝐴
·op 𝑇)‘𝑦) = (𝐴 ·ℎ (𝑇‘𝑦))) |
14 | 13 | oveq2d 7229 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
(𝑥
·ih ((𝐴 ·op 𝑇)‘𝑦)) = (𝑥 ·ih (𝐴
·ℎ (𝑇‘𝑦)))) |
15 | | simpll 767 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
𝐴 ∈
ℂ) |
16 | | simprl 771 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
𝑥 ∈
ℋ) |
17 | | ffvelrn 6902 |
. . . . . . . 8
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) →
(𝑇‘𝑦) ∈ ℋ) |
18 | 17 | ad2ant2l 746 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
(𝑇‘𝑦) ∈ ℋ) |
19 | | his5 29167 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ∧ (𝑇‘𝑦) ∈ ℋ) → (𝑥 ·ih (𝐴
·ℎ (𝑇‘𝑦))) = ((∗‘𝐴) · (𝑥 ·ih (𝑇‘𝑦)))) |
20 | 15, 16, 18, 19 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
(𝑥
·ih (𝐴 ·ℎ (𝑇‘𝑦))) = ((∗‘𝐴) · (𝑥 ·ih (𝑇‘𝑦)))) |
21 | 14, 20 | eqtrd 2777 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
(𝑥
·ih ((𝐴 ·op 𝑇)‘𝑦)) = ((∗‘𝐴) · (𝑥 ·ih (𝑇‘𝑦)))) |
22 | 10, 21 | sylan 583 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥
·ih ((𝐴 ·op 𝑇)‘𝑦)) = ((∗‘𝐴) · (𝑥 ·ih (𝑇‘𝑦)))) |
23 | | homval 29822 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
((𝐴
·op 𝑇)‘𝑥) = (𝐴 ·ℎ (𝑇‘𝑥))) |
24 | 23 | 3expa 1120 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
((𝐴
·op 𝑇)‘𝑥) = (𝐴 ·ℎ (𝑇‘𝑥))) |
25 | 24 | adantrr 717 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
((𝐴
·op 𝑇)‘𝑥) = (𝐴 ·ℎ (𝑇‘𝑥))) |
26 | 25 | oveq1d 7228 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
(((𝐴
·op 𝑇)‘𝑥) ·ih 𝑦) = ((𝐴 ·ℎ (𝑇‘𝑥)) ·ih 𝑦)) |
27 | | ffvelrn 6902 |
. . . . . . . 8
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(𝑇‘𝑥) ∈ ℋ) |
28 | 27 | ad2ant2lr 748 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
(𝑇‘𝑥) ∈ ℋ) |
29 | | simprr 773 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
𝑦 ∈
ℋ) |
30 | | ax-his3 29165 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ (𝑇‘𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝐴 ·ℎ (𝑇‘𝑥)) ·ih 𝑦) = (𝐴 · ((𝑇‘𝑥) ·ih 𝑦))) |
31 | 15, 28, 29, 30 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
((𝐴
·ℎ (𝑇‘𝑥)) ·ih 𝑦) = (𝐴 · ((𝑇‘𝑥) ·ih 𝑦))) |
32 | 26, 31 | eqtrd 2777 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
(((𝐴
·op 𝑇)‘𝑥) ·ih 𝑦) = (𝐴 · ((𝑇‘𝑥) ·ih 𝑦))) |
33 | 10, 32 | sylan 583 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) →
(((𝐴
·op 𝑇)‘𝑥) ·ih 𝑦) = (𝐴 · ((𝑇‘𝑥) ·ih 𝑦))) |
34 | 9, 22, 33 | 3eqtr4d 2787 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥
·ih ((𝐴 ·op 𝑇)‘𝑦)) = (((𝐴 ·op 𝑇)‘𝑥) ·ih 𝑦)) |
35 | 34 | ralrimivva 3112 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp) →
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih ((𝐴 ·op 𝑇)‘𝑦)) = (((𝐴 ·op 𝑇)‘𝑥) ·ih 𝑦)) |
36 | | elhmop 29954 |
. 2
⊢ ((𝐴 ·op
𝑇) ∈ HrmOp ↔
((𝐴
·op 𝑇): ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih ((𝐴 ·op 𝑇)‘𝑦)) = (((𝐴 ·op 𝑇)‘𝑥) ·ih 𝑦))) |
37 | 4, 35, 36 | sylanbrc 586 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp) → (𝐴 ·op
𝑇) ∈
HrmOp) |