Step | Hyp | Ref
| Expression |
1 | | ralcom 3166 |
. . . 4
⊢
(∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦) ↔ ∀𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦)) |
2 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → (𝑆‘𝑧) = (𝑆‘𝑦)) |
3 | 2 | oveq2d 7291 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (𝑥 ·ih (𝑆‘𝑧)) = (𝑥 ·ih (𝑆‘𝑦))) |
4 | | oveq2 7283 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → ((𝑇‘𝑥) ·ih 𝑧) = ((𝑇‘𝑥) ·ih 𝑦)) |
5 | 3, 4 | eqeq12d 2754 |
. . . . . 6
⊢ (𝑧 = 𝑦 → ((𝑥 ·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧) ↔ (𝑥 ·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦))) |
6 | 5 | ralbidv 3112 |
. . . . 5
⊢ (𝑧 = 𝑦 → (∀𝑥 ∈ ℋ (𝑥 ·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧) ↔ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦))) |
7 | 6 | cbvralvw 3383 |
. . . 4
⊢
(∀𝑧 ∈
ℋ ∀𝑥 ∈
ℋ (𝑥
·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧) ↔ ∀𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦)) |
8 | 1, 7 | bitr4i 277 |
. . 3
⊢
(∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦) ↔ ∀𝑧 ∈ ℋ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧)) |
9 | | oveq1 7282 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ·ih (𝑆‘𝑧)) = (𝑦 ·ih (𝑆‘𝑧))) |
10 | | fveq2 6774 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑇‘𝑥) = (𝑇‘𝑦)) |
11 | 10 | oveq1d 7290 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑇‘𝑥) ·ih 𝑧) = ((𝑇‘𝑦) ·ih 𝑧)) |
12 | 9, 11 | eqeq12d 2754 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑥 ·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧) ↔ (𝑦 ·ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧))) |
13 | 12 | cbvralvw 3383 |
. . . 4
⊢
(∀𝑥 ∈
ℋ (𝑥
·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧) ↔ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧)) |
14 | 13 | ralbii 3092 |
. . 3
⊢
(∀𝑧 ∈
ℋ ∀𝑥 ∈
ℋ (𝑥
·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧) ↔ ∀𝑧 ∈ ℋ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧)) |
15 | | fveq2 6774 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (𝑆‘𝑧) = (𝑆‘𝑥)) |
16 | 15 | oveq2d 7291 |
. . . . . 6
⊢ (𝑧 = 𝑥 → (𝑦 ·ih (𝑆‘𝑧)) = (𝑦 ·ih (𝑆‘𝑥))) |
17 | | oveq2 7283 |
. . . . . 6
⊢ (𝑧 = 𝑥 → ((𝑇‘𝑦) ·ih 𝑧) = ((𝑇‘𝑦) ·ih 𝑥)) |
18 | 16, 17 | eqeq12d 2754 |
. . . . 5
⊢ (𝑧 = 𝑥 → ((𝑦 ·ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧) ↔ (𝑦 ·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥))) |
19 | 18 | ralbidv 3112 |
. . . 4
⊢ (𝑧 = 𝑥 → (∀𝑦 ∈ ℋ (𝑦 ·ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧) ↔ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥))) |
20 | 19 | cbvralvw 3383 |
. . 3
⊢
(∀𝑧 ∈
ℋ ∀𝑦 ∈
ℋ (𝑦
·ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥)) |
21 | 8, 14, 20 | 3bitri 297 |
. 2
⊢
(∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥)) |
22 | | ffvelrn 6959 |
. . . . . . . . . . . 12
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) →
(𝑇‘𝑦) ∈ ℋ) |
23 | | ax-his1 29444 |
. . . . . . . . . . . 12
⊢ (((𝑇‘𝑦) ∈ ℋ ∧ 𝑥 ∈ ℋ) → ((𝑇‘𝑦) ·ih 𝑥) = (∗‘(𝑥
·ih (𝑇‘𝑦)))) |
24 | 22, 23 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) ∧
𝑥 ∈ ℋ) →
((𝑇‘𝑦)
·ih 𝑥) = (∗‘(𝑥 ·ih (𝑇‘𝑦)))) |
25 | 24 | adantrl 713 |
. . . . . . . . . 10
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) ∧
(𝑆: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ))
→ ((𝑇‘𝑦)
·ih 𝑥) = (∗‘(𝑥 ·ih (𝑇‘𝑦)))) |
26 | | ffvelrn 6959 |
. . . . . . . . . . . 12
⊢ ((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(𝑆‘𝑥) ∈ ℋ) |
27 | | ax-his1 29444 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℋ ∧ (𝑆‘𝑥) ∈ ℋ) → (𝑦 ·ih (𝑆‘𝑥)) = (∗‘((𝑆‘𝑥) ·ih 𝑦))) |
28 | 26, 27 | sylan2 593 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℋ ∧ (𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ)) →
(𝑦
·ih (𝑆‘𝑥)) = (∗‘((𝑆‘𝑥) ·ih 𝑦))) |
29 | 28 | adantll 711 |
. . . . . . . . . 10
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) ∧
(𝑆: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ))
→ (𝑦
·ih (𝑆‘𝑥)) = (∗‘((𝑆‘𝑥) ·ih 𝑦))) |
30 | 25, 29 | eqeq12d 2754 |
. . . . . . . . 9
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) ∧
(𝑆: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ))
→ (((𝑇‘𝑦)
·ih 𝑥) = (𝑦 ·ih (𝑆‘𝑥)) ↔ (∗‘(𝑥 ·ih (𝑇‘𝑦))) = (∗‘((𝑆‘𝑥) ·ih 𝑦)))) |
31 | 30 | ancoms 459 |
. . . . . . . 8
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑇: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ (((𝑇‘𝑦)
·ih 𝑥) = (𝑦 ·ih (𝑆‘𝑥)) ↔ (∗‘(𝑥 ·ih (𝑇‘𝑦))) = (∗‘((𝑆‘𝑥) ·ih 𝑦)))) |
32 | | hicl 29442 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑦) ∈ ℋ) → (𝑥 ·ih (𝑇‘𝑦)) ∈ ℂ) |
33 | 22, 32 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℋ ∧ (𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ)) →
(𝑥
·ih (𝑇‘𝑦)) ∈ ℂ) |
34 | 33 | adantll 711 |
. . . . . . . . 9
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑇: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ (𝑥
·ih (𝑇‘𝑦)) ∈ ℂ) |
35 | | hicl 29442 |
. . . . . . . . . . 11
⊢ (((𝑆‘𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑆‘𝑥) ·ih 𝑦) ∈
ℂ) |
36 | 26, 35 | sylan 580 |
. . . . . . . . . 10
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
𝑦 ∈ ℋ) →
((𝑆‘𝑥)
·ih 𝑦) ∈ ℂ) |
37 | 36 | adantrl 713 |
. . . . . . . . 9
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑇: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ ((𝑆‘𝑥)
·ih 𝑦) ∈ ℂ) |
38 | | cj11 14873 |
. . . . . . . . 9
⊢ (((𝑥
·ih (𝑇‘𝑦)) ∈ ℂ ∧ ((𝑆‘𝑥) ·ih 𝑦) ∈ ℂ) →
((∗‘(𝑥
·ih (𝑇‘𝑦))) = (∗‘((𝑆‘𝑥) ·ih 𝑦)) ↔ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦))) |
39 | 34, 37, 38 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑇: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ ((∗‘(𝑥
·ih (𝑇‘𝑦))) = (∗‘((𝑆‘𝑥) ·ih 𝑦)) ↔ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦))) |
40 | 31, 39 | bitr2d 279 |
. . . . . . 7
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑇: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ ((𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦) ↔ ((𝑇‘𝑦) ·ih 𝑥) = (𝑦 ·ih (𝑆‘𝑥)))) |
41 | 40 | an4s 657 |
. . . . . 6
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ ((𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦) ↔ ((𝑇‘𝑦) ·ih 𝑥) = (𝑦 ·ih (𝑆‘𝑥)))) |
42 | 41 | anassrs 468 |
. . . . 5
⊢ ((((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
∧ 𝑦 ∈ ℋ)
→ ((𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦) ↔ ((𝑇‘𝑦) ·ih 𝑥) = (𝑦 ·ih (𝑆‘𝑥)))) |
43 | | eqcom 2745 |
. . . . 5
⊢ (((𝑇‘𝑦) ·ih 𝑥) = (𝑦 ·ih (𝑆‘𝑥)) ↔ (𝑦 ·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥)) |
44 | 42, 43 | bitrdi 287 |
. . . 4
⊢ ((((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
∧ 𝑦 ∈ ℋ)
→ ((𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦) ↔ (𝑦 ·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥))) |
45 | 44 | ralbidva 3111 |
. . 3
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ (∀𝑦 ∈
ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦) ↔ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥))) |
46 | 45 | ralbidva 3111 |
. 2
⊢ ((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
→ (∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥))) |
47 | 21, 46 | bitr4id 290 |
1
⊢ ((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
→ (∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦))) |