Step |
Hyp |
Ref |
Expression |
1 |
|
ralcom |
⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ) |
2 |
|
fveq2 |
⊢ ( 𝑧 = 𝑦 → ( 𝑆 ‘ 𝑧 ) = ( 𝑆 ‘ 𝑦 ) ) |
3 |
2
|
oveq2d |
⊢ ( 𝑧 = 𝑦 → ( 𝑥 ·ih ( 𝑆 ‘ 𝑧 ) ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) |
4 |
|
oveq2 |
⊢ ( 𝑧 = 𝑦 → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ) |
5 |
3 4
|
eqeq12d |
⊢ ( 𝑧 = 𝑦 → ( ( 𝑥 ·ih ( 𝑆 ‘ 𝑧 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) ↔ ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ) ) |
6 |
5
|
ralbidv |
⊢ ( 𝑧 = 𝑦 → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑧 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) ↔ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ) ) |
7 |
6
|
cbvralvw |
⊢ ( ∀ 𝑧 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑧 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) ↔ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ) |
8 |
1 7
|
bitr4i |
⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑧 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑧 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) ) |
9 |
|
oveq1 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ·ih ( 𝑆 ‘ 𝑧 ) ) = ( 𝑦 ·ih ( 𝑆 ‘ 𝑧 ) ) ) |
10 |
|
fveq2 |
⊢ ( 𝑥 = 𝑦 → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑦 ) ) |
11 |
10
|
oveq1d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑧 ) ) |
12 |
9 11
|
eqeq12d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ·ih ( 𝑆 ‘ 𝑧 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) ↔ ( 𝑦 ·ih ( 𝑆 ‘ 𝑧 ) ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑧 ) ) ) |
13 |
12
|
cbvralvw |
⊢ ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑧 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) ↔ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑆 ‘ 𝑧 ) ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑧 ) ) |
14 |
13
|
ralbii |
⊢ ( ∀ 𝑧 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑧 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) ↔ ∀ 𝑧 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑆 ‘ 𝑧 ) ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑧 ) ) |
15 |
|
fveq2 |
⊢ ( 𝑧 = 𝑥 → ( 𝑆 ‘ 𝑧 ) = ( 𝑆 ‘ 𝑥 ) ) |
16 |
15
|
oveq2d |
⊢ ( 𝑧 = 𝑥 → ( 𝑦 ·ih ( 𝑆 ‘ 𝑧 ) ) = ( 𝑦 ·ih ( 𝑆 ‘ 𝑥 ) ) ) |
17 |
|
oveq2 |
⊢ ( 𝑧 = 𝑥 → ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑧 ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) ) |
18 |
16 17
|
eqeq12d |
⊢ ( 𝑧 = 𝑥 → ( ( 𝑦 ·ih ( 𝑆 ‘ 𝑧 ) ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑧 ) ↔ ( 𝑦 ·ih ( 𝑆 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) ) ) |
19 |
18
|
ralbidv |
⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑆 ‘ 𝑧 ) ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑧 ) ↔ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑆 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) ) ) |
20 |
19
|
cbvralvw |
⊢ ( ∀ 𝑧 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑆 ‘ 𝑧 ) ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑧 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑆 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) ) |
21 |
8 14 20
|
3bitri |
⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑆 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) ) |
22 |
|
ffvelrn |
⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑇 ‘ 𝑦 ) ∈ ℋ ) |
23 |
|
ax-his1 |
⊢ ( ( ( 𝑇 ‘ 𝑦 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ) ) |
24 |
22 23
|
sylan |
⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ) ) |
25 |
24
|
adantrl |
⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ) ) |
26 |
|
ffvelrn |
⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑆 ‘ 𝑥 ) ∈ ℋ ) |
27 |
|
ax-his1 |
⊢ ( ( 𝑦 ∈ ℋ ∧ ( 𝑆 ‘ 𝑥 ) ∈ ℋ ) → ( 𝑦 ·ih ( 𝑆 ‘ 𝑥 ) ) = ( ∗ ‘ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ) ) |
28 |
26 27
|
sylan2 |
⊢ ( ( 𝑦 ∈ ℋ ∧ ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( 𝑦 ·ih ( 𝑆 ‘ 𝑥 ) ) = ( ∗ ‘ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ) ) |
29 |
28
|
adantll |
⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( 𝑦 ·ih ( 𝑆 ‘ 𝑥 ) ) = ( ∗ ‘ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ) ) |
30 |
25 29
|
eqeq12d |
⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑆 ‘ 𝑥 ) ) ↔ ( ∗ ‘ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ) = ( ∗ ‘ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ) ) ) |
31 |
30
|
ancoms |
⊢ ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑆 ‘ 𝑥 ) ) ↔ ( ∗ ‘ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ) = ( ∗ ‘ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ) ) ) |
32 |
|
hicl |
⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑦 ) ∈ ℋ ) → ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ∈ ℂ ) |
33 |
22 32
|
sylan2 |
⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ∈ ℂ ) |
34 |
33
|
adantll |
⊢ ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ∈ ℂ ) |
35 |
|
hicl |
⊢ ( ( ( 𝑆 ‘ 𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ∈ ℂ ) |
36 |
26 35
|
sylan |
⊢ ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ∈ ℂ ) |
37 |
36
|
adantrl |
⊢ ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ∈ ℂ ) |
38 |
|
cj11 |
⊢ ( ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ∈ ℂ ∧ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ∈ ℂ ) → ( ( ∗ ‘ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ) = ( ∗ ‘ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ) ) |
39 |
34 37 38
|
syl2anc |
⊢ ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ∗ ‘ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ) = ( ∗ ‘ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ) ) |
40 |
31 39
|
bitr2d |
⊢ ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑆 ‘ 𝑥 ) ) ) ) |
41 |
40
|
an4s |
⊢ ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑆 ‘ 𝑥 ) ) ) ) |
42 |
41
|
anassrs |
⊢ ( ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑆 ‘ 𝑥 ) ) ) ) |
43 |
|
eqcom |
⊢ ( ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑆 ‘ 𝑥 ) ) ↔ ( 𝑦 ·ih ( 𝑆 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) ) |
44 |
42 43
|
syl6bb |
⊢ ( ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( 𝑦 ·ih ( 𝑆 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) ) ) |
45 |
44
|
ralbidva |
⊢ ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑆 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) ) ) |
46 |
45
|
ralbidva |
⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑆 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) ) ) |
47 |
21 46
|
bitr4id |
⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) ) ) |