Step |
Hyp |
Ref |
Expression |
1 |
|
cnvopab |
⊢ ◡ { 〈 𝑢 , 𝑡 〉 ∣ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) } = { 〈 𝑡 , 𝑢 〉 ∣ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) } |
2 |
|
3ancoma |
⊢ ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ) |
3 |
|
ffvelrn |
⊢ ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑢 ‘ 𝑦 ) ∈ ℋ ) |
4 |
|
ax-his1 |
⊢ ( ( ( 𝑢 ‘ 𝑦 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ) ) |
5 |
3 4
|
sylan |
⊢ ( ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ) ) |
6 |
5
|
adantrl |
⊢ ( ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ) ) |
7 |
|
ffvelrn |
⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑡 ‘ 𝑥 ) ∈ ℋ ) |
8 |
|
ax-his1 |
⊢ ( ( 𝑦 ∈ ℋ ∧ ( 𝑡 ‘ 𝑥 ) ∈ ℋ ) → ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) = ( ∗ ‘ ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ) |
9 |
7 8
|
sylan2 |
⊢ ( ( 𝑦 ∈ ℋ ∧ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) = ( ∗ ‘ ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ) |
10 |
9
|
adantll |
⊢ ( ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) = ( ∗ ‘ ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ) |
11 |
6 10
|
eqeq12d |
⊢ ( ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) ↔ ( ∗ ‘ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ) = ( ∗ ‘ ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ) ) |
12 |
11
|
ancoms |
⊢ ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) ↔ ( ∗ ‘ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ) = ( ∗ ‘ ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ) ) |
13 |
|
hicl |
⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑢 ‘ 𝑦 ) ∈ ℋ ) → ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ∈ ℂ ) |
14 |
3 13
|
sylan2 |
⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ∈ ℂ ) |
15 |
14
|
adantll |
⊢ ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ∈ ℂ ) |
16 |
|
hicl |
⊢ ( ( ( 𝑡 ‘ 𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ∈ ℂ ) |
17 |
7 16
|
sylan |
⊢ ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ∈ ℂ ) |
18 |
17
|
adantrl |
⊢ ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ∈ ℂ ) |
19 |
|
cj11 |
⊢ ( ( ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ∈ ℂ ∧ ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ∈ ℂ ) → ( ( ∗ ‘ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ) = ( ∗ ‘ ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ) |
20 |
15 18 19
|
syl2anc |
⊢ ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ∗ ‘ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ) = ( ∗ ‘ ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ) |
21 |
12 20
|
bitr2d |
⊢ ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) ) ) |
22 |
21
|
an4s |
⊢ ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) ) ) |
23 |
22
|
anassrs |
⊢ ( ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) ) ) |
24 |
|
eqcom |
⊢ ( ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) ↔ ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) = ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) ) |
25 |
23 24
|
syl6bb |
⊢ ( ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) = ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) ) ) |
26 |
25
|
ralbidva |
⊢ ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) = ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) ) ) |
27 |
26
|
ralbidva |
⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) = ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) ) ) |
28 |
|
ralcom |
⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) = ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) ↔ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) = ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) ) |
29 |
27 28
|
syl6bb |
⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) = ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) ) ) |
30 |
29
|
pm5.32i |
⊢ ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ↔ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) = ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) ) ) |
31 |
|
df-3an |
⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ↔ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ) |
32 |
|
df-3an |
⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) = ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) ) ↔ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) = ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) ) ) |
33 |
30 31 32
|
3bitr4i |
⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) = ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) ) ) |
34 |
2 33
|
bitri |
⊢ ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) = ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) ) ) |
35 |
34
|
opabbii |
⊢ { 〈 𝑡 , 𝑢 〉 ∣ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) } = { 〈 𝑡 , 𝑢 〉 ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) = ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) ) } |
36 |
1 35
|
eqtri |
⊢ ◡ { 〈 𝑢 , 𝑡 〉 ∣ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) } = { 〈 𝑡 , 𝑢 〉 ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) = ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) ) } |
37 |
|
dfadj2 |
⊢ adjℎ = { 〈 𝑢 , 𝑡 〉 ∣ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) } |
38 |
37
|
cnveqi |
⊢ ◡ adjℎ = ◡ { 〈 𝑢 , 𝑡 〉 ∣ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) } |
39 |
|
dfadj2 |
⊢ adjℎ = { 〈 𝑡 , 𝑢 〉 ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡 ‘ 𝑥 ) ) = ( ( 𝑢 ‘ 𝑦 ) ·ih 𝑥 ) ) } |
40 |
36 38 39
|
3eqtr4i |
⊢ ◡ adjℎ = adjℎ |