Metamath Proof Explorer

Theorem lnophsi

Description: The sum of two linear operators is linear. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypotheses lnopco.1 ⊢ S ∈ LinOp
lnopco.2 ⊢ T ∈ LinOp
Assertion lnophsi ⊢ S + op T ∈ LinOp

Proof

Step Hyp Ref Expression
1 lnopco.1 ⊢ S ∈ LinOp
2 lnopco.2 ⊢ T ∈ LinOp
3 1 lnopfi ⊢ S : ℋ ⟶ ℋ
4 2 lnopfi ⊢ T : ℋ ⟶ ℋ
5 3 4 hoaddcli ⊢ S + op T : ℋ ⟶ ℋ
6 hvmulcl ⊢ x ∈ ℂ ∧ y ∈ ℋ → x ⋅ ℎ y ∈ ℋ
7 1 lnopaddi ⊢ x ⋅ ℎ y ∈ ℋ ∧ z ∈ ℋ → S ⁡ x ⋅ ℎ y + ℎ z = S ⁡ x ⋅ ℎ y + ℎ S ⁡ z
8 2 lnopaddi ⊢ x ⋅ ℎ y ∈ ℋ ∧ z ∈ ℋ → T ⁡ x ⋅ ℎ y + ℎ z = T ⁡ x ⋅ ℎ y + ℎ T ⁡ z
9 7 8 oveq12d ⊢ x ⋅ ℎ y ∈ ℋ ∧ z ∈ ℋ → S ⁡ x ⋅ ℎ y + ℎ z + ℎ T ⁡ x ⋅ ℎ y + ℎ z = S ⁡ x ⋅ ℎ y + ℎ S ⁡ z + ℎ T ⁡ x ⋅ ℎ y + ℎ T ⁡ z
10 6 9 sylan ⊢ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → S ⁡ x ⋅ ℎ y + ℎ z + ℎ T ⁡ x ⋅ ℎ y + ℎ z = S ⁡ x ⋅ ℎ y + ℎ S ⁡ z + ℎ T ⁡ x ⋅ ℎ y + ℎ T ⁡ z
11 3 ffvelrni ⊢ x ⋅ ℎ y ∈ ℋ → S ⁡ x ⋅ ℎ y ∈ ℋ
12 6 11 syl ⊢ x ∈ ℂ ∧ y ∈ ℋ → S ⁡ x ⋅ ℎ y ∈ ℋ
13 3 ffvelrni ⊢ z ∈ ℋ → S ⁡ z ∈ ℋ
14 12 13 anim12i ⊢ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → S ⁡ x ⋅ ℎ y ∈ ℋ ∧ S ⁡ z ∈ ℋ
15 4 ffvelrni ⊢ x ⋅ ℎ y ∈ ℋ → T ⁡ x ⋅ ℎ y ∈ ℋ
16 6 15 syl ⊢ x ∈ ℂ ∧ y ∈ ℋ → T ⁡ x ⋅ ℎ y ∈ ℋ
17 4 ffvelrni ⊢ z ∈ ℋ → T ⁡ z ∈ ℋ
18 16 17 anim12i ⊢ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → T ⁡ x ⋅ ℎ y ∈ ℋ ∧ T ⁡ z ∈ ℋ
19 hvadd4 ⊢ S ⁡ x ⋅ ℎ y ∈ ℋ ∧ S ⁡ z ∈ ℋ ∧ T ⁡ x ⋅ ℎ y ∈ ℋ ∧ T ⁡ z ∈ ℋ → S ⁡ x ⋅ ℎ y + ℎ S ⁡ z + ℎ T ⁡ x ⋅ ℎ y + ℎ T ⁡ z = S ⁡ x ⋅ ℎ y + ℎ T ⁡ x ⋅ ℎ y + ℎ S ⁡ z + ℎ T ⁡ z
20 14 18 19 syl2anc ⊢ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → S ⁡ x ⋅ ℎ y + ℎ S ⁡ z + ℎ T ⁡ x ⋅ ℎ y + ℎ T ⁡ z = S ⁡ x ⋅ ℎ y + ℎ T ⁡ x ⋅ ℎ y + ℎ S ⁡ z + ℎ T ⁡ z
21 10 20 eqtrd ⊢ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → S ⁡ x ⋅ ℎ y + ℎ z + ℎ T ⁡ x ⋅ ℎ y + ℎ z = S ⁡ x ⋅ ℎ y + ℎ T ⁡ x ⋅ ℎ y + ℎ S ⁡ z + ℎ T ⁡ z
22 hvaddcl ⊢ x ⋅ ℎ y ∈ ℋ ∧ z ∈ ℋ → x ⋅ ℎ y + ℎ z ∈ ℋ
23 6 22 sylan ⊢ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → x ⋅ ℎ y + ℎ z ∈ ℋ
24 hosval ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ ∧ x ⋅ ℎ y + ℎ z ∈ ℋ → S + op T ⁡ x ⋅ ℎ y + ℎ z = S ⁡ x ⋅ ℎ y + ℎ z + ℎ T ⁡ x ⋅ ℎ y + ℎ z
25 3 4 24 mp3an12 ⊢ x ⋅ ℎ y + ℎ z ∈ ℋ → S + op T ⁡ x ⋅ ℎ y + ℎ z = S ⁡ x ⋅ ℎ y + ℎ z + ℎ T ⁡ x ⋅ ℎ y + ℎ z
26 23 25 syl ⊢ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → S + op T ⁡ x ⋅ ℎ y + ℎ z = S ⁡ x ⋅ ℎ y + ℎ z + ℎ T ⁡ x ⋅ ℎ y + ℎ z
27 3 ffvelrni ⊢ y ∈ ℋ → S ⁡ y ∈ ℋ
28 4 ffvelrni ⊢ y ∈ ℋ → T ⁡ y ∈ ℋ
29 27 28 jca ⊢ y ∈ ℋ → S ⁡ y ∈ ℋ ∧ T ⁡ y ∈ ℋ
30 ax-hvdistr1 ⊢ x ∈ ℂ ∧ S ⁡ y ∈ ℋ ∧ T ⁡ y ∈ ℋ → x ⋅ ℎ S ⁡ y + ℎ T ⁡ y = x ⋅ ℎ S ⁡ y + ℎ x ⋅ ℎ T ⁡ y
31 30 3expb ⊢ x ∈ ℂ ∧ S ⁡ y ∈ ℋ ∧ T ⁡ y ∈ ℋ → x ⋅ ℎ S ⁡ y + ℎ T ⁡ y = x ⋅ ℎ S ⁡ y + ℎ x ⋅ ℎ T ⁡ y
32 29 31 sylan2 ⊢ x ∈ ℂ ∧ y ∈ ℋ → x ⋅ ℎ S ⁡ y + ℎ T ⁡ y = x ⋅ ℎ S ⁡ y + ℎ x ⋅ ℎ T ⁡ y
33 hosval ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ ∧ y ∈ ℋ → S + op T ⁡ y = S ⁡ y + ℎ T ⁡ y
34 3 4 33 mp3an12 ⊢ y ∈ ℋ → S + op T ⁡ y = S ⁡ y + ℎ T ⁡ y
35 34 oveq2d ⊢ y ∈ ℋ → x ⋅ ℎ S + op T ⁡ y = x ⋅ ℎ S ⁡ y + ℎ T ⁡ y
36 35 adantl ⊢ x ∈ ℂ ∧ y ∈ ℋ → x ⋅ ℎ S + op T ⁡ y = x ⋅ ℎ S ⁡ y + ℎ T ⁡ y
37 1 lnopmuli ⊢ x ∈ ℂ ∧ y ∈ ℋ → S ⁡ x ⋅ ℎ y = x ⋅ ℎ S ⁡ y
38 2 lnopmuli ⊢ x ∈ ℂ ∧ y ∈ ℋ → T ⁡ x ⋅ ℎ y = x ⋅ ℎ T ⁡ y
39 37 38 oveq12d ⊢ x ∈ ℂ ∧ y ∈ ℋ → S ⁡ x ⋅ ℎ y + ℎ T ⁡ x ⋅ ℎ y = x ⋅ ℎ S ⁡ y + ℎ x ⋅ ℎ T ⁡ y
40 32 36 39 3eqtr4d ⊢ x ∈ ℂ ∧ y ∈ ℋ → x ⋅ ℎ S + op T ⁡ y = S ⁡ x ⋅ ℎ y + ℎ T ⁡ x ⋅ ℎ y
41 hosval ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ ∧ z ∈ ℋ → S + op T ⁡ z = S ⁡ z + ℎ T ⁡ z
42 3 4 41 mp3an12 ⊢ z ∈ ℋ → S + op T ⁡ z = S ⁡ z + ℎ T ⁡ z
43 40 42 oveqan12d ⊢ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → x ⋅ ℎ S + op T ⁡ y + ℎ S + op T ⁡ z = S ⁡ x ⋅ ℎ y + ℎ T ⁡ x ⋅ ℎ y + ℎ S ⁡ z + ℎ T ⁡ z
44 21 26 43 3eqtr4d ⊢ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → S + op T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ S + op T ⁡ y + ℎ S + op T ⁡ z
45 44 ralrimiva ⊢ x ∈ ℂ ∧ y ∈ ℋ → ∀ z ∈ ℋ S + op T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ S + op T ⁡ y + ℎ S + op T ⁡ z
46 45 rgen2 ⊢ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ S + op T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ S + op T ⁡ y + ℎ S + op T ⁡ z
47 ellnop ⊢ S + op T ∈ LinOp ↔ S + op T : ℋ ⟶ ℋ ∧ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ S + op T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ S + op T ⁡ y + ℎ S + op T ⁡ z
48 5 46 47 mpbir2an ⊢ S + op T ∈ LinOp