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 ⊢S∈LinOp
lnopco.2 ⊢T∈LinOp
Assertion lnopcoi ⊢S∘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 hocofi ⊢S∘T:ℋ⟶ℋ
6 2 lnopli ⊢x∈ℂ∧y∈ℋ∧z∈ℋ→T⁡x⋅ℎy+ℎz=x⋅ℎT⁡y+ℎT⁡z
7 6 fveq2d ⊢x∈ℂ∧y∈ℋ∧z∈ℋ→S⁡T⁡x⋅ℎy+ℎz=S⁡x⋅ℎT⁡y+ℎT⁡z
8 id ⊢x∈ℂ→x∈ℂ
9 4 ffvelcdmi ⊢y∈ℋ→T⁡y∈ℋ
10 4 ffvelcdmi ⊢z∈ℋ→T⁡z∈ℋ
11 1 lnopli ⊢x∈ℂ∧T⁡y∈ℋ∧T⁡z∈ℋ→S⁡x⋅ℎT⁡y+ℎT⁡z=x⋅ℎS⁡T⁡y+ℎS⁡T⁡z
12 8 9 10 11 syl3an ⊢x∈ℂ∧y∈ℋ∧z∈ℋ→S⁡x⋅ℎT⁡y+ℎT⁡z=x⋅ℎS⁡T⁡y+ℎS⁡T⁡z
13 7 12 eqtrd ⊢x∈ℂ∧y∈ℋ∧z∈ℋ→S⁡T⁡x⋅ℎy+ℎz=x⋅ℎS⁡T⁡y+ℎS⁡T⁡z
14 13 3expa ⊢x∈ℂ∧y∈ℋ∧z∈ℋ→S⁡T⁡x⋅ℎy+ℎz=x⋅ℎS⁡T⁡y+ℎS⁡T⁡z
15 hvmulcl ⊢x∈ℂ∧y∈ℋ→x⋅ℎy∈ℋ
16 hvaddcl ⊢x⋅ℎy∈ℋ∧z∈ℋ→x⋅ℎy+ℎz∈ℋ
17 15 16 sylan ⊢x∈ℂ∧y∈ℋ∧z∈ℋ→x⋅ℎy+ℎz∈ℋ
18 3 4 hocoi ⊢x⋅ℎy+ℎz∈ℋ→S∘T⁡x⋅ℎy+ℎz=S⁡T⁡x⋅ℎy+ℎz
19 17 18 syl ⊢x∈ℂ∧y∈ℋ∧z∈ℋ→S∘T⁡x⋅ℎy+ℎz=S⁡T⁡x⋅ℎy+ℎz
20 3 4 hocoi ⊢y∈ℋ→S∘T⁡y=S⁡T⁡y
21 20 oveq2d ⊢y∈ℋ→x⋅ℎS∘T⁡y=x⋅ℎS⁡T⁡y
22 21 adantl ⊢x∈ℂ∧y∈ℋ→x⋅ℎS∘T⁡y=x⋅ℎS⁡T⁡y
23 3 4 hocoi ⊢z∈ℋ→S∘T⁡z=S⁡T⁡z
24 22 23 oveqan12d ⊢x∈ℂ∧y∈ℋ∧z∈ℋ→x⋅ℎS∘T⁡y+ℎS∘T⁡z=x⋅ℎS⁡T⁡y+ℎS⁡T⁡z
25 14 19 24 3eqtr4d ⊢x∈ℂ∧y∈ℋ∧z∈ℋ→S∘T⁡x⋅ℎy+ℎz=x⋅ℎS∘T⁡y+ℎS∘T⁡z
26 25 3impa ⊢x∈ℂ∧y∈ℋ∧z∈ℋ→S∘T⁡x⋅ℎy+ℎz=x⋅ℎS∘T⁡y+ℎS∘T⁡z
27 26 rgen3 ⊢∀x∈ℂ∀y∈ℋ∀z∈ℋS∘T⁡x⋅ℎy+ℎz=x⋅ℎS∘T⁡y+ℎS∘T⁡z
28 ellnop ⊢S∘T∈LinOp↔S∘T:ℋ⟶ℋ∧∀x∈ℂ∀y∈ℋ∀z∈ℋS∘T⁡x⋅ℎy+ℎz=x⋅ℎS∘T⁡y+ℎS∘T⁡z
29 5 27 28 mpbir2an ⊢S∘T∈LinOp