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 \in NrmCVec$
	lnocoi.w	$⊢ W \in NrmCVec$
	lnocoi.x	$⊢ X \in NrmCVec$
	lnocoi.s	$⊢ S \in L$
	lnocoi.t	$⊢ T \in M$
Assertion	lnocoi	$⊢ T \circ S \in 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 \in NrmCVec$
5		lnocoi.w	$⊢ W \in NrmCVec$
6		lnocoi.x	$⊢ X \in NrmCVec$
7		lnocoi.s	$⊢ S \in L$
8		lnocoi.t	$⊢ T \in M$
9		eqid	$⊢ BaseSet (W) = BaseSet (W)$
10		eqid	$⊢ BaseSet (X) = BaseSet (X)$
11	9 10 2	lnof	$⊢ (W \in NrmCVec \land X \in NrmCVec \land T \in M) \to 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 \in NrmCVec \land W \in NrmCVec \land S \in L) \to S : BaseSet (U) ⟶ BaseSet (W)$
15	4 5 7 14	mp3an	$⊢ S : BaseSet (U) ⟶ BaseSet (W)$
16		fco	$⊢ (T : BaseSet (W) ⟶ BaseSet (X) \land S : BaseSet (U) ⟶ BaseSet (W)) \to (T \circ S) : BaseSet (U) ⟶ BaseSet (X)$
17	12 15 16	mp2an	$⊢ (T \circ S) : BaseSet (U) ⟶ BaseSet (X)$
18		eqid	$⊢ \cdot_{𝑠OLD} (U) = \cdot_{𝑠OLD} (U)$
19	13 18	nvscl	$⊢ (U \in NrmCVec \land x \in ℂ \land y \in BaseSet (U)) \to x \cdot_{𝑠OLD} (U) y \in BaseSet (U)$
20	4 19	mp3an1	$⊢ (x \in ℂ \land y \in BaseSet (U)) \to x \cdot_{𝑠OLD} (U) y \in BaseSet (U)$
21		eqid	$⊢ +_{v} (U) = +_{v} (U)$
22	13 21	nvgcl	$⊢ (U \in NrmCVec \land x \cdot_{𝑠OLD} (U) y \in BaseSet (U) \land z \in BaseSet (U)) \to (x \cdot_{𝑠OLD} (U) y) +_{v} (U) z \in BaseSet (U)$
23	4 22	mp3an1	$⊢ (x \cdot_{𝑠OLD} (U) y \in BaseSet (U) \land z \in BaseSet (U)) \to (x \cdot_{𝑠OLD} (U) y) +_{v} (U) z \in BaseSet (U)$
24	20 23	stoic3	$⊢ (x \in ℂ \land y \in BaseSet (U) \land z \in BaseSet (U)) \to (x \cdot_{𝑠OLD} (U) y) +_{v} (U) z \in BaseSet (U)$
25		fvco3	$⊢ (S : BaseSet (U) ⟶ BaseSet (W) \land (x \cdot_{𝑠OLD} (U) y) +_{v} (U) z \in BaseSet (U)) \to (T \circ S) ((x \cdot_{𝑠OLD} (U) y) +_{v} (U) z) = T (S ((x \cdot_{𝑠OLD} (U) y) +_{v} (U) z))$
26	15 24 25	sylancr	$⊢ (x \in ℂ \land y \in BaseSet (U) \land z \in BaseSet (U)) \to (T \circ S) ((x \cdot_{𝑠OLD} (U) y) +_{v} (U) z) = T (S ((x \cdot_{𝑠OLD} (U) y) +_{v} (U) z))$
27		id	$⊢ x \in ℂ \to x \in ℂ$
28	15	ffvelrni	$⊢ y \in BaseSet (U) \to S (y) \in BaseSet (W)$
29	15	ffvelrni	$⊢ z \in BaseSet (U) \to S (z) \in BaseSet (W)$
30	5 6 8	3pm3.2i	$⊢ (W \in NrmCVec \land X \in NrmCVec \land T \in M)$
31		eqid	$⊢ +_{v} (W) = +_{v} (W)$
32		eqid	$⊢ +_{v} (X) = +_{v} (X)$
33		eqid	$⊢ \cdot_{𝑠OLD} (W) = \cdot_{𝑠OLD} (W)$
34		eqid	$⊢ \cdot_{𝑠OLD} (X) = \cdot_{𝑠OLD} (X)$
35	9 10 31 32 33 34 2	lnolin	$⊢ ((W \in NrmCVec \land X \in NrmCVec \land T \in M) \land (x \in ℂ \land S (y) \in BaseSet (W) \land S (z) \in BaseSet (W))) \to T ((x \cdot_{𝑠OLD} (W) S (y)) +_{v} (W) S (z)) = (x \cdot_{𝑠OLD} (X) T (S (y))) +_{v} (X) T (S (z))$
36	30 35	mpan	$⊢ (x \in ℂ \land S (y) \in BaseSet (W) \land S (z) \in BaseSet (W)) \to T ((x \cdot_{𝑠OLD} (W) S (y)) +_{v} (W) S (z)) = (x \cdot_{𝑠OLD} (X) T (S (y))) +_{v} (X) T (S (z))$
37	27 28 29 36	syl3an	$⊢ (x \in ℂ \land y \in BaseSet (U) \land z \in BaseSet (U)) \to T ((x \cdot_{𝑠OLD} (W) S (y)) +_{v} (W) S (z)) = (x \cdot_{𝑠OLD} (X) T (S (y))) +_{v} (X) T (S (z))$
38	4 5 7	3pm3.2i	$⊢ (U \in NrmCVec \land W \in NrmCVec \land S \in L)$
39	13 9 21 31 18 33 1	lnolin	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land S \in L) \land (x \in ℂ \land y \in BaseSet (U) \land z \in BaseSet (U))) \to S ((x \cdot_{𝑠OLD} (U) y) +_{v} (U) z) = (x \cdot_{𝑠OLD} (W) S (y)) +_{v} (W) S (z)$
40	38 39	mpan	$⊢ (x \in ℂ \land y \in BaseSet (U) \land z \in BaseSet (U)) \to S ((x \cdot_{𝑠OLD} (U) y) +_{v} (U) z) = (x \cdot_{𝑠OLD} (W) S (y)) +_{v} (W) S (z)$
41	40	fveq2d	$⊢ (x \in ℂ \land y \in BaseSet (U) \land z \in BaseSet (U)) \to T (S ((x \cdot_{𝑠OLD} (U) y) +_{v} (U) z)) = T ((x \cdot_{𝑠OLD} (W) S (y)) +_{v} (W) S (z))$
42		simp2	$⊢ (x \in ℂ \land y \in BaseSet (U) \land z \in BaseSet (U)) \to y \in BaseSet (U)$
43		fvco3	$⊢ (S : BaseSet (U) ⟶ BaseSet (W) \land y \in BaseSet (U)) \to (T \circ S) (y) = T (S (y))$
44	15 42 43	sylancr	$⊢ (x \in ℂ \land y \in BaseSet (U) \land z \in BaseSet (U)) \to (T \circ S) (y) = T (S (y))$
45	44	oveq2d	$⊢ (x \in ℂ \land y \in BaseSet (U) \land z \in BaseSet (U)) \to x \cdot_{𝑠OLD} (X) (T \circ S) (y) = x \cdot_{𝑠OLD} (X) T (S (y))$
46		simp3	$⊢ (x \in ℂ \land y \in BaseSet (U) \land z \in BaseSet (U)) \to z \in BaseSet (U)$
47		fvco3	$⊢ (S : BaseSet (U) ⟶ BaseSet (W) \land z \in BaseSet (U)) \to (T \circ S) (z) = T (S (z))$
48	15 46 47	sylancr	$⊢ (x \in ℂ \land y \in BaseSet (U) \land z \in BaseSet (U)) \to (T \circ S) (z) = T (S (z))$
49	45 48	oveq12d	$⊢ (x \in ℂ \land y \in BaseSet (U) \land z \in BaseSet (U)) \to (x \cdot_{𝑠OLD} (X) (T \circ S) (y)) +_{v} (X) (T \circ S) (z) = (x \cdot_{𝑠OLD} (X) T (S (y))) +_{v} (X) T (S (z))$
50	37 41 49	3eqtr4rd	$⊢ (x \in ℂ \land y \in BaseSet (U) \land z \in BaseSet (U)) \to (x \cdot_{𝑠OLD} (X) (T \circ S) (y)) +_{v} (X) (T \circ S) (z) = T (S ((x \cdot_{𝑠OLD} (U) y) +_{v} (U) z))$
51	26 50	eqtr4d	$⊢ (x \in ℂ \land y \in BaseSet (U) \land z \in BaseSet (U)) \to (T \circ S) ((x \cdot_{𝑠OLD} (U) y) +_{v} (U) z) = (x \cdot_{𝑠OLD} (X) (T \circ S) (y)) +_{v} (X) (T \circ S) (z)$
52	51	rgen3	$⊢ \forall x \in ℂ \forall y \in BaseSet (U) \forall z \in BaseSet (U) (T \circ S) ((x \cdot_{𝑠OLD} (U) y) +_{v} (U) z) = (x \cdot_{𝑠OLD} (X) (T \circ S) (y)) +_{v} (X) (T \circ S) (z)$
53	13 10 21 32 18 34 3	islno	$⊢ (U \in NrmCVec \land X \in NrmCVec) \to (T \circ S \in N \leftrightarrow ((T \circ S) : BaseSet (U) ⟶ BaseSet (X) \land \forall x \in ℂ \forall y \in BaseSet (U) \forall z \in BaseSet (U) (T \circ S) ((x \cdot_{𝑠OLD} (U) y) +_{v} (U) z) = (x \cdot_{𝑠OLD} (X) (T \circ S) (y)) +_{v} (X) (T \circ S) (z)))$
54	4 6 53	mp2an	$⊢ T \circ S \in N \leftrightarrow ((T \circ S) : BaseSet (U) ⟶ BaseSet (X) \land \forall x \in ℂ \forall y \in BaseSet (U) \forall z \in BaseSet (U) (T \circ S) ((x \cdot_{𝑠OLD} (U) y) +_{v} (U) z) = (x \cdot_{𝑠OLD} (X) (T \circ S) (y)) +_{v} (X) (T \circ S) (z))$
55	17 52 54	mpbir2an	$⊢ T \circ S \in N$

Metamath Proof Explorer

Theorem lnocoi

Proof