Step | Hyp | Ref
| Expression |
1 | | funadj 30248 |
. . . . . . 7
⊢ Fun
adjℎ |
2 | | funfvop 6927 |
. . . . . . 7
⊢ ((Fun
adjℎ ∧ 𝑇 ∈ dom adjℎ) →
〈𝑇,
(adjℎ‘𝑇)〉 ∈
adjℎ) |
3 | 1, 2 | mpan 687 |
. . . . . 6
⊢ (𝑇 ∈ dom
adjℎ → 〈𝑇, (adjℎ‘𝑇)〉 ∈
adjℎ) |
4 | | dfadj2 30247 |
. . . . . 6
⊢
adjℎ = {〈𝑧, 𝑤〉 ∣ (𝑧: ℋ⟶ ℋ ∧ 𝑤: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑧‘𝑦)) = ((𝑤‘𝑥) ·ih 𝑦))} |
5 | 3, 4 | eleqtrdi 2849 |
. . . . 5
⊢ (𝑇 ∈ dom
adjℎ → 〈𝑇, (adjℎ‘𝑇)〉 ∈ {〈𝑧, 𝑤〉 ∣ (𝑧: ℋ⟶ ℋ ∧ 𝑤: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑧‘𝑦)) = ((𝑤‘𝑥) ·ih 𝑦))}) |
6 | | fvex 6787 |
. . . . . 6
⊢
(adjℎ‘𝑇) ∈ V |
7 | | feq1 6581 |
. . . . . . . 8
⊢ (𝑧 = 𝑇 → (𝑧: ℋ⟶ ℋ ↔ 𝑇: ℋ⟶
ℋ)) |
8 | | fveq1 6773 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑇 → (𝑧‘𝑦) = (𝑇‘𝑦)) |
9 | 8 | oveq2d 7291 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑇 → (𝑥 ·ih (𝑧‘𝑦)) = (𝑥 ·ih (𝑇‘𝑦))) |
10 | 9 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑧 = 𝑇 → ((𝑥 ·ih (𝑧‘𝑦)) = ((𝑤‘𝑥) ·ih 𝑦) ↔ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑤‘𝑥) ·ih 𝑦))) |
11 | 10 | 2ralbidv 3129 |
. . . . . . . 8
⊢ (𝑧 = 𝑇 → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑧‘𝑦)) = ((𝑤‘𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑤‘𝑥) ·ih 𝑦))) |
12 | 7, 11 | 3anbi13d 1437 |
. . . . . . 7
⊢ (𝑧 = 𝑇 → ((𝑧: ℋ⟶ ℋ ∧ 𝑤: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑧‘𝑦)) = ((𝑤‘𝑥) ·ih 𝑦)) ↔ (𝑇: ℋ⟶ ℋ ∧ 𝑤: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑇‘𝑦)) = ((𝑤‘𝑥) ·ih 𝑦)))) |
13 | | feq1 6581 |
. . . . . . . 8
⊢ (𝑤 =
(adjℎ‘𝑇) → (𝑤: ℋ⟶ ℋ ↔
(adjℎ‘𝑇): ℋ⟶
ℋ)) |
14 | | fveq1 6773 |
. . . . . . . . . . 11
⊢ (𝑤 =
(adjℎ‘𝑇) → (𝑤‘𝑥) = ((adjℎ‘𝑇)‘𝑥)) |
15 | 14 | oveq1d 7290 |
. . . . . . . . . 10
⊢ (𝑤 =
(adjℎ‘𝑇) → ((𝑤‘𝑥) ·ih 𝑦) =
(((adjℎ‘𝑇)‘𝑥) ·ih 𝑦)) |
16 | 15 | eqeq2d 2749 |
. . . . . . . . 9
⊢ (𝑤 =
(adjℎ‘𝑇) → ((𝑥 ·ih (𝑇‘𝑦)) = ((𝑤‘𝑥) ·ih 𝑦) ↔ (𝑥 ·ih (𝑇‘𝑦)) = (((adjℎ‘𝑇)‘𝑥) ·ih 𝑦))) |
17 | 16 | 2ralbidv 3129 |
. . . . . . . 8
⊢ (𝑤 =
(adjℎ‘𝑇) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑤‘𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥
·ih (𝑇‘𝑦)) = (((adjℎ‘𝑇)‘𝑥) ·ih 𝑦))) |
18 | 13, 17 | 3anbi23d 1438 |
. . . . . . 7
⊢ (𝑤 =
(adjℎ‘𝑇) → ((𝑇: ℋ⟶ ℋ ∧ 𝑤: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑇‘𝑦)) = ((𝑤‘𝑥) ·ih 𝑦)) ↔ (𝑇: ℋ⟶ ℋ ∧
(adjℎ‘𝑇): ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑇‘𝑦)) = (((adjℎ‘𝑇)‘𝑥) ·ih 𝑦)))) |
19 | 12, 18 | opelopabg 5451 |
. . . . . 6
⊢ ((𝑇 ∈ dom
adjℎ ∧ (adjℎ‘𝑇) ∈ V) → (〈𝑇, (adjℎ‘𝑇)〉 ∈ {〈𝑧, 𝑤〉 ∣ (𝑧: ℋ⟶ ℋ ∧ 𝑤: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑧‘𝑦)) = ((𝑤‘𝑥) ·ih 𝑦))} ↔ (𝑇: ℋ⟶ ℋ ∧
(adjℎ‘𝑇): ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑇‘𝑦)) = (((adjℎ‘𝑇)‘𝑥) ·ih 𝑦)))) |
20 | 6, 19 | mpan2 688 |
. . . . 5
⊢ (𝑇 ∈ dom
adjℎ → (〈𝑇, (adjℎ‘𝑇)〉 ∈ {〈𝑧, 𝑤〉 ∣ (𝑧: ℋ⟶ ℋ ∧ 𝑤: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑧‘𝑦)) = ((𝑤‘𝑥) ·ih 𝑦))} ↔ (𝑇: ℋ⟶ ℋ ∧
(adjℎ‘𝑇): ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑇‘𝑦)) = (((adjℎ‘𝑇)‘𝑥) ·ih 𝑦)))) |
21 | 5, 20 | mpbid 231 |
. . . 4
⊢ (𝑇 ∈ dom
adjℎ → (𝑇: ℋ⟶ ℋ ∧
(adjℎ‘𝑇): ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑇‘𝑦)) = (((adjℎ‘𝑇)‘𝑥) ·ih 𝑦))) |
22 | 21 | simp3d 1143 |
. . 3
⊢ (𝑇 ∈ dom
adjℎ → ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = (((adjℎ‘𝑇)‘𝑥) ·ih 𝑦)) |
23 | | oveq1 7282 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 ·ih (𝑇‘𝑦)) = (𝐴 ·ih (𝑇‘𝑦))) |
24 | | fveq2 6774 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((adjℎ‘𝑇)‘𝑥) = ((adjℎ‘𝑇)‘𝐴)) |
25 | 24 | oveq1d 7290 |
. . . . 5
⊢ (𝑥 = 𝐴 →
(((adjℎ‘𝑇)‘𝑥) ·ih 𝑦) =
(((adjℎ‘𝑇)‘𝐴) ·ih 𝑦)) |
26 | 23, 25 | eqeq12d 2754 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝑥 ·ih (𝑇‘𝑦)) = (((adjℎ‘𝑇)‘𝑥) ·ih 𝑦) ↔ (𝐴 ·ih (𝑇‘𝑦)) = (((adjℎ‘𝑇)‘𝐴) ·ih 𝑦))) |
27 | | fveq2 6774 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝑇‘𝑦) = (𝑇‘𝐵)) |
28 | 27 | oveq2d 7291 |
. . . . 5
⊢ (𝑦 = 𝐵 → (𝐴 ·ih (𝑇‘𝑦)) = (𝐴 ·ih (𝑇‘𝐵))) |
29 | | oveq2 7283 |
. . . . 5
⊢ (𝑦 = 𝐵 →
(((adjℎ‘𝑇)‘𝐴) ·ih 𝑦) =
(((adjℎ‘𝑇)‘𝐴) ·ih 𝐵)) |
30 | 28, 29 | eqeq12d 2754 |
. . . 4
⊢ (𝑦 = 𝐵 → ((𝐴 ·ih (𝑇‘𝑦)) = (((adjℎ‘𝑇)‘𝐴) ·ih 𝑦) ↔ (𝐴 ·ih (𝑇‘𝐵)) = (((adjℎ‘𝑇)‘𝐴) ·ih 𝐵))) |
31 | 26, 30 | rspc2v 3570 |
. . 3
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) →
(∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑇‘𝑦)) = (((adjℎ‘𝑇)‘𝑥) ·ih 𝑦) → (𝐴 ·ih (𝑇‘𝐵)) = (((adjℎ‘𝑇)‘𝐴) ·ih 𝐵))) |
32 | 22, 31 | syl5com 31 |
. 2
⊢ (𝑇 ∈ dom
adjℎ → ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih (𝑇‘𝐵)) = (((adjℎ‘𝑇)‘𝐴) ·ih 𝐵))) |
33 | 32 | 3impib 1115 |
1
⊢ ((𝑇 ∈ dom
adjℎ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih (𝑇‘𝐵)) = (((adjℎ‘𝑇)‘𝐴) ·ih 𝐵)) |