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 ⊢ 𝑆 ∈ LinOp
lnopco.2 ⊢ 𝑇 ∈ LinOp
Assertion lnophsi ( 𝑆 +op 𝑇 ) ∈ LinOp

Proof

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