Step | Hyp | Ref
| Expression |
1 | | ffvelrn 6721 |
. . . . . . . . . . . 12
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) →
(𝑇‘𝑦) ∈ ℋ) |
2 | | ax-his1 28546 |
. . . . . . . . . . . 12
⊢ (((𝑇‘𝑦) ∈ ℋ ∧ 𝑥 ∈ ℋ) → ((𝑇‘𝑦) ·ih 𝑥) = (∗‘(𝑥
·ih (𝑇‘𝑦)))) |
3 | 1, 2 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) ∧
𝑥 ∈ ℋ) →
((𝑇‘𝑦)
·ih 𝑥) = (∗‘(𝑥 ·ih (𝑇‘𝑦)))) |
4 | 3 | adantrl 712 |
. . . . . . . . . 10
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) ∧
(𝑆: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ))
→ ((𝑇‘𝑦)
·ih 𝑥) = (∗‘(𝑥 ·ih (𝑇‘𝑦)))) |
5 | | ffvelrn 6721 |
. . . . . . . . . . . 12
⊢ ((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(𝑆‘𝑥) ∈ ℋ) |
6 | | ax-his1 28546 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℋ ∧ (𝑆‘𝑥) ∈ ℋ) → (𝑦 ·ih (𝑆‘𝑥)) = (∗‘((𝑆‘𝑥) ·ih 𝑦))) |
7 | 5, 6 | sylan2 592 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℋ ∧ (𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ)) →
(𝑦
·ih (𝑆‘𝑥)) = (∗‘((𝑆‘𝑥) ·ih 𝑦))) |
8 | 7 | adantll 710 |
. . . . . . . . . 10
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) ∧
(𝑆: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ))
→ (𝑦
·ih (𝑆‘𝑥)) = (∗‘((𝑆‘𝑥) ·ih 𝑦))) |
9 | 4, 8 | eqeq12d 2812 |
. . . . . . . . 9
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) ∧
(𝑆: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ))
→ (((𝑇‘𝑦)
·ih 𝑥) = (𝑦 ·ih (𝑆‘𝑥)) ↔ (∗‘(𝑥 ·ih (𝑇‘𝑦))) = (∗‘((𝑆‘𝑥) ·ih 𝑦)))) |
10 | 9 | ancoms 459 |
. . . . . . . 8
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑇: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ (((𝑇‘𝑦)
·ih 𝑥) = (𝑦 ·ih (𝑆‘𝑥)) ↔ (∗‘(𝑥 ·ih (𝑇‘𝑦))) = (∗‘((𝑆‘𝑥) ·ih 𝑦)))) |
11 | | hicl 28544 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑦) ∈ ℋ) → (𝑥 ·ih (𝑇‘𝑦)) ∈ ℂ) |
12 | 1, 11 | sylan2 592 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℋ ∧ (𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ)) →
(𝑥
·ih (𝑇‘𝑦)) ∈ ℂ) |
13 | 12 | adantll 710 |
. . . . . . . . 9
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑇: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ (𝑥
·ih (𝑇‘𝑦)) ∈ ℂ) |
14 | | hicl 28544 |
. . . . . . . . . . 11
⊢ (((𝑆‘𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑆‘𝑥) ·ih 𝑦) ∈
ℂ) |
15 | 5, 14 | sylan 580 |
. . . . . . . . . 10
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
𝑦 ∈ ℋ) →
((𝑆‘𝑥)
·ih 𝑦) ∈ ℂ) |
16 | 15 | adantrl 712 |
. . . . . . . . 9
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑇: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ ((𝑆‘𝑥)
·ih 𝑦) ∈ ℂ) |
17 | | cj11 14359 |
. . . . . . . . 9
⊢ (((𝑥
·ih (𝑇‘𝑦)) ∈ ℂ ∧ ((𝑆‘𝑥) ·ih 𝑦) ∈ ℂ) →
((∗‘(𝑥
·ih (𝑇‘𝑦))) = (∗‘((𝑆‘𝑥) ·ih 𝑦)) ↔ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦))) |
18 | 13, 16, 17 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑇: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ ((∗‘(𝑥
·ih (𝑇‘𝑦))) = (∗‘((𝑆‘𝑥) ·ih 𝑦)) ↔ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦))) |
19 | 10, 18 | bitr2d 281 |
. . . . . . 7
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑇: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ ((𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦) ↔ ((𝑇‘𝑦) ·ih 𝑥) = (𝑦 ·ih (𝑆‘𝑥)))) |
20 | 19 | an4s 656 |
. . . . . 6
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ ((𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦) ↔ ((𝑇‘𝑦) ·ih 𝑥) = (𝑦 ·ih (𝑆‘𝑥)))) |
21 | 20 | anassrs 468 |
. . . . 5
⊢ ((((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
∧ 𝑦 ∈ ℋ)
→ ((𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦) ↔ ((𝑇‘𝑦) ·ih 𝑥) = (𝑦 ·ih (𝑆‘𝑥)))) |
22 | | eqcom 2804 |
. . . . 5
⊢ (((𝑇‘𝑦) ·ih 𝑥) = (𝑦 ·ih (𝑆‘𝑥)) ↔ (𝑦 ·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥)) |
23 | 21, 22 | syl6bb 288 |
. . . 4
⊢ ((((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
∧ 𝑦 ∈ ℋ)
→ ((𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦) ↔ (𝑦 ·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥))) |
24 | 23 | ralbidva 3165 |
. . 3
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ (∀𝑦 ∈
ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦) ↔ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥))) |
25 | 24 | ralbidva 3165 |
. 2
⊢ ((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
→ (∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥))) |
26 | | ralcom 3317 |
. . . 4
⊢
(∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦) ↔ ∀𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦)) |
27 | | fveq2 6545 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → (𝑆‘𝑧) = (𝑆‘𝑦)) |
28 | 27 | oveq2d 7039 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (𝑥 ·ih (𝑆‘𝑧)) = (𝑥 ·ih (𝑆‘𝑦))) |
29 | | oveq2 7031 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → ((𝑇‘𝑥) ·ih 𝑧) = ((𝑇‘𝑥) ·ih 𝑦)) |
30 | 28, 29 | eqeq12d 2812 |
. . . . . 6
⊢ (𝑧 = 𝑦 → ((𝑥 ·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧) ↔ (𝑥 ·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦))) |
31 | 30 | ralbidv 3166 |
. . . . 5
⊢ (𝑧 = 𝑦 → (∀𝑥 ∈ ℋ (𝑥 ·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧) ↔ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦))) |
32 | 31 | cbvralv 3405 |
. . . 4
⊢
(∀𝑧 ∈
ℋ ∀𝑥 ∈
ℋ (𝑥
·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧) ↔ ∀𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦)) |
33 | 26, 32 | bitr4i 279 |
. . 3
⊢
(∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦) ↔ ∀𝑧 ∈ ℋ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧)) |
34 | | oveq1 7030 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ·ih (𝑆‘𝑧)) = (𝑦 ·ih (𝑆‘𝑧))) |
35 | | fveq2 6545 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑇‘𝑥) = (𝑇‘𝑦)) |
36 | 35 | oveq1d 7038 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑇‘𝑥) ·ih 𝑧) = ((𝑇‘𝑦) ·ih 𝑧)) |
37 | 34, 36 | eqeq12d 2812 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑥 ·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧) ↔ (𝑦 ·ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧))) |
38 | 37 | cbvralv 3405 |
. . . 4
⊢
(∀𝑥 ∈
ℋ (𝑥
·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧) ↔ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧)) |
39 | 38 | ralbii 3134 |
. . 3
⊢
(∀𝑧 ∈
ℋ ∀𝑥 ∈
ℋ (𝑥
·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧) ↔ ∀𝑧 ∈ ℋ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧)) |
40 | | fveq2 6545 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (𝑆‘𝑧) = (𝑆‘𝑥)) |
41 | 40 | oveq2d 7039 |
. . . . . 6
⊢ (𝑧 = 𝑥 → (𝑦 ·ih (𝑆‘𝑧)) = (𝑦 ·ih (𝑆‘𝑥))) |
42 | | oveq2 7031 |
. . . . . 6
⊢ (𝑧 = 𝑥 → ((𝑇‘𝑦) ·ih 𝑧) = ((𝑇‘𝑦) ·ih 𝑥)) |
43 | 41, 42 | eqeq12d 2812 |
. . . . 5
⊢ (𝑧 = 𝑥 → ((𝑦 ·ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧) ↔ (𝑦 ·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥))) |
44 | 43 | ralbidv 3166 |
. . . 4
⊢ (𝑧 = 𝑥 → (∀𝑦 ∈ ℋ (𝑦 ·ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧) ↔ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥))) |
45 | 44 | cbvralv 3405 |
. . 3
⊢
(∀𝑧 ∈
ℋ ∀𝑦 ∈
ℋ (𝑦
·ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥)) |
46 | 33, 39, 45 | 3bitri 298 |
. 2
⊢
(∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥)) |
47 | 25, 46 | syl6rbbr 291 |
1
⊢ ((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
→ (∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦))) |