| Step | Hyp | Ref
| Expression |
| 1 | | dmadjop 31907 |
. . 3
⊢ (𝑇 ∈ dom
adjℎ → 𝑇: ℋ⟶ ℋ) |
| 2 | | homulcl 31778 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ (𝐴
·op 𝑇): ℋ⟶ ℋ) |
| 3 | 1, 2 | sylan2 593 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ) → (𝐴 ·op 𝑇): ℋ⟶
ℋ) |
| 4 | | cjcl 15144 |
. . 3
⊢ (𝐴 ∈ ℂ →
(∗‘𝐴) ∈
ℂ) |
| 5 | | dmadjrn 31914 |
. . . 4
⊢ (𝑇 ∈ dom
adjℎ → (adjℎ‘𝑇) ∈ dom
adjℎ) |
| 6 | | dmadjop 31907 |
. . . 4
⊢
((adjℎ‘𝑇) ∈ dom adjℎ →
(adjℎ‘𝑇): ℋ⟶ ℋ) |
| 7 | 5, 6 | syl 17 |
. . 3
⊢ (𝑇 ∈ dom
adjℎ → (adjℎ‘𝑇): ℋ⟶ ℋ) |
| 8 | | homulcl 31778 |
. . 3
⊢
(((∗‘𝐴)
∈ ℂ ∧ (adjℎ‘𝑇): ℋ⟶ ℋ) →
((∗‘𝐴)
·op (adjℎ‘𝑇)): ℋ⟶
ℋ) |
| 9 | 4, 7, 8 | syl2an 596 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ) → ((∗‘𝐴) ·op
(adjℎ‘𝑇)): ℋ⟶
ℋ) |
| 10 | | adj2 31953 |
. . . . . . . 8
⊢ ((𝑇 ∈ dom
adjℎ ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih
((adjℎ‘𝑇)‘𝑦))) |
| 11 | 10 | 3expb 1121 |
. . . . . . 7
⊢ ((𝑇 ∈ dom
adjℎ ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih
((adjℎ‘𝑇)‘𝑦))) |
| 12 | 11 | adantll 714 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih
((adjℎ‘𝑇)‘𝑦))) |
| 13 | 12 | oveq2d 7447 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝐴 · ((𝑇‘𝑥) ·ih 𝑦)) = (𝐴 · (𝑥 ·ih
((adjℎ‘𝑇)‘𝑦)))) |
| 14 | 1 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ ((𝑇 ∈ dom
adjℎ ∧ 𝑥 ∈ ℋ) → (𝑇‘𝑥) ∈ ℋ) |
| 15 | | ax-his3 31103 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ (𝑇‘𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝐴 ·ℎ (𝑇‘𝑥)) ·ih 𝑦) = (𝐴 · ((𝑇‘𝑥) ·ih 𝑦))) |
| 16 | 14, 15 | syl3an2 1165 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (𝑇 ∈ dom
adjℎ ∧ 𝑥 ∈ ℋ) ∧ 𝑦 ∈ ℋ) → ((𝐴 ·ℎ (𝑇‘𝑥)) ·ih 𝑦) = (𝐴 · ((𝑇‘𝑥) ·ih 𝑦))) |
| 17 | 16 | 3exp 1120 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → ((𝑇 ∈ dom
adjℎ ∧ 𝑥 ∈ ℋ) → (𝑦 ∈ ℋ → ((𝐴 ·ℎ (𝑇‘𝑥)) ·ih 𝑦) = (𝐴 · ((𝑇‘𝑥) ·ih 𝑦))))) |
| 18 | 17 | expd 415 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝑇 ∈ dom
adjℎ → (𝑥 ∈ ℋ → (𝑦 ∈ ℋ → ((𝐴 ·ℎ (𝑇‘𝑥)) ·ih 𝑦) = (𝐴 · ((𝑇‘𝑥) ·ih 𝑦)))))) |
| 19 | 18 | imp43 427 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝐴 ·ℎ (𝑇‘𝑥)) ·ih 𝑦) = (𝐴 · ((𝑇‘𝑥) ·ih 𝑦))) |
| 20 | | simpll 767 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝐴 ∈ ℂ) |
| 21 | | simprl 771 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑥 ∈ ℋ) |
| 22 | | adjcl 31951 |
. . . . . . 7
⊢ ((𝑇 ∈ dom
adjℎ ∧ 𝑦 ∈ ℋ) →
((adjℎ‘𝑇)‘𝑦) ∈ ℋ) |
| 23 | 22 | ad2ant2l 746 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) →
((adjℎ‘𝑇)‘𝑦) ∈ ℋ) |
| 24 | | his52 31106 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ∧
((adjℎ‘𝑇)‘𝑦) ∈ ℋ) → (𝑥 ·ih
((∗‘𝐴)
·ℎ ((adjℎ‘𝑇)‘𝑦))) = (𝐴 · (𝑥 ·ih
((adjℎ‘𝑇)‘𝑦)))) |
| 25 | 20, 21, 23, 24 | syl3anc 1373 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·ih
((∗‘𝐴)
·ℎ ((adjℎ‘𝑇)‘𝑦))) = (𝐴 · (𝑥 ·ih
((adjℎ‘𝑇)‘𝑦)))) |
| 26 | 13, 19, 25 | 3eqtr4d 2787 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝐴 ·ℎ (𝑇‘𝑥)) ·ih 𝑦) = (𝑥 ·ih
((∗‘𝐴)
·ℎ ((adjℎ‘𝑇)‘𝑦)))) |
| 27 | | homval 31760 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
((𝐴
·op 𝑇)‘𝑥) = (𝐴 ·ℎ (𝑇‘𝑥))) |
| 28 | 1, 27 | syl3an2 1165 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ ∧ 𝑥 ∈ ℋ) → ((𝐴 ·op 𝑇)‘𝑥) = (𝐴 ·ℎ (𝑇‘𝑥))) |
| 29 | 28 | 3expa 1119 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ) ∧ 𝑥 ∈ ℋ) → ((𝐴 ·op 𝑇)‘𝑥) = (𝐴 ·ℎ (𝑇‘𝑥))) |
| 30 | 29 | adantrr 717 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝐴 ·op 𝑇)‘𝑥) = (𝐴 ·ℎ (𝑇‘𝑥))) |
| 31 | 30 | oveq1d 7446 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝐴 ·op 𝑇)‘𝑥) ·ih 𝑦) = ((𝐴 ·ℎ (𝑇‘𝑥)) ·ih 𝑦)) |
| 32 | | id 22 |
. . . . . . . 8
⊢ (𝑦 ∈ ℋ → 𝑦 ∈
ℋ) |
| 33 | | homval 31760 |
. . . . . . . 8
⊢
(((∗‘𝐴)
∈ ℂ ∧ (adjℎ‘𝑇): ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) →
(((∗‘𝐴)
·op (adjℎ‘𝑇))‘𝑦) = ((∗‘𝐴) ·ℎ
((adjℎ‘𝑇)‘𝑦))) |
| 34 | 4, 7, 32, 33 | syl3an 1161 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ ∧ 𝑦 ∈ ℋ) →
(((∗‘𝐴)
·op (adjℎ‘𝑇))‘𝑦) = ((∗‘𝐴) ·ℎ
((adjℎ‘𝑇)‘𝑦))) |
| 35 | 34 | 3expa 1119 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ) ∧ 𝑦 ∈ ℋ) →
(((∗‘𝐴)
·op (adjℎ‘𝑇))‘𝑦) = ((∗‘𝐴) ·ℎ
((adjℎ‘𝑇)‘𝑦))) |
| 36 | 35 | adantrl 716 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) →
(((∗‘𝐴)
·op (adjℎ‘𝑇))‘𝑦) = ((∗‘𝐴) ·ℎ
((adjℎ‘𝑇)‘𝑦))) |
| 37 | 36 | oveq2d 7447 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·ih
(((∗‘𝐴)
·op (adjℎ‘𝑇))‘𝑦)) = (𝑥 ·ih
((∗‘𝐴)
·ℎ ((adjℎ‘𝑇)‘𝑦)))) |
| 38 | 26, 31, 37 | 3eqtr4d 2787 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝐴 ·op 𝑇)‘𝑥) ·ih 𝑦) = (𝑥 ·ih
(((∗‘𝐴)
·op (adjℎ‘𝑇))‘𝑦))) |
| 39 | 38 | ralrimivva 3202 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ) → ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (((𝐴 ·op 𝑇)‘𝑥) ·ih 𝑦) = (𝑥 ·ih
(((∗‘𝐴)
·op (adjℎ‘𝑇))‘𝑦))) |
| 40 | | adjeq 31954 |
. 2
⊢ (((𝐴 ·op
𝑇): ℋ⟶ ℋ
∧ ((∗‘𝐴)
·op (adjℎ‘𝑇)): ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(((𝐴
·op 𝑇)‘𝑥) ·ih 𝑦) = (𝑥 ·ih
(((∗‘𝐴)
·op (adjℎ‘𝑇))‘𝑦))) →
(adjℎ‘(𝐴 ·op 𝑇)) = ((∗‘𝐴) ·op
(adjℎ‘𝑇))) |
| 41 | 3, 9, 39, 40 | syl3anc 1373 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom
adjℎ) → (adjℎ‘(𝐴 ·op 𝑇)) = ((∗‘𝐴) ·op
(adjℎ‘𝑇))) |