Step | Hyp | Ref
| Expression |
1 | | lnopco.1 |
. . . 4
⊢ 𝑆 ∈ LinOp |
2 | 1 | lnopfi 29904 |
. . 3
⊢ 𝑆: ℋ⟶
ℋ |
3 | | lnopco.2 |
. . . 4
⊢ 𝑇 ∈ LinOp |
4 | 3 | lnopfi 29904 |
. . 3
⊢ 𝑇: ℋ⟶
ℋ |
5 | 2, 4 | hoaddcli 29703 |
. 2
⊢ (𝑆 +op 𝑇): ℋ⟶
ℋ |
6 | | hvmulcl 28948 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑥
·ℎ 𝑦) ∈ ℋ) |
7 | 1 | lnopaddi 29906 |
. . . . . . . 8
⊢ (((𝑥
·ℎ 𝑦) ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑆‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑆‘𝑧))) |
8 | 3 | lnopaddi 29906 |
. . . . . . . 8
⊢ (((𝑥
·ℎ 𝑦) ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑇‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘𝑧))) |
9 | 7, 8 | oveq12d 7189 |
. . . . . . 7
⊢ (((𝑥
·ℎ 𝑦) ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑆‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) +ℎ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧))) = (((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑆‘𝑧)) +ℎ ((𝑇‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘𝑧)))) |
10 | 6, 9 | sylan 583 |
. . . . . 6
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑆‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) +ℎ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧))) = (((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑆‘𝑧)) +ℎ ((𝑇‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘𝑧)))) |
11 | 2 | ffvelrni 6861 |
. . . . . . . . 9
⊢ ((𝑥
·ℎ 𝑦) ∈ ℋ → (𝑆‘(𝑥 ·ℎ 𝑦)) ∈
ℋ) |
12 | 6, 11 | syl 17 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑆‘(𝑥 ·ℎ 𝑦)) ∈
ℋ) |
13 | 2 | ffvelrni 6861 |
. . . . . . . 8
⊢ (𝑧 ∈ ℋ → (𝑆‘𝑧) ∈ ℋ) |
14 | 12, 13 | anim12i 616 |
. . . . . . 7
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑆‘(𝑥 ·ℎ 𝑦)) ∈ ℋ ∧ (𝑆‘𝑧) ∈ ℋ)) |
15 | 4 | ffvelrni 6861 |
. . . . . . . . 9
⊢ ((𝑥
·ℎ 𝑦) ∈ ℋ → (𝑇‘(𝑥 ·ℎ 𝑦)) ∈
ℋ) |
16 | 6, 15 | syl 17 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑇‘(𝑥 ·ℎ 𝑦)) ∈
ℋ) |
17 | 4 | ffvelrni 6861 |
. . . . . . . 8
⊢ (𝑧 ∈ ℋ → (𝑇‘𝑧) ∈ ℋ) |
18 | 16, 17 | anim12i 616 |
. . . . . . 7
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑇‘(𝑥 ·ℎ 𝑦)) ∈ ℋ ∧ (𝑇‘𝑧) ∈ ℋ)) |
19 | | hvadd4 28971 |
. . . . . . 7
⊢ ((((𝑆‘(𝑥 ·ℎ 𝑦)) ∈ ℋ ∧ (𝑆‘𝑧) ∈ ℋ) ∧ ((𝑇‘(𝑥 ·ℎ 𝑦)) ∈ ℋ ∧ (𝑇‘𝑧) ∈ ℋ)) → (((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑆‘𝑧)) +ℎ ((𝑇‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘𝑧))) = (((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘(𝑥 ·ℎ 𝑦))) +ℎ ((𝑆‘𝑧) +ℎ (𝑇‘𝑧)))) |
20 | 14, 18, 19 | syl2anc 587 |
. . . . . 6
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → (((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑆‘𝑧)) +ℎ ((𝑇‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘𝑧))) = (((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘(𝑥 ·ℎ 𝑦))) +ℎ ((𝑆‘𝑧) +ℎ (𝑇‘𝑧)))) |
21 | 10, 20 | eqtrd 2773 |
. . . . 5
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑆‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) +ℎ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧))) = (((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘(𝑥 ·ℎ 𝑦))) +ℎ ((𝑆‘𝑧) +ℎ (𝑇‘𝑧)))) |
22 | | hvaddcl 28947 |
. . . . . . 7
⊢ (((𝑥
·ℎ 𝑦) ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑥 ·ℎ 𝑦) +ℎ 𝑧) ∈
ℋ) |
23 | 6, 22 | sylan 583 |
. . . . . 6
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑥
·ℎ 𝑦) +ℎ 𝑧) ∈ ℋ) |
24 | | hosval 29675 |
. . . . . . 7
⊢ ((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ
∧ ((𝑥
·ℎ 𝑦) +ℎ 𝑧) ∈ ℋ) → ((𝑆 +op 𝑇)‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑆‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) +ℎ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)))) |
25 | 2, 4, 24 | mp3an12 1452 |
. . . . . 6
⊢ (((𝑥
·ℎ 𝑦) +ℎ 𝑧) ∈ ℋ → ((𝑆 +op 𝑇)‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑆‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) +ℎ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)))) |
26 | 23, 25 | syl 17 |
. . . . 5
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑆 +op 𝑇)‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑆‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) +ℎ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)))) |
27 | 2 | ffvelrni 6861 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℋ → (𝑆‘𝑦) ∈ ℋ) |
28 | 4 | ffvelrni 6861 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℋ → (𝑇‘𝑦) ∈ ℋ) |
29 | 27, 28 | jca 515 |
. . . . . . . 8
⊢ (𝑦 ∈ ℋ → ((𝑆‘𝑦) ∈ ℋ ∧ (𝑇‘𝑦) ∈ ℋ)) |
30 | | ax-hvdistr1 28943 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ (𝑆‘𝑦) ∈ ℋ ∧ (𝑇‘𝑦) ∈ ℋ) → (𝑥 ·ℎ ((𝑆‘𝑦) +ℎ (𝑇‘𝑦))) = ((𝑥 ·ℎ (𝑆‘𝑦)) +ℎ (𝑥 ·ℎ (𝑇‘𝑦)))) |
31 | 30 | 3expb 1121 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ ((𝑆‘𝑦) ∈ ℋ ∧ (𝑇‘𝑦) ∈ ℋ)) → (𝑥 ·ℎ ((𝑆‘𝑦) +ℎ (𝑇‘𝑦))) = ((𝑥 ·ℎ (𝑆‘𝑦)) +ℎ (𝑥 ·ℎ (𝑇‘𝑦)))) |
32 | 29, 31 | sylan2 596 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑥
·ℎ ((𝑆‘𝑦) +ℎ (𝑇‘𝑦))) = ((𝑥 ·ℎ (𝑆‘𝑦)) +ℎ (𝑥 ·ℎ (𝑇‘𝑦)))) |
33 | | hosval 29675 |
. . . . . . . . . 10
⊢ ((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ
∧ 𝑦 ∈ ℋ)
→ ((𝑆 +op
𝑇)‘𝑦) = ((𝑆‘𝑦) +ℎ (𝑇‘𝑦))) |
34 | 2, 4, 33 | mp3an12 1452 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℋ → ((𝑆 +op 𝑇)‘𝑦) = ((𝑆‘𝑦) +ℎ (𝑇‘𝑦))) |
35 | 34 | oveq2d 7187 |
. . . . . . . 8
⊢ (𝑦 ∈ ℋ → (𝑥
·ℎ ((𝑆 +op 𝑇)‘𝑦)) = (𝑥 ·ℎ ((𝑆‘𝑦) +ℎ (𝑇‘𝑦)))) |
36 | 35 | adantl 485 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑥
·ℎ ((𝑆 +op 𝑇)‘𝑦)) = (𝑥 ·ℎ ((𝑆‘𝑦) +ℎ (𝑇‘𝑦)))) |
37 | 1 | lnopmuli 29907 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑆‘(𝑥 ·ℎ 𝑦)) = (𝑥 ·ℎ (𝑆‘𝑦))) |
38 | 3 | lnopmuli 29907 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑇‘(𝑥 ·ℎ 𝑦)) = (𝑥 ·ℎ (𝑇‘𝑦))) |
39 | 37, 38 | oveq12d 7189 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → ((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘(𝑥 ·ℎ 𝑦))) = ((𝑥 ·ℎ (𝑆‘𝑦)) +ℎ (𝑥 ·ℎ (𝑇‘𝑦)))) |
40 | 32, 36, 39 | 3eqtr4d 2783 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑥
·ℎ ((𝑆 +op 𝑇)‘𝑦)) = ((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘(𝑥 ·ℎ 𝑦)))) |
41 | | hosval 29675 |
. . . . . . 7
⊢ ((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ
∧ 𝑧 ∈ ℋ)
→ ((𝑆 +op
𝑇)‘𝑧) = ((𝑆‘𝑧) +ℎ (𝑇‘𝑧))) |
42 | 2, 4, 41 | mp3an12 1452 |
. . . . . 6
⊢ (𝑧 ∈ ℋ → ((𝑆 +op 𝑇)‘𝑧) = ((𝑆‘𝑧) +ℎ (𝑇‘𝑧))) |
43 | 40, 42 | oveqan12d 7190 |
. . . . 5
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑥
·ℎ ((𝑆 +op 𝑇)‘𝑦)) +ℎ ((𝑆 +op 𝑇)‘𝑧)) = (((𝑆‘(𝑥 ·ℎ 𝑦)) +ℎ (𝑇‘(𝑥 ·ℎ 𝑦))) +ℎ ((𝑆‘𝑧) +ℎ (𝑇‘𝑧)))) |
44 | 21, 26, 43 | 3eqtr4d 2783 |
. . . 4
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑆 +op 𝑇)‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ ((𝑆 +op 𝑇)‘𝑦)) +ℎ ((𝑆 +op 𝑇)‘𝑧))) |
45 | 44 | ralrimiva 3096 |
. . 3
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) →
∀𝑧 ∈ ℋ
((𝑆 +op 𝑇)‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ ((𝑆 +op 𝑇)‘𝑦)) +ℎ ((𝑆 +op 𝑇)‘𝑧))) |
46 | 45 | rgen2 3115 |
. 2
⊢
∀𝑥 ∈
ℂ ∀𝑦 ∈
ℋ ∀𝑧 ∈
ℋ ((𝑆 +op
𝑇)‘((𝑥
·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ ((𝑆 +op 𝑇)‘𝑦)) +ℎ ((𝑆 +op 𝑇)‘𝑧)) |
47 | | ellnop 29793 |
. 2
⊢ ((𝑆 +op 𝑇) ∈ LinOp ↔ ((𝑆 +op 𝑇): ℋ⟶ ℋ ∧
∀𝑥 ∈ ℂ
∀𝑦 ∈ ℋ
∀𝑧 ∈ ℋ
((𝑆 +op 𝑇)‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ ((𝑆 +op 𝑇)‘𝑦)) +ℎ ((𝑆 +op 𝑇)‘𝑧)))) |
48 | 5, 46, 47 | mpbir2an 711 |
1
⊢ (𝑆 +op 𝑇) ∈ LinOp |