lnolin

Description: Basic linearity property of a linear operator. (Contributed by NM, 4-Dec-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lnoval.1	$⊢ X = BaseSet (U)$
	lnoval.2	$⊢ Y = BaseSet (W)$
	lnoval.3	$⊢ G = +_{v} (U)$
	lnoval.4	$⊢ H = +_{v} (W)$
	lnoval.5	$⊢ R = \cdot_{𝑠OLD} (U)$
	lnoval.6	$⊢ S = \cdot_{𝑠OLD} (W)$
	lnoval.7	$⊢ L = U LnOp W$
Assertion	lnolin	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X \land C \in X)) \to T ((A R B) G C) = (A S T (B)) H T (C)$

Proof

Step	Hyp	Ref	Expression
1		lnoval.1	$⊢ X = BaseSet (U)$
2		lnoval.2	$⊢ Y = BaseSet (W)$
3		lnoval.3	$⊢ G = +_{v} (U)$
4		lnoval.4	$⊢ H = +_{v} (W)$
5		lnoval.5	$⊢ R = \cdot_{𝑠OLD} (U)$
6		lnoval.6	$⊢ S = \cdot_{𝑠OLD} (W)$
7		lnoval.7	$⊢ L = U LnOp W$
8	1 2 3 4 5 6 7	islno	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to (T \in L \leftrightarrow (T : X ⟶ Y \land \forall u \in ℂ \forall w \in X \forall t \in X T ((u R w) G t) = (u S T (w)) H T (t)))$
9	8	biimp3a	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in L) \to (T : X ⟶ Y \land \forall u \in ℂ \forall w \in X \forall t \in X T ((u R w) G t) = (u S T (w)) H T (t))$
10	9	simprd	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in L) \to \forall u \in ℂ \forall w \in X \forall t \in X T ((u R w) G t) = (u S T (w)) H T (t)$
11		oveq1	$⊢ u = A \to u R w = A R w$
12	11	fvoveq1d	$⊢ u = A \to T ((u R w) G t) = T ((A R w) G t)$
13		oveq1	$⊢ u = A \to u S T (w) = A S T (w)$
14	13	oveq1d	$⊢ u = A \to (u S T (w)) H T (t) = (A S T (w)) H T (t)$
15	12 14	eqeq12d	$⊢ u = A \to (T ((u R w) G t) = (u S T (w)) H T (t) \leftrightarrow T ((A R w) G t) = (A S T (w)) H T (t))$
16		oveq2	$⊢ w = B \to A R w = A R B$
17	16	fvoveq1d	$⊢ w = B \to T ((A R w) G t) = T ((A R B) G t)$
18		fveq2	$⊢ w = B \to T (w) = T (B)$
19	18	oveq2d	$⊢ w = B \to A S T (w) = A S T (B)$
20	19	oveq1d	$⊢ w = B \to (A S T (w)) H T (t) = (A S T (B)) H T (t)$
21	17 20	eqeq12d	$⊢ w = B \to (T ((A R w) G t) = (A S T (w)) H T (t) \leftrightarrow T ((A R B) G t) = (A S T (B)) H T (t))$
22		oveq2	$⊢ t = C \to (A R B) G t = (A R B) G C$
23	22	fveq2d	$⊢ t = C \to T ((A R B) G t) = T ((A R B) G C)$
24		fveq2	$⊢ t = C \to T (t) = T (C)$
25	24	oveq2d	$⊢ t = C \to (A S T (B)) H T (t) = (A S T (B)) H T (C)$
26	23 25	eqeq12d	$⊢ t = C \to (T ((A R B) G t) = (A S T (B)) H T (t) \leftrightarrow T ((A R B) G C) = (A S T (B)) H T (C))$
27	15 21 26	rspc3v	$⊢ (A \in ℂ \land B \in X \land C \in X) \to (\forall u \in ℂ \forall w \in X \forall t \in X T ((u R w) G t) = (u S T (w)) H T (t) \to T ((A R B) G C) = (A S T (B)) H T (C))$
28	10 27	mpan9	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X \land C \in X)) \to T ((A R B) G C) = (A S T (B)) H T (C)$

Metamath Proof Explorer

Theorem lnolin

Proof