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 
|- L = ( U LnOp W )
lnocoi.m 
|- M = ( W LnOp X )
lnocoi.n 
|- N = ( U LnOp X )
lnocoi.u 
|- U e. NrmCVec
lnocoi.w 
|- W e. NrmCVec
lnocoi.x 
|- X e. NrmCVec
lnocoi.s 
|- S e. L
lnocoi.t 
|- T e. M
Assertion lnocoi 
|- ( T o. S ) e. N

Proof

Step Hyp Ref Expression
1 lnocoi.l 
 |-  L = ( U LnOp W )
2 lnocoi.m 
 |-  M = ( W LnOp X )
3 lnocoi.n 
 |-  N = ( U LnOp X )
4 lnocoi.u 
 |-  U e. NrmCVec
5 lnocoi.w 
 |-  W e. NrmCVec
6 lnocoi.x 
 |-  X e. NrmCVec
7 lnocoi.s 
 |-  S e. L
8 lnocoi.t 
 |-  T e. M
9 eqid 
 |-  ( BaseSet ` W ) = ( BaseSet ` W )
10 eqid 
 |-  ( BaseSet ` X ) = ( BaseSet ` X )
11 9 10 2 lnof 
 |-  ( ( W e. NrmCVec /\ X e. NrmCVec /\ T e. M ) -> T : ( BaseSet ` W ) --> ( BaseSet ` X ) )
12 5 6 8 11 mp3an 
 |-  T : ( BaseSet ` W ) --> ( BaseSet ` X )
13 eqid 
 |-  ( BaseSet ` U ) = ( BaseSet ` U )
14 13 9 1 lnof 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ S e. L ) -> S : ( BaseSet ` U ) --> ( BaseSet ` W ) )
15 4 5 7 14 mp3an 
 |-  S : ( BaseSet ` U ) --> ( BaseSet ` W )
16 fco 
 |-  ( ( T : ( BaseSet ` W ) --> ( BaseSet ` X ) /\ S : ( BaseSet ` U ) --> ( BaseSet ` W ) ) -> ( T o. S ) : ( BaseSet ` U ) --> ( BaseSet ` X ) )
17 12 15 16 mp2an 
 |-  ( T o. S ) : ( BaseSet ` U ) --> ( BaseSet ` X )
18 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
19 13 18 nvscl 
 |-  ( ( U e. NrmCVec /\ x e. CC /\ y e. ( BaseSet ` U ) ) -> ( x ( .sOLD ` U ) y ) e. ( BaseSet ` U ) )
20 4 19 mp3an1 
 |-  ( ( x e. CC /\ y e. ( BaseSet ` U ) ) -> ( x ( .sOLD ` U ) y ) e. ( BaseSet ` U ) )
21 eqid 
 |-  ( +v ` U ) = ( +v ` U )
22 13 21 nvgcl 
 |-  ( ( U e. NrmCVec /\ ( x ( .sOLD ` U ) y ) e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) -> ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) e. ( BaseSet ` U ) )
23 4 22 mp3an1 
 |-  ( ( ( x ( .sOLD ` U ) y ) e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) -> ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) e. ( BaseSet ` U ) )
24 20 23 stoic3 
 |-  ( ( x e. CC /\ y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) -> ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) e. ( BaseSet ` U ) )
25 fvco3 
 |-  ( ( S : ( BaseSet ` U ) --> ( BaseSet ` W ) /\ ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) e. ( BaseSet ` U ) ) -> ( ( T o. S ) ` ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) ) = ( T ` ( S ` ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) ) ) )
26 15 24 25 sylancr 
 |-  ( ( x e. CC /\ y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) -> ( ( T o. S ) ` ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) ) = ( T ` ( S ` ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) ) ) )
27 id 
 |-  ( x e. CC -> x e. CC )
28 15 ffvelrni 
 |-  ( y e. ( BaseSet ` U ) -> ( S ` y ) e. ( BaseSet ` W ) )
29 15 ffvelrni 
 |-  ( z e. ( BaseSet ` U ) -> ( S ` z ) e. ( BaseSet ` W ) )
30 5 6 8 3pm3.2i 
 |-  ( W e. NrmCVec /\ X e. NrmCVec /\ T e. M )
31 eqid 
 |-  ( +v ` W ) = ( +v ` W )
32 eqid 
 |-  ( +v ` X ) = ( +v ` X )
33 eqid 
 |-  ( .sOLD ` W ) = ( .sOLD ` W )
34 eqid 
 |-  ( .sOLD ` X ) = ( .sOLD ` X )
