Theorem lnocoi 8418

Description: The composition of two linear operators is linear.

Hypotheses

Ref	Expression
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

Ref	Expression
lnocoi	|- (T o. S) e. N

Proof of Theorem lnocoi

Step	Hyp	Ref	Expression
1		lnocoi.u	. . 3 |- U e. NrmCVec
2		lnocoi.x	. . 3 |- X e. NrmCVec
3		eqid 1475	. . . 4 |- (Base` U) = (Base` U)
4		eqid 1475	. . . 4 |- (Base` X) = (Base` X)
5		eqid 1475	. . . 4 |- (+v` U) = (+v` U)
6		eqid 1475	. . . 4 |- (+v` X) = (+v` X)
7		eqid 1475	. . . 4 |- (.s` U) = (.s` U)
8		eqid 1475	. . . 4 |- (.s` X) = (.s` X)
9		lnocoi.n	. . . 4 |- N = (U LnOp X)
10	3, 4, 5, 6, 7, 8, 9	islno 8414	. . 3 |- ((U e. NrmCVec /\ X e. NrmCVec) -> ((T o. S) e. N <-> ((T o. S):(Base` U)-->(Base` X) /\ A.x e. (Base` U)A.y e. CC A.z e. (Base` U)((T o. S)` (x(+v` U)(y(.s` U)z))) = (((T o. S)` x)(+v` X)(y(.s` X)((T o. S)` z))))))
11	1, 2, 10	mp2an 697	. 2 |- ((T o. S) e. N <-> ((T o. S):(Base` U)-->(Base` X) /\ A.x e. (Base` U)A.y e. CC A.z e. (Base` U)((T o. S)` (x(+v` U)(y(.s` U)z))) = (((T o. S)` x)(+v` X)(y(.s` X)((T o. S)` z)))))
12		lnocoi.w	. . . 4 |- W e. NrmCVec
13		lnocoi.t	. . . 4 |- T e. M
14		eqid 1475	. . . . 5 |- (Base` W) = (Base` W)
15		lnocoi.m	. . . . 5 |- M = (W LnOp X)
16	14, 4, 15	lnof 8416	. . . 4 |- ((W e. NrmCVec /\ X e. NrmCVec /\ T e. M) -> T:(Base` W)-->(Base` X))
17	12, 2, 13, 16	mp3an 916	. . 3 |- T:(Base` W)-->(Base` X)
18		lnocoi.s	. . . 4 |- S e. L
19		lnocoi.l	. . . . 5 |- L = (U LnOp W)
20	3, 14, 19	lnof 8416	. . . 4 |- ((U e. NrmCVec /\ W e. NrmCVec /\ S e. L) -> S:(Base` U)-->(Base` W))
21	1, 12, 18, 20	mp3an 916	. . 3 |- S:(Base` U)-->(Base` W)
22		fco 3636	. . 3 |- ((T:(Base` W)-->(Base` X) /\ S:(Base` U)-->(Base` W)) -> (T o. S):(Base` U)-->(Base` X))
23	17, 21, 22	mp2an 697	. 2 |- (T o. S):(Base` U)-->(Base` X)
24	3, 5	nvgcl 8239	. . . . . . . . 9 |- ((U e. NrmCVec /\ x e. (Base` U) /\ (y(.s` U)z) e. (Base` U)) -> (x(+v` U)(y(.s` U)z)) e. (Base` U))
25	1, 24	mp3an1 903	. . . . . . . 8 |- ((x e. (Base` U) /\ (y(.s` U)z) e. (Base` U)) -> (x(+v` U)(y(.s` U)z)) e. (Base` U))
26	3, 7	nvscl 8247	. . . . . . . . 9 |- ((U e. NrmCVec /\ y e. CC /\ z e. (Base` U)) -> (y(.s` U)z) e. (Base` U))
27	1, 26	mp3an1 903	. . . . . . . 8 |- ((y e. CC /\ z e. (Base` U)) -> (y(.s` U)z) e. (Base` U))
28	25, 27	sylan2 451	. . . . . . 7 |- ((x e. (Base` U) /\ (y e. CC /\ z e. (Base` U))) -> (x(+v` U)(y(.s` U)z)) e. (Base` U))
29	28	3impb 829	. . . . . 6 |- ((x e. (Base` U) /\ y e. CC /\ z e. (Base` U)) -> (x(+v` U)(y(.s` U)z)) e. (Base` U))
30		ffun 3629	. . . . . . . 8 |- (T:(Base` W)-->(Base` X) -> Fun T)
31	17, 30	ax-mp 7	. . . . . . 7 |- Fun T
32		fvco3 3776	. . . . . . 7 |- ((Fun T /\ S:(Base` U)-->(Base` W) /\ (x(+v` U)(y(.s` U)z)) e. (Base` U)) -> ((T o. S)` (x(+v` U)(y(.s` U)z))) = (T` (S` (x(+v` U)(y(.s` U)z)))))
33	31, 21, 32	mp3an12 906	. . . . . 6 |- ((x(+v` U)(y(.s` U)z)) e. (Base` U) -> ((T o. S)` (x(+v` U)(y(.s` U)z))) = (T` (S` (x(+v` U)(y(.s` U)z)))))
34	29, 33	syl 10	. . . . 5 |- ((x e. (Base` U) /\ y e. CC /\ z e. (Base` U)) -> ((T o. S)` (x(+v` U)(y(.s` U)z))) = (T` (S` (x(+v` U)(y(.s` U)z)))))
35	1, 12, 18	3pm3.2i 818	. . . . . . 7 |- (U e. NrmCVec /\ W e. NrmCVec /\ S e. L)
36		eqid 1475	. . . . . . . 8 |- (+v` W) = (+v` W)
37		eqid 1475	. . . . . . . 8 |- (.s` W) = (.s` W)
38	3, 14, 5, 36, 7, 37, 19	lnolin 8415	. . . . . . 7 |- (((U e. NrmCVec /\ W e. NrmCVec /\ S e. L) /\ (x e. (Base` U) /\ y e. CC /\ z e. (Base` U))) -> (S` (x(+v` U)(y(.s` U)z))) = ((S` x)(+v` W)(y(.s` W)(S` z))))
39	35, 38	mpan 695	. . . . . 6 |- ((x e. (Base` U) /\ y e. CC /\ z e. (Base` U)) -> (S` (x(+v` U)(y(.s` U)z))) = ((S` x)(+v` W)(y(.s` W)(S` z))))
40	39	fveq2d 3728	. . . . 5 |- ((x e. (Base` U) /\ y e. CC /\ z e. (Base` U)) -> (T` (S` (x(+v` U)(y(.s` U)z)))) = (T` ((S` x)(+v` W)(y(.s` W)(S` z)))))
41	12, 2, 13	3pm3.2i 818	. . . . . . 7 |- (W e. NrmCVec /\ X e. NrmCVec /\ T e. M)
42	14, 4, 36, 6, 37, 8, 15	lnolin 8415	. . . . . . 7 |- (((W e. NrmCVec /\ X e. NrmCVec /\ T e. M) /\ ((S` x) e. (Base` W) /\ y e. CC /\ (S` z) e. (Base` W))) -> (T` ((S` x)(+v` W)(y(.s` W)(S` z)))) = ((T` (S` x))(+v` X)(y(.s` X)(T` (S` z)))))
43	41, 42	mpan 695	. . . . . 6 |- (((S` x) e. (Base` W) /\ y e. CC /\ (S` z) e. (Base` W)) -> (T` ((S` x)(+v` W)(y(.s` W)(S` z)))) = ((T` (S` x))(+v` X)(y(.s` X)(T` (S` z)))))
44	21	ffvelrni 3815	. . . . . 6 |- (x e. (Base` U) -> (S` x) e. (Base` W))
45		id 59	. . . . . 6 |- (y e. CC -> y e. CC)
46	21	ffvelrni 3815	. . . . . 6 |- (z e. (Base` U) -> (S` z) e. (Base` W))
47	43, 44, 45, 46	syl3an 868	. . . . 5 |- ((x e. (Base` U) /\ y e. CC /\ z e. (Base` U)) -> (T` ((S` x)(+v` W)(y(.s` W)(S` z)))) = ((T` (S` x))(+v` X)(y(.s` X)(T` (S` z)))))
48	34, 40, 47	3eqtrd 1511	. . . 4 |- ((x e. (Base` U) /\ y e. CC /\ z e. (Base` U)) -> ((T o. S)` (x(+v` U)(y(.s` U)z))) = ((T` (S` x))(+v` X)(y(.s` X)(T` (S` z)))))
49		fvco3 3776	. . . . . . 7 |- ((Fun T /\ S:(Base` U)-->(Base` W) /\ x e. (Base` U)) -> ((T o. S)` x) = (T` (S` x)))
50	31, 21, 49	mp3an12 906	. . . . . 6 |- (x e. (Base` U) -> ((T o. S)` x) = (T` (S` x)))
51		fvco3 3776	. . . . . . . . 9 |- ((Fun T /\ S:(Base` U)-->(Base` W) /\ z e. (Base` U)) -> ((T o. S)` z) = (T` (S` z)))
52	31, 21, 51	mp3an12 906	. . . . . . . 8 |- (z e. (Base` U) -> ((T o. S)` z) = (T` (S` z)))
53	52	opreq2d 3976	. . . . . . 7 |- (z e. (Base` U) -> (y(.s` X)((T o. S)` z)) = (y(.s` X)(T` (S` z))))
54	53	adantl 388	. . . . . 6 |- ((y e. CC /\ z e. (Base` U)) -> (y(.s` X)((T o. S)` z)) = (y(.s` X)(T` (S` z))))
55	50, 54	opreqan12d 3979	. . . . 5 |- ((x e. (Base` U) /\ (y e. CC /\ z e. (Base` U))) -> (((T o. S)` x)(+v` X)(y(.s` X)((T o. S)` z))) = ((