Step | Hyp | Ref
| Expression |
1 | | hmopf 29987 |
. . 3
⊢ (𝑇 ∈ HrmOp → 𝑇: ℋ⟶
ℋ) |
2 | | hmopf 29987 |
. . 3
⊢ (𝑈 ∈ HrmOp → 𝑈: ℋ⟶
ℋ) |
3 | | hoaddcl 29871 |
. . 3
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
→ (𝑇 +op
𝑈): ℋ⟶
ℋ) |
4 | 1, 2, 3 | syl2an 599 |
. 2
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 +op 𝑈): ℋ⟶
ℋ) |
5 | | hmop 30035 |
. . . . . . 7
⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥
·ih (𝑇‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦)) |
6 | 5 | 3expb 1122 |
. . . . . 6
⊢ ((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥
·ih (𝑇‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦)) |
7 | | hmop 30035 |
. . . . . . 7
⊢ ((𝑈 ∈ HrmOp ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥
·ih (𝑈‘𝑦)) = ((𝑈‘𝑥) ·ih 𝑦)) |
8 | 7 | 3expb 1122 |
. . . . . 6
⊢ ((𝑈 ∈ HrmOp ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥
·ih (𝑈‘𝑦)) = ((𝑈‘𝑥) ·ih 𝑦)) |
9 | 6, 8 | oveqan12d 7254 |
. . . . 5
⊢ (((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) ∧ (𝑈 ∈ HrmOp ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ))) →
((𝑥
·ih (𝑇‘𝑦)) + (𝑥 ·ih (𝑈‘𝑦))) = (((𝑇‘𝑥) ·ih 𝑦) + ((𝑈‘𝑥) ·ih 𝑦))) |
10 | 9 | anandirs 679 |
. . . 4
⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝑥
·ih (𝑇‘𝑦)) + (𝑥 ·ih (𝑈‘𝑦))) = (((𝑇‘𝑥) ·ih 𝑦) + ((𝑈‘𝑥) ·ih 𝑦))) |
11 | 1, 2 | anim12i 616 |
. . . . 5
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶
ℋ)) |
12 | | hosval 29853 |
. . . . . . . . 9
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ)
→ ((𝑇 +op
𝑈)‘𝑦) = ((𝑇‘𝑦) +ℎ (𝑈‘𝑦))) |
13 | 12 | oveq2d 7251 |
. . . . . . . 8
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ)
→ (𝑥
·ih ((𝑇 +op 𝑈)‘𝑦)) = (𝑥 ·ih ((𝑇‘𝑦) +ℎ (𝑈‘𝑦)))) |
14 | 13 | 3expa 1120 |
. . . . . . 7
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑦 ∈ ℋ)
→ (𝑥
·ih ((𝑇 +op 𝑈)‘𝑦)) = (𝑥 ·ih ((𝑇‘𝑦) +ℎ (𝑈‘𝑦)))) |
15 | 14 | adantrl 716 |
. . . . . 6
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (𝑥
·ih ((𝑇 +op 𝑈)‘𝑦)) = (𝑥 ·ih ((𝑇‘𝑦) +ℎ (𝑈‘𝑦)))) |
16 | | simprl 771 |
. . . . . . 7
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ 𝑥 ∈
ℋ) |
17 | | ffvelrn 6924 |
. . . . . . . 8
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) →
(𝑇‘𝑦) ∈ ℋ) |
18 | 17 | ad2ant2rl 749 |
. . . . . . 7
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (𝑇‘𝑦) ∈
ℋ) |
19 | | ffvelrn 6924 |
. . . . . . . 8
⊢ ((𝑈: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) →
(𝑈‘𝑦) ∈ ℋ) |
20 | 19 | ad2ant2l 746 |
. . . . . . 7
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (𝑈‘𝑦) ∈
ℋ) |
21 | | his7 29203 |
. . . . . . 7
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑦) ∈ ℋ ∧ (𝑈‘𝑦) ∈ ℋ) → (𝑥 ·ih ((𝑇‘𝑦) +ℎ (𝑈‘𝑦))) = ((𝑥 ·ih (𝑇‘𝑦)) + (𝑥 ·ih (𝑈‘𝑦)))) |
22 | 16, 18, 20, 21 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (𝑥
·ih ((𝑇‘𝑦) +ℎ (𝑈‘𝑦))) = ((𝑥 ·ih (𝑇‘𝑦)) + (𝑥 ·ih (𝑈‘𝑦)))) |
23 | 15, 22 | eqtrd 2779 |
. . . . 5
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (𝑥
·ih ((𝑇 +op 𝑈)‘𝑦)) = ((𝑥 ·ih (𝑇‘𝑦)) + (𝑥 ·ih (𝑈‘𝑦)))) |
24 | 11, 23 | sylan 583 |
. . . 4
⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥
·ih ((𝑇 +op 𝑈)‘𝑦)) = ((𝑥 ·ih (𝑇‘𝑦)) + (𝑥 ·ih (𝑈‘𝑦)))) |
25 | | hosval 29853 |
. . . . . . . . 9
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ)
→ ((𝑇 +op
𝑈)‘𝑥) = ((𝑇‘𝑥) +ℎ (𝑈‘𝑥))) |
26 | 25 | oveq1d 7250 |
. . . . . . . 8
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ)
→ (((𝑇 +op
𝑈)‘𝑥) ·ih 𝑦) = (((𝑇‘𝑥) +ℎ (𝑈‘𝑥)) ·ih 𝑦)) |
27 | 26 | 3expa 1120 |
. . . . . . 7
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ (((𝑇 +op
𝑈)‘𝑥) ·ih 𝑦) = (((𝑇‘𝑥) +ℎ (𝑈‘𝑥)) ·ih 𝑦)) |
28 | 27 | adantrr 717 |
. . . . . 6
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (((𝑇 +op
𝑈)‘𝑥) ·ih 𝑦) = (((𝑇‘𝑥) +ℎ (𝑈‘𝑥)) ·ih 𝑦)) |
29 | | ffvelrn 6924 |
. . . . . . . 8
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(𝑇‘𝑥) ∈ ℋ) |
30 | 29 | ad2ant2r 747 |
. . . . . . 7
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (𝑇‘𝑥) ∈
ℋ) |
31 | | ffvelrn 6924 |
. . . . . . . 8
⊢ ((𝑈: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(𝑈‘𝑥) ∈ ℋ) |
32 | 31 | ad2ant2lr 748 |
. . . . . . 7
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (𝑈‘𝑥) ∈
ℋ) |
33 | | simprr 773 |
. . . . . . 7
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ 𝑦 ∈
ℋ) |
34 | | ax-his2 29196 |
. . . . . . 7
⊢ (((𝑇‘𝑥) ∈ ℋ ∧ (𝑈‘𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑇‘𝑥) +ℎ (𝑈‘𝑥)) ·ih 𝑦) = (((𝑇‘𝑥) ·ih 𝑦) + ((𝑈‘𝑥) ·ih 𝑦))) |
35 | 30, 32, 33, 34 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (((𝑇‘𝑥) +ℎ (𝑈‘𝑥)) ·ih 𝑦) = (((𝑇‘𝑥) ·ih 𝑦) + ((𝑈‘𝑥) ·ih 𝑦))) |
36 | 28, 35 | eqtrd 2779 |
. . . . 5
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ (𝑥 ∈ ℋ
∧ 𝑦 ∈ ℋ))
→ (((𝑇 +op
𝑈)‘𝑥) ·ih 𝑦) = (((𝑇‘𝑥) ·ih 𝑦) + ((𝑈‘𝑥) ·ih 𝑦))) |
37 | 11, 36 | sylan 583 |
. . . 4
⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) →
(((𝑇 +op 𝑈)‘𝑥) ·ih 𝑦) = (((𝑇‘𝑥) ·ih 𝑦) + ((𝑈‘𝑥) ·ih 𝑦))) |
38 | 10, 24, 37 | 3eqtr4d 2789 |
. . 3
⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥
·ih ((𝑇 +op 𝑈)‘𝑦)) = (((𝑇 +op 𝑈)‘𝑥) ·ih 𝑦)) |
39 | 38 | ralrimivva 3115 |
. 2
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) →
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih ((𝑇 +op 𝑈)‘𝑦)) = (((𝑇 +op 𝑈)‘𝑥) ·ih 𝑦)) |
40 | | elhmop 29986 |
. 2
⊢ ((𝑇 +op 𝑈) ∈ HrmOp ↔ ((𝑇 +op 𝑈): ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih ((𝑇 +op 𝑈)‘𝑦)) = (((𝑇 +op 𝑈)‘𝑥) ·ih 𝑦))) |
41 | 4, 39, 40 | sylanbrc 586 |
1
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 +op 𝑈) ∈ HrmOp) |