| Step | Hyp | Ref
| Expression |
| 1 | | hvmulcl 31032 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝐴
·ℎ 𝐵) ∈ ℋ) |
| 2 | | kbfval 31971 |
. . 3
⊢ (((𝐴
·ℎ 𝐵) ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ketbra 𝐶) = (𝑥 ∈ ℋ ↦ ((𝑥 ·ih 𝐶)
·ℎ (𝐴 ·ℎ 𝐵)))) |
| 3 | 1, 2 | stoic3 1776 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴
·ℎ 𝐵) ketbra 𝐶) = (𝑥 ∈ ℋ ↦ ((𝑥 ·ih 𝐶)
·ℎ (𝐴 ·ℎ 𝐵)))) |
| 4 | | simp2 1138 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → 𝐵 ∈
ℋ) |
| 5 | | cjcl 15144 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(∗‘𝐴) ∈
ℂ) |
| 6 | 5 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) →
(∗‘𝐴) ∈
ℂ) |
| 7 | | simp3 1139 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → 𝐶 ∈
ℋ) |
| 8 | | hvmulcl 31032 |
. . . . 5
⊢
(((∗‘𝐴)
∈ ℂ ∧ 𝐶
∈ ℋ) → ((∗‘𝐴) ·ℎ 𝐶) ∈
ℋ) |
| 9 | 6, 7, 8 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) →
((∗‘𝐴)
·ℎ 𝐶) ∈ ℋ) |
| 10 | | kbfval 31971 |
. . . 4
⊢ ((𝐵 ∈ ℋ ∧
((∗‘𝐴)
·ℎ 𝐶) ∈ ℋ) → (𝐵 ketbra ((∗‘𝐴) ·ℎ 𝐶)) = (𝑥 ∈ ℋ ↦ ((𝑥 ·ih
((∗‘𝐴)
·ℎ 𝐶)) ·ℎ 𝐵))) |
| 11 | 4, 9, 10 | syl2anc 584 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐵 ketbra ((∗‘𝐴)
·ℎ 𝐶)) = (𝑥 ∈ ℋ ↦ ((𝑥 ·ih
((∗‘𝐴)
·ℎ 𝐶)) ·ℎ 𝐵))) |
| 12 | | simpr 484 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → 𝑥 ∈
ℋ) |
| 13 | | simpl3 1194 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → 𝐶 ∈
ℋ) |
| 14 | | hicl 31099 |
. . . . . . 7
⊢ ((𝑥 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑥
·ih 𝐶) ∈ ℂ) |
| 15 | 12, 13, 14 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → (𝑥
·ih 𝐶) ∈ ℂ) |
| 16 | | simpl1 1192 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → 𝐴 ∈
ℂ) |
| 17 | | simpl2 1193 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → 𝐵 ∈
ℋ) |
| 18 | | ax-hvmulass 31026 |
. . . . . 6
⊢ (((𝑥
·ih 𝐶) ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (((𝑥
·ih 𝐶) · 𝐴) ·ℎ 𝐵) = ((𝑥 ·ih 𝐶)
·ℎ (𝐴 ·ℎ 𝐵))) |
| 19 | 15, 16, 17, 18 | syl3anc 1373 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → (((𝑥
·ih 𝐶) · 𝐴) ·ℎ 𝐵) = ((𝑥 ·ih 𝐶)
·ℎ (𝐴 ·ℎ 𝐵))) |
| 20 | 15, 16 | mulcomd 11282 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → ((𝑥
·ih 𝐶) · 𝐴) = (𝐴 · (𝑥 ·ih 𝐶))) |
| 21 | | his52 31106 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑥
·ih ((∗‘𝐴) ·ℎ 𝐶)) = (𝐴 · (𝑥 ·ih 𝐶))) |
| 22 | 16, 12, 13, 21 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → (𝑥
·ih ((∗‘𝐴) ·ℎ 𝐶)) = (𝐴 · (𝑥 ·ih 𝐶))) |
| 23 | 20, 22 | eqtr4d 2780 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → ((𝑥
·ih 𝐶) · 𝐴) = (𝑥 ·ih
((∗‘𝐴)
·ℎ 𝐶))) |
| 24 | 23 | oveq1d 7446 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → (((𝑥
·ih 𝐶) · 𝐴) ·ℎ 𝐵) = ((𝑥 ·ih
((∗‘𝐴)
·ℎ 𝐶)) ·ℎ 𝐵)) |
| 25 | 19, 24 | eqtr3d 2779 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → ((𝑥
·ih 𝐶) ·ℎ (𝐴
·ℎ 𝐵)) = ((𝑥 ·ih
((∗‘𝐴)
·ℎ 𝐶)) ·ℎ 𝐵)) |
| 26 | 25 | mpteq2dva 5242 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑥 ∈ ℋ ↦ ((𝑥
·ih 𝐶) ·ℎ (𝐴
·ℎ 𝐵))) = (𝑥 ∈ ℋ ↦ ((𝑥 ·ih
((∗‘𝐴)
·ℎ 𝐶)) ·ℎ 𝐵))) |
| 27 | 11, 26 | eqtr4d 2780 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐵 ketbra ((∗‘𝐴)
·ℎ 𝐶)) = (𝑥 ∈ ℋ ↦ ((𝑥 ·ih 𝐶)
·ℎ (𝐴 ·ℎ 𝐵)))) |
| 28 | 3, 27 | eqtr4d 2780 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴
·ℎ 𝐵) ketbra 𝐶) = (𝐵 ketbra ((∗‘𝐴) ·ℎ 𝐶))) |