| Step | Hyp | Ref
| Expression |
| 1 | | hmopf 31893 |
. 2
⊢ (𝑇 ∈ HrmOp → 𝑇: ℋ⟶
ℋ) |
| 2 | | simplll 775 |
. . . . . . . 8
⊢ ((((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → 𝑇 ∈ HrmOp) |
| 3 | | hvmulcl 31032 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑥
·ℎ 𝑦) ∈ ℋ) |
| 4 | | hvaddcl 31031 |
. . . . . . . . . . 11
⊢ (((𝑥
·ℎ 𝑦) ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑥 ·ℎ 𝑦) +ℎ 𝑧) ∈
ℋ) |
| 5 | 3, 4 | sylan 580 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑥
·ℎ 𝑦) +ℎ 𝑧) ∈ ℋ) |
| 6 | 5 | adantll 714 |
. . . . . . . . 9
⊢ (((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) → ((𝑥
·ℎ 𝑦) +ℎ 𝑧) ∈ ℋ) |
| 7 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → ((𝑥
·ℎ 𝑦) +ℎ 𝑧) ∈ ℋ) |
| 8 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → 𝑤 ∈
ℋ) |
| 9 | | hmop 31941 |
. . . . . . . . 9
⊢ ((𝑇 ∈ HrmOp ∧ ((𝑥
·ℎ 𝑦) +ℎ 𝑧) ∈ ℋ ∧ 𝑤 ∈ ℋ) → (((𝑥 ·ℎ 𝑦) +ℎ 𝑧)
·ih (𝑇‘𝑤)) = ((𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧))
·ih 𝑤)) |
| 10 | 9 | eqcomd 2743 |
. . . . . . . 8
⊢ ((𝑇 ∈ HrmOp ∧ ((𝑥
·ℎ 𝑦) +ℎ 𝑧) ∈ ℋ ∧ 𝑤 ∈ ℋ) → ((𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧))
·ih 𝑤) = (((𝑥 ·ℎ 𝑦) +ℎ 𝑧)
·ih (𝑇‘𝑤))) |
| 11 | 2, 7, 8, 10 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → ((𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧))
·ih 𝑤) = (((𝑥 ·ℎ 𝑦) +ℎ 𝑧)
·ih (𝑇‘𝑤))) |
| 12 | | simprl 771 |
. . . . . . . . 9
⊢ ((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → 𝑥 ∈
ℂ) |
| 13 | 12 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → 𝑥 ∈
ℂ) |
| 14 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → 𝑦 ∈
ℋ) |
| 15 | 14 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → 𝑦 ∈
ℋ) |
| 16 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → 𝑧 ∈
ℋ) |
| 17 | 1 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ HrmOp ∧ 𝑤 ∈ ℋ) → (𝑇‘𝑤) ∈ ℋ) |
| 18 | 17 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝑇 ∈ HrmOp ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → (𝑇‘𝑤) ∈ ℋ) |
| 19 | 18 | adantllr 719 |
. . . . . . . 8
⊢ ((((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → (𝑇‘𝑤) ∈ ℋ) |
| 20 | | hiassdi 31110 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ (𝑇‘𝑤) ∈ ℋ)) → (((𝑥
·ℎ 𝑦) +ℎ 𝑧) ·ih (𝑇‘𝑤)) = ((𝑥 · (𝑦 ·ih (𝑇‘𝑤))) + (𝑧 ·ih (𝑇‘𝑤)))) |
| 21 | 13, 15, 16, 19, 20 | syl22anc 839 |
. . . . . . 7
⊢ ((((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → (((𝑥
·ℎ 𝑦) +ℎ 𝑧) ·ih (𝑇‘𝑤)) = ((𝑥 · (𝑦 ·ih (𝑇‘𝑤))) + (𝑧 ·ih (𝑇‘𝑤)))) |
| 22 | 1 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ HrmOp ∧ 𝑦 ∈ ℋ) → (𝑇‘𝑦) ∈ ℋ) |
| 23 | 22 | adantrl 716 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → (𝑇‘𝑦) ∈ ℋ) |
| 24 | 23 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → (𝑇‘𝑦) ∈ ℋ) |
| 25 | 1 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ HrmOp ∧ 𝑧 ∈ ℋ) → (𝑇‘𝑧) ∈ ℋ) |
| 26 | 25 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑇 ∈ HrmOp ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → (𝑇‘𝑧) ∈ ℋ) |
| 27 | 26 | adantllr 719 |
. . . . . . . . 9
⊢ ((((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → (𝑇‘𝑧) ∈ ℋ) |
| 28 | | hiassdi 31110 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℂ ∧ (𝑇‘𝑦) ∈ ℋ) ∧ ((𝑇‘𝑧) ∈ ℋ ∧ 𝑤 ∈ ℋ)) → (((𝑥
·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧)) ·ih 𝑤) = ((𝑥 · ((𝑇‘𝑦) ·ih 𝑤)) + ((𝑇‘𝑧) ·ih 𝑤))) |
| 29 | 13, 24, 27, 8, 28 | syl22anc 839 |
. . . . . . . 8
⊢ ((((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → (((𝑥
·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧)) ·ih 𝑤) = ((𝑥 · ((𝑇‘𝑦) ·ih 𝑤)) + ((𝑇‘𝑧) ·ih 𝑤))) |
| 30 | | hmop 31941 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 ∈ HrmOp ∧ 𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ) → (𝑦
·ih (𝑇‘𝑤)) = ((𝑇‘𝑦) ·ih 𝑤)) |
| 31 | 30 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ HrmOp ∧ 𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ) → ((𝑇‘𝑦) ·ih 𝑤) = (𝑦 ·ih (𝑇‘𝑤))) |
| 32 | 31 | 3expa 1119 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ HrmOp ∧ 𝑦 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → ((𝑇‘𝑦) ·ih 𝑤) = (𝑦 ·ih (𝑇‘𝑤))) |
| 33 | 32 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ HrmOp ∧ 𝑦 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → (𝑥 · ((𝑇‘𝑦) ·ih 𝑤)) = (𝑥 · (𝑦 ·ih (𝑇‘𝑤)))) |
| 34 | 33 | adantlrl 720 |
. . . . . . . . . 10
⊢ (((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑤 ∈ ℋ) → (𝑥 · ((𝑇‘𝑦) ·ih 𝑤)) = (𝑥 · (𝑦 ·ih (𝑇‘𝑤)))) |
| 35 | 34 | adantlr 715 |
. . . . . . . . 9
⊢ ((((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → (𝑥 · ((𝑇‘𝑦) ·ih 𝑤)) = (𝑥 · (𝑦 ·ih (𝑇‘𝑤)))) |
| 36 | | hmop 31941 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ HrmOp ∧ 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ) → (𝑧
·ih (𝑇‘𝑤)) = ((𝑇‘𝑧) ·ih 𝑤)) |
| 37 | 36 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ HrmOp ∧ 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ) → ((𝑇‘𝑧) ·ih 𝑤) = (𝑧 ·ih (𝑇‘𝑤))) |
| 38 | 37 | 3expa 1119 |
. . . . . . . . . 10
⊢ (((𝑇 ∈ HrmOp ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → ((𝑇‘𝑧) ·ih 𝑤) = (𝑧 ·ih (𝑇‘𝑤))) |
| 39 | 38 | adantllr 719 |
. . . . . . . . 9
⊢ ((((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → ((𝑇‘𝑧) ·ih 𝑤) = (𝑧 ·ih (𝑇‘𝑤))) |
| 40 | 35, 39 | oveq12d 7449 |
. . . . . . . 8
⊢ ((((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → ((𝑥 · ((𝑇‘𝑦) ·ih 𝑤)) + ((𝑇‘𝑧) ·ih 𝑤)) = ((𝑥 · (𝑦 ·ih (𝑇‘𝑤))) + (𝑧 ·ih (𝑇‘𝑤)))) |
| 41 | 29, 40 | eqtr2d 2778 |
. . . . . . 7
⊢ ((((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → ((𝑥 · (𝑦 ·ih (𝑇‘𝑤))) + (𝑧 ·ih (𝑇‘𝑤))) = (((𝑥 ·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧)) ·ih 𝑤)) |
| 42 | 11, 21, 41 | 3eqtrd 2781 |
. . . . . 6
⊢ ((((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → ((𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧))
·ih 𝑤) = (((𝑥 ·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧)) ·ih 𝑤)) |
| 43 | 42 | ralrimiva 3146 |
. . . . 5
⊢ (((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) →
∀𝑤 ∈ ℋ
((𝑇‘((𝑥
·ℎ 𝑦) +ℎ 𝑧)) ·ih 𝑤) = (((𝑥 ·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧)) ·ih 𝑤)) |
| 44 | | ffvelcdm 7101 |
. . . . . . . . 9
⊢ ((𝑇: ℋ⟶ ℋ ∧
((𝑥
·ℎ 𝑦) +ℎ 𝑧) ∈ ℋ) → (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) ∈
ℋ) |
| 45 | 5, 44 | sylan2 593 |
. . . . . . . 8
⊢ ((𝑇: ℋ⟶ ℋ ∧
((𝑥 ∈ ℂ ∧
𝑦 ∈ ℋ) ∧
𝑧 ∈ ℋ)) →
(𝑇‘((𝑥
·ℎ 𝑦) +ℎ 𝑧)) ∈ ℋ) |
| 46 | 45 | anassrs 467 |
. . . . . . 7
⊢ (((𝑇: ℋ⟶ ℋ ∧
(𝑥 ∈ ℂ ∧
𝑦 ∈ ℋ)) ∧
𝑧 ∈ ℋ) →
(𝑇‘((𝑥
·ℎ 𝑦) +ℎ 𝑧)) ∈ ℋ) |
| 47 | | ffvelcdm 7101 |
. . . . . . . . . . 11
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ) →
(𝑇‘𝑦) ∈ ℋ) |
| 48 | | hvmulcl 31032 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ (𝑇‘𝑦) ∈ ℋ) → (𝑥 ·ℎ (𝑇‘𝑦)) ∈ ℋ) |
| 49 | 47, 48 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧ (𝑇: ℋ⟶ ℋ ∧
𝑦 ∈ ℋ)) →
(𝑥
·ℎ (𝑇‘𝑦)) ∈ ℋ) |
| 50 | 49 | an12s 649 |
. . . . . . . . 9
⊢ ((𝑇: ℋ⟶ ℋ ∧
(𝑥 ∈ ℂ ∧
𝑦 ∈ ℋ)) →
(𝑥
·ℎ (𝑇‘𝑦)) ∈ ℋ) |
| 51 | 50 | adantr 480 |
. . . . . . . 8
⊢ (((𝑇: ℋ⟶ ℋ ∧
(𝑥 ∈ ℂ ∧
𝑦 ∈ ℋ)) ∧
𝑧 ∈ ℋ) →
(𝑥
·ℎ (𝑇‘𝑦)) ∈ ℋ) |
| 52 | | ffvelcdm 7101 |
. . . . . . . . 9
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑧 ∈ ℋ) →
(𝑇‘𝑧) ∈ ℋ) |
| 53 | 52 | adantlr 715 |
. . . . . . . 8
⊢ (((𝑇: ℋ⟶ ℋ ∧
(𝑥 ∈ ℂ ∧
𝑦 ∈ ℋ)) ∧
𝑧 ∈ ℋ) →
(𝑇‘𝑧) ∈ ℋ) |
| 54 | | hvaddcl 31031 |
. . . . . . . 8
⊢ (((𝑥
·ℎ (𝑇‘𝑦)) ∈ ℋ ∧ (𝑇‘𝑧) ∈ ℋ) → ((𝑥 ·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧)) ∈ ℋ) |
| 55 | 51, 53, 54 | syl2anc 584 |
. . . . . . 7
⊢ (((𝑇: ℋ⟶ ℋ ∧
(𝑥 ∈ ℂ ∧
𝑦 ∈ ℋ)) ∧
𝑧 ∈ ℋ) →
((𝑥
·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧)) ∈ ℋ) |
| 56 | | hial2eq 31125 |
. . . . . . 7
⊢ (((𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) ∈ ℋ ∧ ((𝑥
·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧)) ∈ ℋ) → (∀𝑤 ∈ ℋ ((𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧))
·ih 𝑤) = (((𝑥 ·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧)) ·ih 𝑤) ↔ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧)))) |
| 57 | 46, 55, 56 | syl2anc 584 |
. . . . . 6
⊢ (((𝑇: ℋ⟶ ℋ ∧
(𝑥 ∈ ℂ ∧
𝑦 ∈ ℋ)) ∧
𝑧 ∈ ℋ) →
(∀𝑤 ∈ ℋ
((𝑇‘((𝑥
·ℎ 𝑦) +ℎ 𝑧)) ·ih 𝑤) = (((𝑥 ·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧)) ·ih 𝑤) ↔ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧)))) |
| 58 | 1, 57 | sylanl1 680 |
. . . . 5
⊢ (((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) →
(∀𝑤 ∈ ℋ
((𝑇‘((𝑥
·ℎ 𝑦) +ℎ 𝑧)) ·ih 𝑤) = (((𝑥 ·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧)) ·ih 𝑤) ↔ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧)))) |
| 59 | 43, 58 | mpbid 232 |
. . . 4
⊢ (((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) → (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧))) |
| 60 | 59 | ralrimiva 3146 |
. . 3
⊢ ((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) →
∀𝑧 ∈ ℋ
(𝑇‘((𝑥
·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧))) |
| 61 | 60 | ralrimivva 3202 |
. 2
⊢ (𝑇 ∈ HrmOp →
∀𝑥 ∈ ℂ
∀𝑦 ∈ ℋ
∀𝑧 ∈ ℋ
(𝑇‘((𝑥
·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧))) |
| 62 | | ellnop 31877 |
. 2
⊢ (𝑇 ∈ LinOp ↔ (𝑇: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℂ
∀𝑦 ∈ ℋ
∀𝑧 ∈ ℋ
(𝑇‘((𝑥
·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧)))) |
| 63 | 1, 61, 62 | sylanbrc 583 |
1
⊢ (𝑇 ∈ HrmOp → 𝑇 ∈ LinOp) |