| Step | Hyp | Ref
| Expression |
| 1 | | cnvopab 6157 |
. . 3
⊢ ◡{〈𝑢, 𝑡〉 ∣ (𝑢: ℋ⟶ ℋ ∧ 𝑡: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦))} = {〈𝑡, 𝑢〉 ∣ (𝑢: ℋ⟶ ℋ ∧ 𝑡: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦))} |
| 2 | | 3ancoma 1098 |
. . . . 5
⊢ ((𝑢: ℋ⟶ ℋ ∧
𝑡: ℋ⟶ ℋ
∧ ∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦)) ↔ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦))) |
| 3 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) →
(𝑢‘𝑦) ∈ ℋ) |
| 4 | | ax-his1 31101 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑢‘𝑦) ∈ ℋ ∧ 𝑥 ∈ ℋ) → ((𝑢‘𝑦) ·ih 𝑥) = (∗‘(𝑥
·ih (𝑢‘𝑦)))) |
| 5 | 3, 4 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑢: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) ∧
𝑥 ∈ ℋ) →
((𝑢‘𝑦)
·ih 𝑥) = (∗‘(𝑥 ·ih (𝑢‘𝑦)))) |
| 6 | 5 | adantrl 716 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑢: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) ∧
(𝑡: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ))
→ ((𝑢‘𝑦)
·ih 𝑥) = (∗‘(𝑥 ·ih (𝑢‘𝑦)))) |
| 7 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑡: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(𝑡‘𝑥) ∈ ℋ) |
| 8 | | ax-his1 31101 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℋ ∧ (𝑡‘𝑥) ∈ ℋ) → (𝑦 ·ih (𝑡‘𝑥)) = (∗‘((𝑡‘𝑥) ·ih 𝑦))) |
| 9 | 7, 8 | sylan2 593 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℋ ∧ (𝑡: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ)) →
(𝑦
·ih (𝑡‘𝑥)) = (∗‘((𝑡‘𝑥) ·ih 𝑦))) |
| 10 | 9 | adantll 714 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑢: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) ∧
(𝑡: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ))
→ (𝑦
·ih (𝑡‘𝑥)) = (∗‘((𝑡‘𝑥) ·ih 𝑦))) |
| 11 | 6, 10 | eqeq12d 2753 |
. . . . . . . . . . . . . . 15
⊢ (((𝑢: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) ∧
(𝑡: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ))
→ (((𝑢‘𝑦)
·ih 𝑥) = (𝑦 ·ih (𝑡‘𝑥)) ↔ (∗‘(𝑥 ·ih (𝑢‘𝑦))) = (∗‘((𝑡‘𝑥) ·ih 𝑦)))) |
| 12 | 11 | ancoms 458 |
. . . . . . . . . . . . . 14
⊢ (((𝑡: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑢: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ (((𝑢‘𝑦)
·ih 𝑥) = (𝑦 ·ih (𝑡‘𝑥)) ↔ (∗‘(𝑥 ·ih (𝑢‘𝑦))) = (∗‘((𝑡‘𝑥) ·ih 𝑦)))) |
| 13 | | hicl 31099 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℋ ∧ (𝑢‘𝑦) ∈ ℋ) → (𝑥 ·ih (𝑢‘𝑦)) ∈ ℂ) |
| 14 | 3, 13 | sylan2 593 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℋ ∧ (𝑢: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ)) →
(𝑥
·ih (𝑢‘𝑦)) ∈ ℂ) |
| 15 | 14 | adantll 714 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑢: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ (𝑥
·ih (𝑢‘𝑦)) ∈ ℂ) |
| 16 | | hicl 31099 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑡‘𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑡‘𝑥) ·ih 𝑦) ∈
ℂ) |
| 17 | 7, 16 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
𝑦 ∈ ℋ) →
((𝑡‘𝑥)
·ih 𝑦) ∈ ℂ) |
| 18 | 17 | adantrl 716 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑢: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ ((𝑡‘𝑥)
·ih 𝑦) ∈ ℂ) |
| 19 | | cj11 15201 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥
·ih (𝑢‘𝑦)) ∈ ℂ ∧ ((𝑡‘𝑥) ·ih 𝑦) ∈ ℂ) →
((∗‘(𝑥
·ih (𝑢‘𝑦))) = (∗‘((𝑡‘𝑥) ·ih 𝑦)) ↔ (𝑥 ·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦))) |
| 20 | 15, 18, 19 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝑡: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑢: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ ((∗‘(𝑥
·ih (𝑢‘𝑦))) = (∗‘((𝑡‘𝑥) ·ih 𝑦)) ↔ (𝑥 ·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦))) |
| 21 | 12, 20 | bitr2d 280 |
. . . . . . . . . . . . 13
⊢ (((𝑡: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑢: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ ((𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦) ↔ ((𝑢‘𝑦) ·ih 𝑥) = (𝑦 ·ih (𝑡‘𝑥)))) |
| 22 | 21 | an4s 660 |
. . . . . . . . . . . 12
⊢ (((𝑡: ℋ⟶ ℋ ∧
𝑢: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ ((𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦) ↔ ((𝑢‘𝑦) ·ih 𝑥) = (𝑦 ·ih (𝑡‘𝑥)))) |
| 23 | 22 | anassrs 467 |
. . . . . . . . . . 11
⊢ ((((𝑡: ℋ⟶ ℋ ∧
𝑢: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
∧ 𝑦 ∈ ℋ)
→ ((𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦) ↔ ((𝑢‘𝑦) ·ih 𝑥) = (𝑦 ·ih (𝑡‘𝑥)))) |
| 24 | | eqcom 2744 |
. . . . . . . . . . 11
⊢ (((𝑢‘𝑦) ·ih 𝑥) = (𝑦 ·ih (𝑡‘𝑥)) ↔ (𝑦 ·ih (𝑡‘𝑥)) = ((𝑢‘𝑦) ·ih 𝑥)) |
| 25 | 23, 24 | bitrdi 287 |
. . . . . . . . . 10
⊢ ((((𝑡: ℋ⟶ ℋ ∧
𝑢: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
∧ 𝑦 ∈ ℋ)
→ ((𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦) ↔ (𝑦 ·ih (𝑡‘𝑥)) = ((𝑢‘𝑦) ·ih 𝑥))) |
| 26 | 25 | ralbidva 3176 |
. . . . . . . . 9
⊢ (((𝑡: ℋ⟶ ℋ ∧
𝑢: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ (∀𝑦 ∈
ℋ (𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦) ↔ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑡‘𝑥)) = ((𝑢‘𝑦) ·ih 𝑥))) |
| 27 | 26 | ralbidva 3176 |
. . . . . . . 8
⊢ ((𝑡: ℋ⟶ ℋ ∧
𝑢: ℋ⟶ ℋ)
→ (∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑡‘𝑥)) = ((𝑢‘𝑦) ·ih 𝑥))) |
| 28 | | ralcom 3289 |
. . . . . . . 8
⊢
(∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑦
·ih (𝑡‘𝑥)) = ((𝑢‘𝑦) ·ih 𝑥) ↔ ∀𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑦
·ih (𝑡‘𝑥)) = ((𝑢‘𝑦) ·ih 𝑥)) |
| 29 | 27, 28 | bitrdi 287 |
. . . . . . 7
⊢ ((𝑡: ℋ⟶ ℋ ∧
𝑢: ℋ⟶ ℋ)
→ (∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦) ↔ ∀𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑦
·ih (𝑡‘𝑥)) = ((𝑢‘𝑦) ·ih 𝑥))) |
| 30 | 29 | pm5.32i 574 |
. . . . . 6
⊢ (((𝑡: ℋ⟶ ℋ ∧
𝑢: ℋ⟶ ℋ)
∧ ∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦)) ↔ ((𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ) ∧
∀𝑦 ∈ ℋ
∀𝑥 ∈ ℋ
(𝑦
·ih (𝑡‘𝑥)) = ((𝑢‘𝑦) ·ih 𝑥))) |
| 31 | | df-3an 1089 |
. . . . . 6
⊢ ((𝑡: ℋ⟶ ℋ ∧
𝑢: ℋ⟶ ℋ
∧ ∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦)) ↔ ((𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ) ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦))) |
| 32 | | df-3an 1089 |
. . . . . 6
⊢ ((𝑡: ℋ⟶ ℋ ∧
𝑢: ℋ⟶ ℋ
∧ ∀𝑦 ∈
ℋ ∀𝑥 ∈
ℋ (𝑦
·ih (𝑡‘𝑥)) = ((𝑢‘𝑦) ·ih 𝑥)) ↔ ((𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ) ∧
∀𝑦 ∈ ℋ
∀𝑥 ∈ ℋ
(𝑦
·ih (𝑡‘𝑥)) = ((𝑢‘𝑦) ·ih 𝑥))) |
| 33 | 30, 31, 32 | 3bitr4i 303 |
. . . . 5
⊢ ((𝑡: ℋ⟶ ℋ ∧
𝑢: ℋ⟶ ℋ
∧ ∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦)) ↔ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧
∀𝑦 ∈ ℋ
∀𝑥 ∈ ℋ
(𝑦
·ih (𝑡‘𝑥)) = ((𝑢‘𝑦) ·ih 𝑥))) |
| 34 | 2, 33 | bitri 275 |
. . . 4
⊢ ((𝑢: ℋ⟶ ℋ ∧
𝑡: ℋ⟶ ℋ
∧ ∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦)) ↔ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧
∀𝑦 ∈ ℋ
∀𝑥 ∈ ℋ
(𝑦
·ih (𝑡‘𝑥)) = ((𝑢‘𝑦) ·ih 𝑥))) |
| 35 | 34 | opabbii 5210 |
. . 3
⊢
{〈𝑡, 𝑢〉 ∣ (𝑢: ℋ⟶ ℋ ∧
𝑡: ℋ⟶ ℋ
∧ ∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦))} = {〈𝑡, 𝑢〉 ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧
∀𝑦 ∈ ℋ
∀𝑥 ∈ ℋ
(𝑦
·ih (𝑡‘𝑥)) = ((𝑢‘𝑦) ·ih 𝑥))} |
| 36 | 1, 35 | eqtri 2765 |
. 2
⊢ ◡{〈𝑢, 𝑡〉 ∣ (𝑢: ℋ⟶ ℋ ∧ 𝑡: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦))} = {〈𝑡, 𝑢〉 ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧
∀𝑦 ∈ ℋ
∀𝑥 ∈ ℋ
(𝑦
·ih (𝑡‘𝑥)) = ((𝑢‘𝑦) ·ih 𝑥))} |
| 37 | | dfadj2 31904 |
. . 3
⊢
adjℎ = {〈𝑢, 𝑡〉 ∣ (𝑢: ℋ⟶ ℋ ∧ 𝑡: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦))} |
| 38 | 37 | cnveqi 5885 |
. 2
⊢ ◡adjℎ = ◡{〈𝑢, 𝑡〉 ∣ (𝑢: ℋ⟶ ℋ ∧ 𝑡: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑢‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦))} |
| 39 | | dfadj2 31904 |
. 2
⊢
adjℎ = {〈𝑡, 𝑢〉 ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧
∀𝑦 ∈ ℋ
∀𝑥 ∈ ℋ
(𝑦
·ih (𝑡‘𝑥)) = ((𝑢‘𝑦) ·ih 𝑥))} |
| 40 | 36, 38, 39 | 3eqtr4i 2775 |
1
⊢ ◡adjℎ =
adjℎ |