| Step |
Hyp |
Ref |
Expression |
| 1 |
|
kbass5 |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) = ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ) |
| 2 |
|
kbval |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) = ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ) |
| 3 |
2
|
3expa |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) = ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ) |
| 4 |
3
|
adantrr |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) = ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ) |
| 5 |
4
|
oveq1d |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) = ( ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ketbra 𝐷 ) ) |
| 6 |
|
hicl |
⊢ ( ( 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐶 ·ih 𝐵 ) ∈ ℂ ) |
| 7 |
|
kbmul |
⊢ ( ( ( 𝐶 ·ih 𝐵 ) ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ketbra 𝐷 ) = ( 𝐴 ketbra ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) ) ) |
| 8 |
6 7
|
syl3an1 |
⊢ ( ( ( 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝐴 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ketbra 𝐷 ) = ( 𝐴 ketbra ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) ) ) |
| 9 |
8
|
3exp |
⊢ ( ( 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ∈ ℋ → ( 𝐷 ∈ ℋ → ( ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ketbra 𝐷 ) = ( 𝐴 ketbra ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) ) ) ) ) |
| 10 |
9
|
ex |
⊢ ( 𝐶 ∈ ℋ → ( 𝐵 ∈ ℋ → ( 𝐴 ∈ ℋ → ( 𝐷 ∈ ℋ → ( ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ketbra 𝐷 ) = ( 𝐴 ketbra ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) ) ) ) ) ) |
| 11 |
10
|
com13 |
⊢ ( 𝐴 ∈ ℋ → ( 𝐵 ∈ ℋ → ( 𝐶 ∈ ℋ → ( 𝐷 ∈ ℋ → ( ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ketbra 𝐷 ) = ( 𝐴 ketbra ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) ) ) ) ) ) |
| 12 |
11
|
imp43 |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ketbra 𝐷 ) = ( 𝐴 ketbra ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) ) ) |
| 13 |
|
bracl |
⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ∈ ℂ ) |
| 14 |
|
bracnln |
⊢ ( 𝐷 ∈ ℋ → ( bra ‘ 𝐷 ) ∈ ( LinFn ∩ ContFn ) ) |
| 15 |
|
cnvbramul |
⊢ ( ( ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ∈ ℂ ∧ ( bra ‘ 𝐷 ) ∈ ( LinFn ∩ ContFn ) ) → ( ◡ bra ‘ ( ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ·fn ( bra ‘ 𝐷 ) ) ) = ( ( ∗ ‘ ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ) ·ℎ ( ◡ bra ‘ ( bra ‘ 𝐷 ) ) ) ) |
| 16 |
13 14 15
|
syl2an |
⊢ ( ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝐷 ∈ ℋ ) → ( ◡ bra ‘ ( ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ·fn ( bra ‘ 𝐷 ) ) ) = ( ( ∗ ‘ ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ) ·ℎ ( ◡ bra ‘ ( bra ‘ 𝐷 ) ) ) ) |
| 17 |
|
braval |
⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) = ( 𝐶 ·ih 𝐵 ) ) |
| 18 |
17
|
fveq2d |
⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ∗ ‘ ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ) = ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ) |
| 19 |
|
cnvbrabra |
⊢ ( 𝐷 ∈ ℋ → ( ◡ bra ‘ ( bra ‘ 𝐷 ) ) = 𝐷 ) |
| 20 |
18 19
|
oveqan12d |
⊢ ( ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝐷 ∈ ℋ ) → ( ( ∗ ‘ ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ) ·ℎ ( ◡ bra ‘ ( bra ‘ 𝐷 ) ) ) = ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) ) |
| 21 |
16 20
|
eqtr2d |
⊢ ( ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝐷 ∈ ℋ ) → ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) = ( ◡ bra ‘ ( ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ·fn ( bra ‘ 𝐷 ) ) ) ) |
| 22 |
21
|
anasss |
⊢ ( ( 𝐵 ∈ ℋ ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) = ( ◡ bra ‘ ( ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ·fn ( bra ‘ 𝐷 ) ) ) ) |
| 23 |
|
kbass2 |
⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ·fn ( bra ‘ 𝐷 ) ) = ( ( bra ‘ 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ) |
| 24 |
23
|
3expb |
⊢ ( ( 𝐵 ∈ ℋ ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ·fn ( bra ‘ 𝐷 ) ) = ( ( bra ‘ 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ) |
| 25 |
24
|
fveq2d |
⊢ ( ( 𝐵 ∈ ℋ ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ◡ bra ‘ ( ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ·fn ( bra ‘ 𝐷 ) ) ) = ( ◡ bra ‘ ( ( bra ‘ 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ) ) |
| 26 |
22 25
|
eqtr2d |
⊢ ( ( 𝐵 ∈ ℋ ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ◡ bra ‘ ( ( bra ‘ 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ) = ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) ) |
| 27 |
26
|
adantll |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ◡ bra ‘ ( ( bra ‘ 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ) = ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) ) |
| 28 |
27
|
oveq2d |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( 𝐴 ketbra ( ◡ bra ‘ ( ( bra ‘ 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ) ) = ( 𝐴 ketbra ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) ) ) |
| 29 |
12 28
|
eqtr4d |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ketbra 𝐷 ) = ( 𝐴 ketbra ( ◡ bra ‘ ( ( bra ‘ 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ) ) ) |
| 30 |
1 5 29
|
3eqtrd |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) = ( 𝐴 ketbra ( ◡ bra ‘ ( ( bra ‘ 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ) ) ) |