| Step | Hyp | Ref
| Expression |
| 1 | | hmopf 31893 |
. . 3
⊢ (𝑇 ∈ HrmOp → 𝑇: ℋ⟶
ℋ) |
| 2 | | hmopf 31893 |
. . 3
⊢ (𝑈 ∈ HrmOp → 𝑈: ℋ⟶
ℋ) |
| 3 | | hoaddcl 31777 |
. . 3
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
→ (𝑇 +op
𝑈): ℋ⟶
ℋ) |
| 4 | 1, 2, 3 | syl2an 596 |
. 2
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 +op 𝑈): ℋ⟶
ℋ) |
| 5 | | hmop 31941 |
. . . . . . 7
⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥
·ih (𝑇‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦)) |
| 6 | 5 | 3expb 1121 |
. . . . . 6
⊢ ((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥
·ih (𝑇‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦)) |
| 7 | | hmop 31941 |
. . . . . . 7
⊢ ((𝑈 ∈ HrmOp ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥
·ih (𝑈‘𝑦)) = ((𝑈‘𝑥) ·ih 𝑦)) |
| 8 | 7 | 3expb 1121 |
. . . . . 6
⊢ ((𝑈 ∈ HrmOp ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥
·ih (𝑈‘𝑦)) = ((𝑈‘𝑥) ·ih 𝑦)) |
| 9 | 6, 8 | oveqan12d 7450 |
. . . . 5
⊢ (((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) ∧ (𝑈 ∈ HrmOp ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ))) →
((𝑥
·ih (𝑇‘𝑦)) + (𝑥 ·ih (𝑈‘𝑦))) = (((𝑇‘𝑥) ·ih 𝑦) + ((𝑈‘𝑥) ·ih 𝑦))) |
| 10 | 9 | anandirs 679 |
. . . 4
⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝑥
·ih (𝑇‘𝑦)) + (𝑥 ·ih (𝑈‘𝑦))) = (((𝑇‘𝑥) ·ih 𝑦) + ((𝑈‘𝑥) ·ih 𝑦))) |
| 11 | 1, 2 | anim12i 613 |
. . . . 5
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶
ℋ)) |
| 12 | | hosval 31759 |
. . . . . . . . 9
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ)
→ ((𝑇 +op
𝑈)‘𝑦) = ((𝑇‘𝑦) +ℎ (𝑈‘𝑦))) |
| 13 | 12 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ)
→ (𝑥
·ih ((𝑇 +op 𝑈)‘𝑦)) = (𝑥 ·ih ((𝑇‘𝑦) +ℎ (𝑈‘𝑦)))) |
| 14 | 13 | 3expa 1119 |
. . . . . . 7
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑦 ∈ ℋ)
→ (𝑥
·ih ((𝑇 +op 𝑈)‘𝑦)) = (𝑥 ·ih ((𝑇‘𝑦) +ℎ (𝑈‘𝑦)))) |
| 15 | 14 | adantrl 716 |
. . . . . 6
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (𝑥
·ih ((𝑇 +op 𝑈)‘𝑦)) = (𝑥 ·ih ((𝑇‘𝑦) +ℎ (𝑈‘𝑦)))) |
| 16 | | simprl 771 |
. . . . . . 7
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ 𝑥 ∈
ℋ) |
| 17 | | ffvelcdm 7101 |
. . . . . . . 8
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) →
(𝑇‘𝑦) ∈ ℋ) |
| 18 | 17 | ad2ant2rl 749 |
. . . . . . 7
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (𝑇‘𝑦) ∈
ℋ) |
| 19 | | ffvelcdm 7101 |
. . . . . . . 8
⊢ ((𝑈: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) →
(𝑈‘𝑦) ∈ ℋ) |
| 20 | 19 | ad2ant2l 746 |
. . . . . . 7
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (𝑈‘𝑦) ∈
ℋ) |
| 21 | | his7 31109 |
. . . . . . 7
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑦) ∈ ℋ ∧ (𝑈‘𝑦) ∈ ℋ) → (𝑥 ·ih ((𝑇‘𝑦) +ℎ (𝑈‘𝑦))) = ((𝑥 ·ih (𝑇‘𝑦)) + (𝑥 ·ih (𝑈‘𝑦)))) |
| 22 | 16, 18, 20, 21 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (𝑥
·ih ((𝑇‘𝑦) +ℎ (𝑈‘𝑦))) = ((𝑥 ·ih (𝑇‘𝑦)) + (𝑥 ·ih (𝑈‘𝑦)))) |
| 23 | 15, 22 | eqtrd 2777 |
. . . . 5
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (𝑥
·ih ((𝑇 +op 𝑈)‘𝑦)) = ((𝑥 ·ih (𝑇‘𝑦)) + (𝑥 ·ih (𝑈‘𝑦)))) |
| 24 | 11, 23 | sylan 580 |
. . . 4
⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥
·ih ((𝑇 +op 𝑈)‘𝑦)) = ((𝑥 ·ih (𝑇‘𝑦)) + (𝑥 ·ih (𝑈‘𝑦)))) |
| 25 | | hosval 31759 |
. . . . . . . . 9
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ)
→ ((𝑇 +op
𝑈)‘𝑥) = ((𝑇‘𝑥) +ℎ (𝑈‘𝑥))) |
| 26 | 25 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ)
→ (((𝑇 +op
𝑈)‘𝑥) ·ih 𝑦) = (((𝑇‘𝑥) +ℎ (𝑈‘𝑥)) ·ih 𝑦)) |
| 27 | 26 | 3expa 1119 |
. . . . . . 7
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ (((𝑇 +op
𝑈)‘𝑥) ·ih 𝑦) = (((𝑇‘𝑥) +ℎ (𝑈‘𝑥)) ·ih 𝑦)) |
| 28 | 27 | adantrr 717 |
. . . . . 6
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (((𝑇 +op
𝑈)‘𝑥) ·ih 𝑦) = (((𝑇‘𝑥) +ℎ (𝑈‘𝑥)) ·ih 𝑦)) |
| 29 | | ffvelcdm 7101 |
. . . . . . . 8
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(𝑇‘𝑥) ∈ ℋ) |
| 30 | 29 | ad2ant2r 747 |
. . . . . . 7
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (𝑇‘𝑥) ∈
ℋ) |
| 31 | | ffvelcdm 7101 |
. . . . . . . 8
⊢ ((𝑈: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(𝑈‘𝑥) ∈ ℋ) |
| 32 | 31 | ad2ant2lr 748 |
. . . . . . 7
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (𝑈‘𝑥) ∈
ℋ) |
| 33 | | simprr 773 |
. . . . . . 7
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ 𝑦 ∈
ℋ) |
| 34 | | ax-his2 31102 |
. . . . . . 7
⊢ (((𝑇‘𝑥) ∈ ℋ ∧ (𝑈‘𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑇‘𝑥) +ℎ (𝑈‘𝑥)) ·ih 𝑦) = (((𝑇‘𝑥) ·ih 𝑦) + ((𝑈‘𝑥) ·ih 𝑦))) |
| 35 | 30, 32, 33, 34 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (((𝑇‘𝑥) +ℎ (𝑈‘𝑥)) ·ih 𝑦) = (((𝑇‘𝑥) ·ih 𝑦) + ((𝑈‘𝑥) ·ih 𝑦))) |
| 36 | 28, 35 | eqtrd 2777 |
. . . . 5
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (((𝑇 +op
𝑈)‘𝑥) ·ih 𝑦) = (((𝑇‘𝑥) ·ih 𝑦) + ((𝑈‘𝑥) ·ih 𝑦))) |
| 37 | 11, 36 | sylan 580 |
. . . 4
⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) →
(((𝑇 +op 𝑈)‘𝑥) ·ih 𝑦) = (((𝑇‘𝑥) ·ih 𝑦) + ((𝑈‘𝑥) ·ih 𝑦))) |
| 38 | 10, 24, 37 | 3eqtr4d 2787 |
. . 3
⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥
·ih ((𝑇 +op 𝑈)‘𝑦)) = (((𝑇 +op 𝑈)‘𝑥) ·ih 𝑦)) |
| 39 | 38 | ralrimivva 3202 |
. 2
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) →
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih ((𝑇 +op 𝑈)‘𝑦)) = (((𝑇 +op 𝑈)‘𝑥) ·ih 𝑦)) |
| 40 | | elhmop 31892 |
. 2
⊢ ((𝑇 +op 𝑈) ∈ HrmOp ↔ ((𝑇 +op 𝑈): ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih ((𝑇 +op 𝑈)‘𝑦)) = (((𝑇 +op 𝑈)‘𝑥) ·ih 𝑦))) |
| 41 | 4, 39, 40 | sylanbrc 583 |
1
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 +op 𝑈) ∈ HrmOp) |