Theorem 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	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	lnomul.5	⊢ 𝑅 = ( ·𝑠OLD ‘ 𝑈 )
	lnomul.6	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑊 )
	lnomul.7	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
Assertion	lnomul	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( 𝐴 𝑅 𝐵 ) ) = ( 𝐴 𝑆 ( 𝑇 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lnomul.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		lnomul.5	⊢ 𝑅 = ( ·𝑠OLD ‘ 𝑈 )
3		lnomul.6	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑊 )
4		lnomul.7	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
5		simpl	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) )
6		simprl	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → 𝐴 ∈ ℂ )
7		simprr	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 )
8		simpl1	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → 𝑈 ∈ NrmCVec )
9		eqid	⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
10	1 9	nvzcl	⊢ ( 𝑈 ∈ NrmCVec → ( 0vec ‘ 𝑈 ) ∈ 𝑋 )
11	8 10	syl	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( 0vec ‘ 𝑈 ) ∈ 𝑋 )
12		eqid	⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
13		eqid	⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
14		eqid	⊢ ( +𝑣 ‘ 𝑊 ) = ( +𝑣 ‘ 𝑊 )
15	1 12 13 14 2 3 4	lnolin	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ ( 0vec ‘ 𝑈 ) ∈ 𝑋 ) ) → ( 𝑇 ‘ ( ( 𝐴 𝑅 𝐵 ) ( +𝑣 ‘ 𝑈 ) ( 0vec ‘ 𝑈 ) ) ) = ( ( 𝐴 𝑆 ( 𝑇 ‘ 𝐵 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) )
16	5 6 7 11 15	syl13anc	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( ( 𝐴 𝑅 𝐵 ) ( +𝑣 ‘ 𝑈 ) ( 0vec ‘ 𝑈 ) ) ) = ( ( 𝐴 𝑆 ( 𝑇 ‘ 𝐵 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) )
17	1 2	nvscl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑅 𝐵 ) ∈ 𝑋 )
18	8 6 7 17	syl3anc	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝑅 𝐵 ) ∈ 𝑋 )
19	1 13 9	nv0rid	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝑅 𝐵 ) ∈ 𝑋 ) → ( ( 𝐴 𝑅 𝐵 ) ( +𝑣 ‘ 𝑈 ) ( 0vec ‘ 𝑈 ) ) = ( 𝐴 𝑅 𝐵 ) )
20	8 18 19	syl2anc	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝑅 𝐵 ) ( +𝑣 ‘ 𝑈 ) ( 0vec ‘ 𝑈 ) ) = ( 𝐴 𝑅 𝐵 ) )
21	20	fveq2d	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( ( 𝐴 𝑅 𝐵 ) ( +𝑣 ‘ 𝑈 ) ( 0vec ‘ 𝑈 ) ) ) = ( 𝑇 ‘ ( 𝐴 𝑅 𝐵 ) ) )
22		eqid	⊢ ( 0vec ‘ 𝑊 ) = ( 0vec ‘ 𝑊 )
23	1 12 9 22 4	lno0	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) = ( 0vec ‘ 𝑊 ) )
24	23	oveq2d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( ( 𝐴 𝑆 ( 𝑇 ‘ 𝐵 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) = ( ( 𝐴 𝑆 ( 𝑇 ‘ 𝐵 ) ) ( +𝑣 ‘ 𝑊 ) ( 0vec ‘ 𝑊 ) ) )
25	24	adantr	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝑆 ( 𝑇 ‘ 𝐵 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) = ( ( 𝐴 𝑆 ( 𝑇 ‘ 𝐵 ) ) ( +𝑣 ‘ 𝑊 ) ( 0vec ‘ 𝑊 ) ) )
26		simpl2	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → 𝑊 ∈ NrmCVec )
27	1 12 4	lnof	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
28	27	adantr	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
29	28 7	ffvelcdmd	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑇 ‘ 𝐵 ) ∈ ( BaseSet ‘ 𝑊 ) )
30	12 3	nvscl	⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ ( 𝑇 ‘ 𝐵 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( 𝐴 𝑆 ( 𝑇 ‘ 𝐵 ) ) ∈ ( BaseSet ‘ 𝑊 ) )
31	26 6 29 30	syl3anc	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝑆 ( 𝑇 ‘ 𝐵 ) ) ∈ ( BaseSet ‘ 𝑊 ) )
32	12 14 22	nv0rid	⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝐴 𝑆 ( 𝑇 ‘ 𝐵 ) ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( ( 𝐴 𝑆 ( 𝑇 ‘ 𝐵 ) ) ( +𝑣 ‘ 𝑊 ) ( 0vec ‘ 𝑊 ) ) = ( 𝐴 𝑆 ( 𝑇 ‘ 𝐵 ) ) )
33	26 31 32	syl2anc	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝑆 ( 𝑇 ‘ 𝐵 ) ) ( +𝑣 ‘ 𝑊 ) ( 0vec ‘ 𝑊 ) ) = ( 𝐴 𝑆 ( 𝑇 ‘ 𝐵 ) ) )
34	25 33	eqtrd	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝑆 ( 𝑇 ‘ 𝐵 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) = ( 𝐴 𝑆 ( 𝑇 ‘ 𝐵 ) ) )
35	16 21 34	3eqtr3d	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( 𝐴 𝑅 𝐵 ) ) = ( 𝐴 𝑆 ( 𝑇 ‘ 𝐵 ) ) )