| Step | Hyp | Ref
| Expression |
| 1 | | lnopco.1 |
. . . 4
⊢ 𝑆 ∈ LinOp |
| 2 | 1 | lnopfi 31988 |
. . 3
⊢ 𝑆: ℋ⟶
ℋ |
| 3 | | lnopco.2 |
. . . 4
⊢ 𝑇 ∈ LinOp |
| 4 | 3 | lnopfi 31988 |
. . 3
⊢ 𝑇: ℋ⟶
ℋ |
| 5 | 2, 4 | hoaddcli 31787 |
. 2
⊢ (𝑆 +op 𝑇): ℋ⟶
ℋ |
| 6 | | hvmulcl 31032 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑥
·ℎ 𝑦) ∈ ℋ) |
| 7 | 1 | lnopaddi 31990 |
. . . . . . . 8
⊢ (((𝑥
·ℎ 𝑦) ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑆‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑆‘𝑧))) |
| 8 | 3 | lnopaddi 31990 |
. . . . . . . 8
⊢ (((𝑥
·ℎ 𝑦) ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑇‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘𝑧))) |
| 9 | 7, 8 | oveq12d 7449 |
. . . . . . 7
⊢ (((𝑥
·ℎ 𝑦) ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑆‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) +ℎ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧))) = (((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑆‘𝑧)) +ℎ ((𝑇‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘𝑧)))) |
| 10 | 6, 9 | sylan 580 |
. . . . . 6
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑆‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) +ℎ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧))) = (((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑆‘𝑧)) +ℎ ((𝑇‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘𝑧)))) |
| 11 | 2 | ffvelcdmi 7103 |
. . . . . . . . 9
⊢ ((𝑥
·ℎ 𝑦) ∈ ℋ → (𝑆‘(𝑥 ·ℎ 𝑦)) ∈
ℋ) |
| 12 | 6, 11 | syl 17 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑆‘(𝑥 ·ℎ 𝑦)) ∈
ℋ) |
| 13 | 2 | ffvelcdmi 7103 |
. . . . . . . 8
⊢ (𝑧 ∈ ℋ → (𝑆‘𝑧) ∈ ℋ) |
| 14 | 12, 13 | anim12i 613 |
. . . . . . 7
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑆‘(𝑥 ·ℎ 𝑦)) ∈ ℋ ∧ (𝑆‘𝑧) ∈ ℋ)) |
| 15 | 4 | ffvelcdmi 7103 |
. . . . . . . . 9
⊢ ((𝑥
·ℎ 𝑦) ∈ ℋ → (𝑇‘(𝑥 ·ℎ 𝑦)) ∈
ℋ) |
| 16 | 6, 15 | syl 17 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑇‘(𝑥 ·ℎ 𝑦)) ∈
ℋ) |
| 17 | 4 | ffvelcdmi 7103 |
. . . . . . . 8
⊢ (𝑧 ∈ ℋ → (𝑇‘𝑧) ∈ ℋ) |
| 18 | 16, 17 | anim12i 613 |
. . . . . . 7
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑇‘(𝑥 ·ℎ 𝑦)) ∈ ℋ ∧ (𝑇‘𝑧) ∈ ℋ)) |
| 19 | | hvadd4 31055 |
. . . . . . 7
⊢ ((((𝑆‘(𝑥 ·ℎ 𝑦)) ∈ ℋ ∧ (𝑆‘𝑧) ∈ ℋ) ∧ ((𝑇‘(𝑥 ·ℎ 𝑦)) ∈ ℋ ∧ (𝑇‘𝑧) ∈ ℋ)) → (((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑆‘𝑧)) +ℎ ((𝑇‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘𝑧))) = (((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘(𝑥 ·ℎ 𝑦))) +ℎ ((𝑆‘𝑧) +ℎ (𝑇‘𝑧)))) |
| 20 | 14, 18, 19 | syl2anc 584 |
. . . . . 6
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → (((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑆‘𝑧)) +ℎ ((𝑇‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘𝑧))) = (((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘(𝑥 ·ℎ 𝑦))) +ℎ ((𝑆‘𝑧) +ℎ (𝑇‘𝑧)))) |
| 21 | 10, 20 | eqtrd 2777 |
. . . . 5
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑆‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) +ℎ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧))) = (((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘(𝑥 ·ℎ 𝑦))) +ℎ ((𝑆‘𝑧) +ℎ (𝑇‘𝑧)))) |
| 22 | | hvaddcl 31031 |
. . . . . . 7
⊢ (((𝑥
·ℎ 𝑦) ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑥 ·ℎ 𝑦) +ℎ 𝑧) ∈
ℋ) |
| 23 | 6, 22 | sylan 580 |
. . . . . 6
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑥
·ℎ 𝑦) +ℎ 𝑧) ∈ ℋ) |
| 24 | | hosval 31759 |
. . . . . . 7
⊢ ((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ
∧ ((𝑥
·ℎ 𝑦) +ℎ 𝑧) ∈ ℋ) → ((𝑆 +op 𝑇)‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑆‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) +ℎ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)))) |
| 25 | 2, 4, 24 | mp3an12 1453 |
. . . . . 6
⊢ (((𝑥
·ℎ 𝑦) +ℎ 𝑧) ∈ ℋ → ((𝑆 +op 𝑇)‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑆‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) +ℎ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)))) |
| 26 | 23, 25 | syl 17 |
. . . . 5
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑆 +op 𝑇)‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑆‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) +ℎ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)))) |
| 27 | 2 | ffvelcdmi 7103 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℋ → (𝑆‘𝑦) ∈ ℋ) |
| 28 | 4 | ffvelcdmi 7103 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℋ → (𝑇‘𝑦) ∈ ℋ) |
| 29 | 27, 28 | jca 511 |
. . . . . . . 8
⊢ (𝑦 ∈ ℋ → ((𝑆‘𝑦) ∈ ℋ ∧ (𝑇‘𝑦) ∈ ℋ)) |
| 30 | | ax-hvdistr1 31027 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ (𝑆‘𝑦) ∈ ℋ ∧ (𝑇‘𝑦) ∈ ℋ) → (𝑥 ·ℎ ((𝑆‘𝑦) +ℎ (𝑇‘𝑦))) = ((𝑥 ·ℎ (𝑆‘𝑦)) +ℎ (𝑥 ·ℎ (𝑇‘𝑦)))) |
| 31 | 30 | 3expb 1121 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ ((𝑆‘𝑦) ∈ ℋ ∧ (𝑇‘𝑦) ∈ ℋ)) → (𝑥 ·ℎ ((𝑆‘𝑦) +ℎ (𝑇‘𝑦))) = ((𝑥 ·ℎ (𝑆‘𝑦)) +ℎ (𝑥 ·ℎ (𝑇‘𝑦)))) |
| 32 | 29, 31 | sylan2 593 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑥
·ℎ ((𝑆‘𝑦) +ℎ (𝑇‘𝑦))) = ((𝑥 ·ℎ (𝑆‘𝑦)) +ℎ (𝑥 ·ℎ (𝑇‘𝑦)))) |
| 33 | | hosval 31759 |
. . . . . . . . . 10
⊢ ((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ)
→ ((𝑆 +op
𝑇)‘𝑦) = ((𝑆‘𝑦) +ℎ (𝑇‘𝑦))) |
| 34 | 2, 4, 33 | mp3an12 1453 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℋ → ((𝑆 +op 𝑇)‘𝑦) = ((𝑆‘𝑦) +ℎ (𝑇‘𝑦))) |
| 35 | 34 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑦 ∈ ℋ → (𝑥
·ℎ ((𝑆 +op 𝑇)‘𝑦)) = (𝑥 ·ℎ ((𝑆‘𝑦) +ℎ (𝑇‘𝑦)))) |
| 36 | 35 | adantl 481 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑥
·ℎ ((𝑆 +op 𝑇)‘𝑦)) = (𝑥 ·ℎ ((𝑆‘𝑦) +ℎ (𝑇‘𝑦)))) |
| 37 | 1 | lnopmuli 31991 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑆‘(𝑥 ·ℎ 𝑦)) = (𝑥 ·ℎ (𝑆‘𝑦))) |
| 38 | 3 | lnopmuli 31991 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑇‘(𝑥 ·ℎ 𝑦)) = (𝑥 ·ℎ (𝑇‘𝑦))) |
| 39 | 37, 38 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → ((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘(𝑥 ·ℎ 𝑦))) = ((𝑥 ·ℎ (𝑆‘𝑦)) +ℎ (𝑥 ·ℎ (𝑇‘𝑦)))) |
| 40 | 32, 36, 39 | 3eqtr4d 2787 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑥
·ℎ ((𝑆 +op 𝑇)‘𝑦)) = ((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘(𝑥 ·ℎ 𝑦)))) |
| 41 | | hosval 31759 |
. . . . . . 7
⊢ ((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ
∧ 𝑧 ∈ ℋ)
→ ((𝑆 +op
𝑇)‘𝑧) = ((𝑆‘𝑧) +ℎ (𝑇‘𝑧))) |
| 42 | 2, 4, 41 | mp3an12 1453 |
. . . . . 6
⊢ (𝑧 ∈ ℋ → ((𝑆 +op 𝑇)‘𝑧) = ((𝑆‘𝑧) +ℎ (𝑇‘𝑧))) |
| 43 | 40, 42 | oveqan12d 7450 |
. . . . 5
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑥
·ℎ ((𝑆 +op 𝑇)‘𝑦)) +ℎ ((𝑆 +op 𝑇)‘𝑧)) = (((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘(𝑥 ·ℎ 𝑦))) +ℎ ((𝑆‘𝑧) +ℎ (𝑇‘𝑧)))) |
| 44 | 21, 26, 43 | 3eqtr4d 2787 |
. . . 4
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑆 +op 𝑇)‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ ((𝑆 +op 𝑇)‘𝑦)) +ℎ ((𝑆 +op 𝑇)‘𝑧))) |
| 45 | 44 | ralrimiva 3146 |
. . 3
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) →
∀𝑧 ∈ ℋ
((𝑆 +op 𝑇)‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ ((𝑆 +op 𝑇)‘𝑦)) +ℎ ((𝑆 +op 𝑇)‘𝑧))) |
| 46 | 45 | rgen2 3199 |
. 2
⊢
∀𝑥 ∈
ℂ ∀𝑦 ∈
ℋ ∀𝑧 ∈
ℋ ((𝑆 +op
𝑇)‘((𝑥
·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ ((𝑆 +op 𝑇)‘𝑦)) +ℎ ((𝑆 +op 𝑇)‘𝑧)) |
| 47 | | ellnop 31877 |
. 2
⊢ ((𝑆 +op 𝑇) ∈ LinOp ↔ ((𝑆 +op 𝑇): ℋ⟶ ℋ ∧
∀𝑥 ∈ ℂ
∀𝑦 ∈ ℋ
∀𝑧 ∈ ℋ
((𝑆 +op 𝑇)‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ ((𝑆 +op 𝑇)‘𝑦)) +ℎ ((𝑆 +op 𝑇)‘𝑧)))) |
| 48 | 5, 46, 47 | mpbir2an 711 |
1
⊢ (𝑆 +op 𝑇) ∈ LinOp |