35 9 10 31 32 33 34 2 lnolin 
 |-  ( ( ( W e. NrmCVec /\ X e. NrmCVec /\ T e. M ) /\ ( x e. CC /\ ( S ` y ) e. ( BaseSet ` W ) /\ ( S ` z ) e. ( BaseSet ` W ) ) ) -> ( T ` ( ( x ( .sOLD ` W ) ( S ` y ) ) ( +v ` W ) ( S ` z ) ) ) = ( ( x ( .sOLD ` X ) ( T ` ( S ` y ) ) ) ( +v ` X ) ( T ` ( S ` z ) ) ) )
36 30 35 mpan 
 |-  ( ( x e. CC /\ ( S ` y ) e. ( BaseSet ` W ) /\ ( S ` z ) e. ( BaseSet ` W ) ) -> ( T ` ( ( x ( .sOLD ` W ) ( S ` y ) ) ( +v ` W ) ( S ` z ) ) ) = ( ( x ( .sOLD ` X ) ( T ` ( S ` y ) ) ) ( +v ` X ) ( T ` ( S ` z ) ) ) )
37 27 28 29 36 syl3an 
 |-  ( ( x e. CC /\ y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) -> ( T ` ( ( x ( .sOLD ` W ) ( S ` y ) ) ( +v ` W ) ( S ` z ) ) ) = ( ( x ( .sOLD ` X ) ( T ` ( S ` y ) ) ) ( +v ` X ) ( T ` ( S ` z ) ) ) )
38 4 5 7 3pm3.2i 
 |-  ( U e. NrmCVec /\ W e. NrmCVec /\ S e. L )
39 13 9 21 31 18 33 1 lnolin 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ S e. L ) /\ ( x e. CC /\ y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) ) -> ( S ` ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) ) = ( ( x ( .sOLD ` W ) ( S ` y ) ) ( +v ` W ) ( S ` z ) ) )
40 38 39 mpan 
 |-  ( ( x e. CC /\ y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) -> ( S ` ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) ) = ( ( x ( .sOLD ` W ) ( S ` y ) ) ( +v ` W ) ( S ` z ) ) )
41 40 fveq2d 
 |-  ( ( x e. CC /\ y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) -> ( T ` ( S ` ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) ) ) = ( T ` ( ( x ( .sOLD ` W ) ( S ` y ) ) ( +v ` W ) ( S ` z ) ) ) )
42 simp2 
 |-  ( ( x e. CC /\ y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) -> y e. ( BaseSet ` U ) )
43 fvco3 
 |-  ( ( S : ( BaseSet ` U ) --> ( BaseSet ` W ) /\ y e. ( BaseSet ` U ) ) -> ( ( T o. S ) ` y ) = ( T ` ( S ` y ) ) )
44 15 42 43 sylancr 
 |-  ( ( x e. CC /\ y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) -> ( ( T o. S ) ` y ) = ( T ` ( S ` y ) ) )
45 44 oveq2d 
 |-  ( ( x e. CC /\ y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) -> ( x ( .sOLD ` X ) ( ( T o. S ) ` y ) ) = ( x ( .sOLD ` X ) ( T ` ( S ` y ) ) ) )
46 simp3 
 |-  ( ( x e. CC /\ y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) -> z e. ( BaseSet ` U ) )
47 fvco3 
 |-  ( ( S : ( BaseSet ` U ) --> ( BaseSet ` W ) /\ z e. ( BaseSet ` U ) ) -> ( ( T o. S ) ` z ) = ( T ` ( S ` z ) ) )
48 15 46 47 sylancr 
 |-  ( ( x e. CC /\ y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) -> ( ( T o. S ) ` z ) = ( T ` ( S ` z ) ) )
49 45 48 oveq12d 
 |-  ( ( x e. CC /\ y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) -> ( ( x ( .sOLD ` X ) ( ( T o. S ) ` y ) ) ( +v ` X ) ( ( T o. S ) ` z ) ) = ( ( x ( .sOLD ` X ) ( T ` ( S ` y ) ) ) ( +v ` X ) ( T ` ( S ` z ) ) ) )
50 37 41 49 3eqtr4rd 
 |-  ( ( x e. CC /\ y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) -> ( ( x ( .sOLD ` X ) ( ( T o. S ) ` y ) ) ( +v ` X ) ( ( T o. S ) ` z ) ) = ( T ` ( S ` ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) ) ) )
51 26 50 eqtr4d 
 |-  ( ( x e. CC /\ y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) -> ( ( T o. S ) ` ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) ) = ( ( x ( .sOLD ` X ) ( ( T o. S ) ` y ) ) ( +v ` X ) ( ( T o. S ) ` z ) ) )
52 51 rgen3 
 |-  A. x e. CC A. y e. ( BaseSet ` U ) A. z e. ( BaseSet ` U ) ( ( T o. S ) ` ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) ) = ( ( x ( .sOLD ` X ) ( ( T o. S ) ` y ) ) ( +v ` X ) ( ( T o. S ) ` z ) )
53 13 10 21 32 18 34 3 islno 
 |-  ( ( U e. NrmCVec /\ X e. NrmCVec ) -> ( ( T o. S ) e. N <-> ( ( T o. S ) : ( BaseSet ` U ) --> ( BaseSet ` X ) /\ A. x e. CC A. y e. ( BaseSet ` U ) A. z e. ( BaseSet ` U ) ( ( T o. S ) ` ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) ) = ( ( x ( .sOLD ` X ) ( ( T o. S ) ` y ) ) ( +v ` X ) ( ( T o. S ) ` z ) ) ) ) )
54 4 6 53 mp2an 
 |-  ( ( T o. S ) e. N <-> ( ( T o. S ) : ( BaseSet ` U ) --> ( BaseSet ` X ) /\ A. x e. CC A. y e. ( BaseSet ` U ) A. z e. ( BaseSet ` U ) ( ( T o. S ) ` ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) ) = ( ( x ( .sOLD ` X ) ( ( T o. S ) ` y ) ) ( +v ` X ) ( ( T o. S ) ` z ) ) ) )
55 17 52 54 mpbir2an 
 |-  ( T o. S ) e. N