Step |
Hyp |
Ref |
Expression |
1 |
|
lnopl.1 |
⊢ 𝑇 ∈ LinOp |
2 |
|
hvmulcl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·ℎ 𝐶 ) ∈ ℋ ) |
3 |
1
|
lnopsubi |
⊢ ( ( 𝐵 ∈ ℋ ∧ ( 𝐴 ·ℎ 𝐶 ) ∈ ℋ ) → ( 𝑇 ‘ ( 𝐵 −ℎ ( 𝐴 ·ℎ 𝐶 ) ) ) = ( ( 𝑇 ‘ 𝐵 ) −ℎ ( 𝑇 ‘ ( 𝐴 ·ℎ 𝐶 ) ) ) ) |
4 |
2 3
|
sylan2 |
⊢ ( ( 𝐵 ∈ ℋ ∧ ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ) ) → ( 𝑇 ‘ ( 𝐵 −ℎ ( 𝐴 ·ℎ 𝐶 ) ) ) = ( ( 𝑇 ‘ 𝐵 ) −ℎ ( 𝑇 ‘ ( 𝐴 ·ℎ 𝐶 ) ) ) ) |
5 |
4
|
3impb |
⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐵 −ℎ ( 𝐴 ·ℎ 𝐶 ) ) ) = ( ( 𝑇 ‘ 𝐵 ) −ℎ ( 𝑇 ‘ ( 𝐴 ·ℎ 𝐶 ) ) ) ) |
6 |
5
|
3com12 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐵 −ℎ ( 𝐴 ·ℎ 𝐶 ) ) ) = ( ( 𝑇 ‘ 𝐵 ) −ℎ ( 𝑇 ‘ ( 𝐴 ·ℎ 𝐶 ) ) ) ) |
7 |
1
|
lnopmuli |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 ·ℎ 𝐶 ) ) = ( 𝐴 ·ℎ ( 𝑇 ‘ 𝐶 ) ) ) |
8 |
7
|
oveq2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐵 ) −ℎ ( 𝑇 ‘ ( 𝐴 ·ℎ 𝐶 ) ) ) = ( ( 𝑇 ‘ 𝐵 ) −ℎ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝐶 ) ) ) ) |
9 |
8
|
3adant2 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐵 ) −ℎ ( 𝑇 ‘ ( 𝐴 ·ℎ 𝐶 ) ) ) = ( ( 𝑇 ‘ 𝐵 ) −ℎ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝐶 ) ) ) ) |
10 |
6 9
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐵 −ℎ ( 𝐴 ·ℎ 𝐶 ) ) ) = ( ( 𝑇 ‘ 𝐵 ) −ℎ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝐶 ) ) ) ) |