Metamath Proof Explorer

Theorem lnocoi

Description: The composition of two linear operators is linear. (Contributed by NM, 12-Jan-2008) (Revised by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses lnocoi.l ⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
lnocoi.m ⊢ 𝑀 = ( 𝑊 LnOp 𝑋 )
lnocoi.n ⊢ 𝑁 = ( 𝑈 LnOp 𝑋 )
lnocoi.u ⊢ 𝑈 ∈ NrmCVec
lnocoi.w ⊢ 𝑊 ∈ NrmCVec
lnocoi.x ⊢ 𝑋 ∈ NrmCVec
lnocoi.s ⊢ 𝑆 ∈ 𝐿
lnocoi.t ⊢ 𝑇 ∈ 𝑀
Assertion lnocoi ( 𝑇 ∘ 𝑆 ) ∈ 𝑁

Proof

Step Hyp Ref Expression
1 lnocoi.l ⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
2 lnocoi.m ⊢ 𝑀 = ( 𝑊 LnOp 𝑋 )
3 lnocoi.n ⊢ 𝑁 = ( 𝑈 LnOp 𝑋 )
4 lnocoi.u ⊢ 𝑈 ∈ NrmCVec
5 lnocoi.w ⊢ 𝑊 ∈ NrmCVec
6 lnocoi.x ⊢ 𝑋 ∈ NrmCVec
7 lnocoi.s ⊢ 𝑆 ∈ 𝐿
8 lnocoi.t ⊢ 𝑇 ∈ 𝑀
9 eqid ⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
10 eqid ⊢ ( BaseSet ‘ 𝑋 ) = ( BaseSet ‘ 𝑋 )
11 9 10 2 lnof ⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑋 ∈ NrmCVec ∧ 𝑇 ∈ 𝑀 ) → 𝑇 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑋 ) )
12 5 6 8 11 mp3an ⊢ 𝑇 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑋 )
13 eqid ⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
14 13 9 1 lnof ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑆 ∈ 𝐿 ) → 𝑆 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) )
15 4 5 7 14 mp3an ⊢ 𝑆 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 )
16 fco ⊢ ( ( 𝑇 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑋 ) ∧ 𝑆 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ) → ( 𝑇 ∘ 𝑆 ) : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑋 ) )
17 12 15 16 mp2an ⊢ ( 𝑇 ∘ 𝑆 ) : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑋 )
18 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
19 13 18 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ∈ ( BaseSet ‘ 𝑈 ) )
20 4 19 mp3an1 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ∈ ( BaseSet ‘ 𝑈 ) )
21 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
22 13 21 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ∈ ( BaseSet ‘ 𝑈 ) )
23 4 22 mp3an1 ⊢ ( ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ∈ ( BaseSet ‘ 𝑈 ) )
24 20 23 stoic3 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ∈ ( BaseSet ‘ 𝑈 ) )
25 fvco3 ⊢ ( ( 𝑆 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑇 ∘ 𝑆 ) ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ) = ( 𝑇 ‘ ( 𝑆 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ) ) )
26 15 24 25 sylancr ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑇 ∘ 𝑆 ) ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ) = ( 𝑇 ‘ ( 𝑆 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ) ) )
27 id ⊢ ( 𝑥 ∈ ℂ → 𝑥 ∈ ℂ )
28 15 ffvelrni ⊢ ( 𝑦 ∈ ( BaseSet ‘ 𝑈 ) → ( 𝑆 ‘ 𝑦 ) ∈ ( BaseSet ‘ 𝑊 ) )
29 15 ffvelrni ⊢ ( 𝑧 ∈ ( BaseSet ‘ 𝑈 ) → ( 𝑆 ‘ 𝑧 ) ∈ ( BaseSet ‘ 𝑊 ) )
30 5 6 8 3pm3.2i ⊢ ( 𝑊 ∈ NrmCVec ∧ 𝑋 ∈ NrmCVec ∧ 𝑇 ∈ 𝑀 )
31 eqid ⊢ ( +𝑣 ‘ 𝑊 ) = ( +𝑣 ‘ 𝑊 )
32 eqid ⊢ ( +𝑣 ‘ 𝑋 ) = ( +𝑣 ‘ 𝑋 )
33 eqid ⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
34 eqid ⊢ ( ·𝑠OLD ‘ 𝑋 ) = ( ·𝑠OLD ‘ 𝑋 )
35 9 10 31 32 33 34 2 lnolin ⊢ ( ( ( 𝑊 ∈ NrmCVec ∧ 𝑋 ∈ NrmCVec ∧ 𝑇 ∈ 𝑀 ) ∧ ( 𝑥 ∈ ℂ ∧ ( 𝑆 ‘ 𝑦 ) ∈ ( BaseSet ‘ 𝑊 ) ∧ ( 𝑆 ‘ 𝑧 ) ∈ ( BaseSet ‘ 𝑊 ) ) ) → ( 𝑇 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑆 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑆 ‘ 𝑧 ) ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑋 ) ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) ) ( +𝑣 ‘ 𝑋 ) ( 𝑇 ‘ ( 𝑆 ‘ 𝑧 ) ) ) )
36 30 35 mpan ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑆 ‘ 𝑦 ) ∈ ( BaseSet ‘ 𝑊 ) ∧ ( 𝑆 ‘ 𝑧 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( 𝑇 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑆 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑆 ‘ 𝑧 ) ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑋 ) ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) ) ( +𝑣 ‘ 𝑋 ) ( 𝑇 ‘ ( 𝑆 ‘ 𝑧 ) ) ) )
37 27 28 29 36 syl3an ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑇 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑆 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑆 ‘ 𝑧 ) ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑋 ) ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) ) ( +𝑣 ‘ 𝑋 ) ( 𝑇 ‘ ( 𝑆 ‘ 𝑧 ) ) ) )
38 4 5 7 3pm3.2i ⊢ ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑆 ∈ 𝐿 )
39 13 9 21 31 18 33 1 lnolin ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑆 ∈ 𝐿 ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝑆 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑆 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑆 ‘ 𝑧 ) ) )
40 38 39 mpan ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑆 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑆 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑆 ‘ 𝑧 ) ) )
41 40 fveq2d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑇 ‘ ( 𝑆 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ) ) = ( 𝑇 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑆 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑆 ‘ 𝑧 ) ) ) )
42 simp2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → 𝑦 ∈ ( BaseSet ‘ 𝑈 ) )
43 fvco3 ⊢ ( ( 𝑆 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) = ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) )
44 15 42 43 sylancr ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) = ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) )
45 44 oveq2d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑥 ( ·𝑠OLD ‘ 𝑋 ) ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) = ( 𝑥 ( ·𝑠OLD ‘ 𝑋 ) ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) ) )
46 simp3 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → 𝑧 ∈ ( BaseSet ‘ 𝑈 ) )
47 fvco3 ⊢ ( ( 𝑆 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑧 ) = ( 𝑇 ‘ ( 𝑆 ‘ 𝑧 ) ) )
48 15 46 47 sylancr ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑧 ) = ( 𝑇 ‘ ( 𝑆 ‘ 𝑧 ) ) )
49 45 48 oveq12d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑥 ( ·𝑠OLD ‘ 𝑋 ) ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑋 ) ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑋 ) ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) ) ( +𝑣 ‘ 𝑋 ) ( 𝑇 ‘ ( 𝑆 ‘ 𝑧 ) ) ) )
50 37 41 49 3eqtr4rd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑥 ( ·𝑠OLD ‘ 𝑋 ) ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑋 ) ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑧 ) ) = ( 𝑇 ‘ ( 𝑆 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ) ) )
51 26 50 eqtr4d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑇 ∘ 𝑆 ) ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑋 ) ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑋 ) ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑧 ) ) )
52 51 rgen3 ⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( ( 𝑇 ∘ 𝑆 ) ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑋 ) ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑋 ) ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑧 ) )
53 13 10 21 32 18 34 3 islno ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑋 ∈ NrmCVec ) → ( ( 𝑇 ∘ 𝑆 ) ∈ 𝑁 ↔ ( ( 𝑇 ∘ 𝑆 ) : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( ( 𝑇 ∘ 𝑆 ) ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑋 ) ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑋 ) ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑧 ) ) ) ) )
54 4 6 53 mp2an ⊢ ( ( 𝑇 ∘ 𝑆 ) ∈ 𝑁 ↔ ( ( 𝑇 ∘ 𝑆 ) : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( ( 𝑇 ∘ 𝑆 ) ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑋 ) ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑋 ) ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑧 ) ) ) )
55 17 52 54 mpbir2an ⊢ ( 𝑇 ∘ 𝑆 ) ∈ 𝑁