lnomul

Description: Scalar multiplication property of a linear operator. (Contributed by NM, 5-Dec-2007) (Revised by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lnomul.1	$⊢ X = BaseSet (U)$
	lnomul.5	$⊢ R = \cdot_{𝑠OLD} (U)$
	lnomul.6	$⊢ S = \cdot_{𝑠OLD} (W)$
	lnomul.7	$⊢ L = U LnOp W$
Assertion	lnomul	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X)) \to T (A R B) = A S T (B)$

Proof

Step	Hyp	Ref	Expression
1		lnomul.1	$⊢ X = BaseSet (U)$
2		lnomul.5	$⊢ R = \cdot_{𝑠OLD} (U)$
3		lnomul.6	$⊢ S = \cdot_{𝑠OLD} (W)$
4		lnomul.7	$⊢ L = U LnOp W$
5		simpl	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X)) \to (U \in NrmCVec \land W \in NrmCVec \land T \in L)$
6		simprl	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X)) \to A \in ℂ$
7		simprr	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X)) \to B \in X$
8		simpl1	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X)) \to U \in NrmCVec$
9		eqid	$⊢ 0_{vec} (U) = 0_{vec} (U)$
10	1 9	nvzcl	$⊢ U \in NrmCVec \to 0_{vec} (U) \in X$
11	8 10	syl	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X)) \to 0_{vec} (U) \in X$
12		eqid	$⊢ BaseSet (W) = BaseSet (W)$
13		eqid	$⊢ +_{v} (U) = +_{v} (U)$
14		eqid	$⊢ +_{v} (W) = +_{v} (W)$
15	1 12 13 14 2 3 4	lnolin	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X \land 0_{vec} (U) \in X)) \to T ((A R B) +_{v} (U) 0_{vec} (U)) = (A S T (B)) +_{v} (W) T (0_{vec} (U))$
16	5 6 7 11 15	syl13anc	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X)) \to T ((A R B) +_{v} (U) 0_{vec} (U)) = (A S T (B)) +_{v} (W) T (0_{vec} (U))$
17	1 2	nvscl	$⊢ (U \in NrmCVec \land A \in ℂ \land B \in X) \to A R B \in X$
18	8 6 7 17	syl3anc	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X)) \to A R B \in X$
19	1 13 9	nv0rid	$⊢ (U \in NrmCVec \land A R B \in X) \to (A R B) +_{v} (U) 0_{vec} (U) = A R B$
20	8 18 19	syl2anc	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X)) \to (A R B) +_{v} (U) 0_{vec} (U) = A R B$
21	20	fveq2d	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X)) \to T ((A R B) +_{v} (U) 0_{vec} (U)) = T (A R B)$
22		eqid	$⊢ 0_{vec} (W) = 0_{vec} (W)$
23	1 12 9 22 4	lno0	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in L) \to T (0_{vec} (U)) = 0_{vec} (W)$
24	23	oveq2d	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in L) \to (A S T (B)) +_{v} (W) T (0_{vec} (U)) = (A S T (B)) +_{v} (W) 0_{vec} (W)$
25	24	adantr	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X)) \to (A S T (B)) +_{v} (W) T (0_{vec} (U)) = (A S T (B)) +_{v} (W) 0_{vec} (W)$
26		simpl2	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X)) \to W \in NrmCVec$
27	1 12 4	lnof	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in L) \to T : X ⟶ BaseSet (W)$
28	27	adantr	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X)) \to T : X ⟶ BaseSet (W)$
29	28 7	ffvelcdmd	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X)) \to T (B) \in BaseSet (W)$
30	12 3	nvscl	$⊢ (W \in NrmCVec \land A \in ℂ \land T (B) \in BaseSet (W)) \to A S T (B) \in BaseSet (W)$
31	26 6 29 30	syl3anc	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X)) \to A S T (B) \in BaseSet (W)$
32	12 14 22	nv0rid	$⊢ (W \in NrmCVec \land A S T (B) \in BaseSet (W)) \to (A S T (B)) +_{v} (W) 0_{vec} (W) = A S T (B)$
33	26 31 32	syl2anc	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X)) \to (A S T (B)) +_{v} (W) 0_{vec} (W) = A S T (B)$
34	25 33	eqtrd	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X)) \to (A S T (B)) +_{v} (W) T (0_{vec} (U)) = A S T (B)$
35	16 21 34	3eqtr3d	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (A \in ℂ \land B \in X)) \to T (A R B) = A S T (B)$

Metamath Proof Explorer

Theorem lnomul

Proof