| Step | Hyp | Ref
| Expression |
| 1 | | ralcom 3289 |
. . . 4
⊢
(∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦) ↔ ∀𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦)) |
| 2 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → (𝑆‘𝑧) = (𝑆‘𝑦)) |
| 3 | 2 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (𝑥 ·ih (𝑆‘𝑧)) = (𝑥 ·ih (𝑆‘𝑦))) |
| 4 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → ((𝑇‘𝑥) ·ih 𝑧) = ((𝑇‘𝑥) ·ih 𝑦)) |
| 5 | 3, 4 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑧 = 𝑦 → ((𝑥 ·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧) ↔ (𝑥 ·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦))) |
| 6 | 5 | ralbidv 3178 |
. . . . 5
⊢ (𝑧 = 𝑦 → (∀𝑥 ∈ ℋ (𝑥 ·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧) ↔ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦))) |
| 7 | 6 | cbvralvw 3237 |
. . . 4
⊢
(∀𝑧 ∈
ℋ ∀𝑥 ∈
ℋ (𝑥
·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧) ↔ ∀𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦)) |
| 8 | 1, 7 | bitr4i 278 |
. . 3
⊢
(∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦) ↔ ∀𝑧 ∈ ℋ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧)) |
| 9 | | oveq1 7438 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ·ih (𝑆‘𝑧)) = (𝑦 ·ih (𝑆‘𝑧))) |
| 10 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑇‘𝑥) = (𝑇‘𝑦)) |
| 11 | 10 | oveq1d 7446 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑇‘𝑥) ·ih 𝑧) = ((𝑇‘𝑦) ·ih 𝑧)) |
| 12 | 9, 11 | eqeq12d 2753 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑥 ·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧) ↔ (𝑦 ·ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧))) |
| 13 | 12 | cbvralvw 3237 |
. . . 4
⊢
(∀𝑥 ∈
ℋ (𝑥
·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧) ↔ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧)) |
| 14 | 13 | ralbii 3093 |
. . 3
⊢
(∀𝑧 ∈
ℋ ∀𝑥 ∈
ℋ (𝑥
·ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·ih 𝑧) ↔ ∀𝑧 ∈ ℋ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧)) |
| 15 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (𝑆‘𝑧) = (𝑆‘𝑥)) |
| 16 | 15 | oveq2d 7447 |
. . . . . 6
⊢ (𝑧 = 𝑥 → (𝑦 ·ih (𝑆‘𝑧)) = (𝑦 ·ih (𝑆‘𝑥))) |
| 17 | | oveq2 7439 |
. . . . . 6
⊢ (𝑧 = 𝑥 → ((𝑇‘𝑦) ·ih 𝑧) = ((𝑇‘𝑦) ·ih 𝑥)) |
| 18 | 16, 17 | eqeq12d 2753 |
. . . . 5
⊢ (𝑧 = 𝑥 → ((𝑦 ·ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧) ↔ (𝑦 ·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥))) |
| 19 | 18 | ralbidv 3178 |
. . . 4
⊢ (𝑧 = 𝑥 → (∀𝑦 ∈ ℋ (𝑦 ·ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧) ↔ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥))) |
| 20 | 19 | cbvralvw 3237 |
. . 3
⊢
(∀𝑧 ∈
ℋ ∀𝑦 ∈
ℋ (𝑦
·ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥)) |
| 21 | 8, 14, 20 | 3bitri 297 |
. 2
⊢
(∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥)) |
| 22 | | ffvelcdm 7101 |
. . . . . . . . . . . 12
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) →
(𝑇‘𝑦) ∈ ℋ) |
| 23 | | ax-his1 31101 |
. . . . . . . . . . . 12
⊢ (((𝑇‘𝑦) ∈ ℋ ∧ 𝑥 ∈ ℋ) → ((𝑇‘𝑦) ·ih 𝑥) = (∗‘(𝑥
·ih (𝑇‘𝑦)))) |
| 24 | 22, 23 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) ∧
𝑥 ∈ ℋ) →
((𝑇‘𝑦)
·ih 𝑥) = (∗‘(𝑥 ·ih (𝑇‘𝑦)))) |
| 25 | 24 | adantrl 716 |
. . . . . . . . . 10
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) ∧
(𝑆: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ))
→ ((𝑇‘𝑦)
·ih 𝑥) = (∗‘(𝑥 ·ih (𝑇‘𝑦)))) |
| 26 | | ffvelcdm 7101 |
. . . . . . . . . . . 12
⊢ ((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(𝑆‘𝑥) ∈ ℋ) |
| 27 | | ax-his1 31101 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℋ ∧ (𝑆‘𝑥) ∈ ℋ) → (𝑦 ·ih (𝑆‘𝑥)) = (∗‘((𝑆‘𝑥) ·ih 𝑦))) |
| 28 | 26, 27 | sylan2 593 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℋ ∧ (𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ)) →
(𝑦
·ih (𝑆‘𝑥)) = (∗‘((𝑆‘𝑥) ·ih 𝑦))) |
| 29 | 28 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) ∧
(𝑆: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ))
→ (𝑦
·ih (𝑆‘𝑥)) = (∗‘((𝑆‘𝑥) ·ih 𝑦))) |
| 30 | 25, 29 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) ∧
(𝑆: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ))
→ (((𝑇‘𝑦)
·ih 𝑥) = (𝑦 ·ih (𝑆‘𝑥)) ↔ (∗‘(𝑥 ·ih (𝑇‘𝑦))) = (∗‘((𝑆‘𝑥) ·ih 𝑦)))) |
| 31 | 30 | ancoms 458 |
. . . . . . . 8
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑇: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ (((𝑇‘𝑦)
·ih 𝑥) = (𝑦 ·ih (𝑆‘𝑥)) ↔ (∗‘(𝑥 ·ih (𝑇‘𝑦))) = (∗‘((𝑆‘𝑥) ·ih 𝑦)))) |
| 32 | | hicl 31099 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑦) ∈ ℋ) → (𝑥 ·ih (𝑇‘𝑦)) ∈ ℂ) |
| 33 | 22, 32 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℋ ∧ (𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ)) →
(𝑥
·ih (𝑇‘𝑦)) ∈ ℂ) |
| 34 | 33 | adantll 714 |
. . . . . . . . 9
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑇: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ (𝑥
·ih (𝑇‘𝑦)) ∈ ℂ) |
| 35 | | hicl 31099 |
. . . . . . . . . . 11
⊢ (((𝑆‘𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑆‘𝑥) ·ih 𝑦) ∈
ℂ) |
| 36 | 26, 35 | sylan 580 |
. . . . . . . . . 10
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
𝑦 ∈ ℋ) →
((𝑆‘𝑥)
·ih 𝑦) ∈ ℂ) |
| 37 | 36 | adantrl 716 |
. . . . . . . . 9
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑇: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ ((𝑆‘𝑥)
·ih 𝑦) ∈ ℂ) |
| 38 | | cj11 15201 |
. . . . . . . . 9
⊢ (((𝑥
·ih (𝑇‘𝑦)) ∈ ℂ ∧ ((𝑆‘𝑥) ·ih 𝑦) ∈ ℂ) →
((∗‘(𝑥
·ih (𝑇‘𝑦))) = (∗‘((𝑆‘𝑥) ·ih 𝑦)) ↔ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦))) |
| 39 | 34, 37, 38 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑇: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ ((∗‘(𝑥
·ih (𝑇‘𝑦))) = (∗‘((𝑆‘𝑥) ·ih 𝑦)) ↔ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦))) |
| 40 | 31, 39 | bitr2d 280 |
. . . . . . 7
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑇: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ))
→ ((𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦) ↔ ((𝑇‘𝑦) ·ih 𝑥) = (𝑦 ·ih (𝑆‘𝑥)))) |
| 41 | 40 | an4s 660 |
. . . . . 6
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ ((𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦) ↔ ((𝑇‘𝑦) ·ih 𝑥) = (𝑦 ·ih (𝑆‘𝑥)))) |
| 42 | 41 | anassrs 467 |
. . . . 5
⊢ ((((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
∧ 𝑦 ∈ ℋ)
→ ((𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦) ↔ ((𝑇‘𝑦) ·ih 𝑥) = (𝑦 ·ih (𝑆‘𝑥)))) |
| 43 | | eqcom 2744 |
. . . . 5
⊢ (((𝑇‘𝑦) ·ih 𝑥) = (𝑦 ·ih (𝑆‘𝑥)) ↔ (𝑦 ·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥)) |
| 44 | 42, 43 | bitrdi 287 |
. . . 4
⊢ ((((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
∧ 𝑦 ∈ ℋ)
→ ((𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦) ↔ (𝑦 ·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥))) |
| 45 | 44 | ralbidva 3176 |
. . 3
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ (∀𝑦 ∈
ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦) ↔ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥))) |
| 46 | 45 | ralbidva 3176 |
. 2
⊢ ((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
→ (∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·ih 𝑥))) |
| 47 | 21, 46 | bitr4id 290 |
1
⊢ ((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
→ (∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦))) |