Step |
Hyp |
Ref |
Expression |
1 |
|
kbval |
⊢ ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝐶 ketbra 𝐷 ) ‘ 𝑥 ) = ( ( 𝑥 ·ih 𝐷 ) ·ℎ 𝐶 ) ) |
2 |
1
|
3expa |
⊢ ( ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐶 ketbra 𝐷 ) ‘ 𝑥 ) = ( ( 𝑥 ·ih 𝐷 ) ·ℎ 𝐶 ) ) |
3 |
2
|
adantll |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐶 ketbra 𝐷 ) ‘ 𝑥 ) = ( ( 𝑥 ·ih 𝐷 ) ·ℎ 𝐶 ) ) |
4 |
3
|
fveq2d |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ ( ( 𝐶 ketbra 𝐷 ) ‘ 𝑥 ) ) = ( ( 𝐴 ketbra 𝐵 ) ‘ ( ( 𝑥 ·ih 𝐷 ) ·ℎ 𝐶 ) ) ) |
5 |
|
simplll |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → 𝐴 ∈ ℋ ) |
6 |
|
simpllr |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → 𝐵 ∈ ℋ ) |
7 |
|
simpr |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → 𝑥 ∈ ℋ ) |
8 |
|
simplrr |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → 𝐷 ∈ ℋ ) |
9 |
|
hicl |
⊢ ( ( 𝑥 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( 𝑥 ·ih 𝐷 ) ∈ ℂ ) |
10 |
7 8 9
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( 𝑥 ·ih 𝐷 ) ∈ ℂ ) |
11 |
|
simplrl |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → 𝐶 ∈ ℋ ) |
12 |
|
hvmulcl |
⊢ ( ( ( 𝑥 ·ih 𝐷 ) ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( ( 𝑥 ·ih 𝐷 ) ·ℎ 𝐶 ) ∈ ℋ ) |
13 |
10 11 12
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑥 ·ih 𝐷 ) ·ℎ 𝐶 ) ∈ ℋ ) |
14 |
|
kbval |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ ( ( 𝑥 ·ih 𝐷 ) ·ℎ 𝐶 ) ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ ( ( 𝑥 ·ih 𝐷 ) ·ℎ 𝐶 ) ) = ( ( ( ( 𝑥 ·ih 𝐷 ) ·ℎ 𝐶 ) ·ih 𝐵 ) ·ℎ 𝐴 ) ) |
15 |
5 6 13 14
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ ( ( 𝑥 ·ih 𝐷 ) ·ℎ 𝐶 ) ) = ( ( ( ( 𝑥 ·ih 𝐷 ) ·ℎ 𝐶 ) ·ih 𝐵 ) ·ℎ 𝐴 ) ) |
16 |
4 15
|
eqtrd |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ ( ( 𝐶 ketbra 𝐷 ) ‘ 𝑥 ) ) = ( ( ( ( 𝑥 ·ih 𝐷 ) ·ℎ 𝐶 ) ·ih 𝐵 ) ·ℎ 𝐴 ) ) |
17 |
|
kbop |
⊢ ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( 𝐶 ketbra 𝐷 ) : ℋ ⟶ ℋ ) |
18 |
17
|
adantl |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( 𝐶 ketbra 𝐷 ) : ℋ ⟶ ℋ ) |
19 |
|
fvco3 |
⊢ ( ( ( 𝐶 ketbra 𝐷 ) : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ‘ 𝑥 ) = ( ( 𝐴 ketbra 𝐵 ) ‘ ( ( 𝐶 ketbra 𝐷 ) ‘ 𝑥 ) ) ) |
20 |
18 19
|
sylan |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ‘ 𝑥 ) = ( ( 𝐴 ketbra 𝐵 ) ‘ ( ( 𝐶 ketbra 𝐷 ) ‘ 𝑥 ) ) ) |
21 |
|
kbval |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) = ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ) |
22 |
5 6 11 21
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) = ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ) |
23 |
22
|
oveq2d |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑥 ·ih 𝐷 ) ·ℎ ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ) = ( ( 𝑥 ·ih 𝐷 ) ·ℎ ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ) ) |
24 |
|
kbop |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ketbra 𝐵 ) : ℋ ⟶ ℋ ) |
25 |
24
|
ffvelrnda |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ∈ ℋ ) |
26 |
25
|
adantrr |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ∈ ℋ ) |
27 |
26
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ∈ ℋ ) |
28 |
|
kbval |
⊢ ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ∈ ℋ ∧ 𝐷 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ‘ 𝑥 ) = ( ( 𝑥 ·ih 𝐷 ) ·ℎ ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ) ) |
29 |
27 8 7 28
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ‘ 𝑥 ) = ( ( 𝑥 ·ih 𝐷 ) ·ℎ ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ) ) |
30 |
|
ax-his3 |
⊢ ( ( ( 𝑥 ·ih 𝐷 ) ∈ ℂ ∧ 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( 𝑥 ·ih 𝐷 ) ·ℎ 𝐶 ) ·ih 𝐵 ) = ( ( 𝑥 ·ih 𝐷 ) · ( 𝐶 ·ih 𝐵 ) ) ) |
31 |
10 11 6 30
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑥 ·ih 𝐷 ) ·ℎ 𝐶 ) ·ih 𝐵 ) = ( ( 𝑥 ·ih 𝐷 ) · ( 𝐶 ·ih 𝐵 ) ) ) |
32 |
31
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( ( 𝑥 ·ih 𝐷 ) ·ℎ 𝐶 ) ·ih 𝐵 ) ·ℎ 𝐴 ) = ( ( ( 𝑥 ·ih 𝐷 ) · ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐴 ) ) |
33 |
|
hicl |
⊢ ( ( 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐶 ·ih 𝐵 ) ∈ ℂ ) |
34 |
11 6 33
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( 𝐶 ·ih 𝐵 ) ∈ ℂ ) |
35 |
|
ax-hvmulass |
⊢ ( ( ( 𝑥 ·ih 𝐷 ) ∈ ℂ ∧ ( 𝐶 ·ih 𝐵 ) ∈ ℂ ∧ 𝐴 ∈ ℋ ) → ( ( ( 𝑥 ·ih 𝐷 ) · ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐴 ) = ( ( 𝑥 ·ih 𝐷 ) ·ℎ ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ) ) |
36 |
10 34 5 35
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑥 ·ih 𝐷 ) · ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐴 ) = ( ( 𝑥 ·ih 𝐷 ) ·ℎ ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ) ) |
37 |
32 36
|
eqtrd |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( ( 𝑥 ·ih 𝐷 ) ·ℎ 𝐶 ) ·ih 𝐵 ) ·ℎ 𝐴 ) = ( ( 𝑥 ·ih 𝐷 ) ·ℎ ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ) ) |
38 |
23 29 37
|
3eqtr4d |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ‘ 𝑥 ) = ( ( ( ( 𝑥 ·ih 𝐷 ) ·ℎ 𝐶 ) ·ih 𝐵 ) ·ℎ 𝐴 ) ) |
39 |
16 20 38
|
3eqtr4d |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ‘ 𝑥 ) = ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ‘ 𝑥 ) ) |
40 |
39
|
ralrimiva |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ∀ 𝑥 ∈ ℋ ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ‘ 𝑥 ) = ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ‘ 𝑥 ) ) |
41 |
|
fco |
⊢ ( ( ( 𝐴 ketbra 𝐵 ) : ℋ ⟶ ℋ ∧ ( 𝐶 ketbra 𝐷 ) : ℋ ⟶ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) : ℋ ⟶ ℋ ) |
42 |
24 17 41
|
syl2an |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) : ℋ ⟶ ℋ ) |
43 |
|
kbop |
⊢ ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) : ℋ ⟶ ℋ ) |
44 |
25 43
|
sylan |
⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝐶 ∈ ℋ ) ∧ 𝐷 ∈ ℋ ) → ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) : ℋ ⟶ ℋ ) |
45 |
44
|
anasss |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) : ℋ ⟶ ℋ ) |
46 |
|
ffn |
⊢ ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) : ℋ ⟶ ℋ → ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) Fn ℋ ) |
47 |
|
ffn |
⊢ ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) : ℋ ⟶ ℋ → ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) Fn ℋ ) |
48 |
|
eqfnfv |
⊢ ( ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) Fn ℋ ∧ ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) Fn ℋ ) → ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) = ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ↔ ∀ 𝑥 ∈ ℋ ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ‘ 𝑥 ) = ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ‘ 𝑥 ) ) ) |
49 |
46 47 48
|
syl2an |
⊢ ( ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) : ℋ ⟶ ℋ ∧ ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) : ℋ ⟶ ℋ ) → ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) = ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ↔ ∀ 𝑥 ∈ ℋ ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ‘ 𝑥 ) = ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ‘ 𝑥 ) ) ) |
50 |
42 45 49
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) = ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ↔ ∀ 𝑥 ∈ ℋ ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ‘ 𝑥 ) = ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ‘ 𝑥 ) ) ) |
51 |
40 50
|
mpbird |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) = ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ) |