Metamath Proof Explorer

Theorem lnopcoi

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

Ref Expression
Hypotheses lnopco.1 ⊢ 𝑆 ∈ LinOp
lnopco.2 ⊢ 𝑇 ∈ LinOp
Assertion lnopcoi ( 𝑆 ∘ 𝑇 ) ∈ LinOp

Proof

Step Hyp Ref Expression
1 lnopco.1 ⊢ 𝑆 ∈ LinOp
2 lnopco.2 ⊢ 𝑇 ∈ LinOp
3 1 lnopfi ⊢ 𝑆 : ℋ ⟶ ℋ
4 2 lnopfi ⊢ 𝑇 : ℋ ⟶ ℋ
5 3 4 hocofi ⊢ ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ ℋ
6 2 lnopli ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) )
7 6 fveq2d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑆 ‘ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) = ( 𝑆 ‘ ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) )
8 id ⊢ ( 𝑥 ∈ ℂ → 𝑥 ∈ ℂ )
9 4 ffvelcdmi ⊢ ( 𝑦 ∈ ℋ → ( 𝑇 ‘ 𝑦 ) ∈ ℋ )
10 4 ffvelcdmi ⊢ ( 𝑧 ∈ ℋ → ( 𝑇 ‘ 𝑧 ) ∈ ℋ )
11 1 lnopli ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑇 ‘ 𝑦 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑧 ) ∈ ℋ ) → ( 𝑆 ‘ ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) = ( ( 𝑥 ·ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑦 ) ) ) +ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑧 ) ) ) )
12 8 9 10 11 syl3an ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑆 ‘ ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) = ( ( 𝑥 ·ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑦 ) ) ) +ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑧 ) ) ) )
13 7 12 eqtrd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑆 ‘ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) = ( ( 𝑥 ·ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑦 ) ) ) +ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑧 ) ) ) )
14 13 3expa ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( 𝑆 ‘ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) = ( ( 𝑥 ·ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑦 ) ) ) +ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑧 ) ) ) )
15 hvmulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ )
16 hvaddcl ⊢ ( ( ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ )
17 15 16 sylan ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ )
18 3 4 hocoi ⊢ ( ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ → ( ( 𝑆 ∘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( 𝑆 ‘ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) )
19 17 18 syl ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑆 ∘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( 𝑆 ‘ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) )
20 3 4 hocoi ⊢ ( 𝑦 ∈ ℋ → ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑦 ) = ( 𝑆 ‘ ( 𝑇 ‘ 𝑦 ) ) )
21 20 oveq2d ⊢ ( 𝑦 ∈ ℋ → ( 𝑥 ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑦 ) ) = ( 𝑥 ·ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
22 21 adantl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑦 ) ) = ( 𝑥 ·ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
23 3 4 hocoi ⊢ ( 𝑧 ∈ ℋ → ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑧 ) = ( 𝑆 ‘ ( 𝑇 ‘ 𝑧 ) ) )
24 22 23 oveqan12d ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑦 ) ) ) +ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑧 ) ) ) )
25 14 19 24 3eqtr4d ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑆 ∘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑧 ) ) )
26 25 3impa ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑆 ∘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑧 ) ) )
27 26 rgen3 ⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑆 ∘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑧 ) )
28 ellnop ⊢ ( ( 𝑆 ∘ 𝑇 ) ∈ LinOp ↔ ( ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑆 ∘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑧 ) ) ) )
29 5 27 28 mpbir2an ⊢ ( 𝑆 ∘ 𝑇 ) ∈ LinOp