Metamath Proof Explorer

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 ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( 𝐴 𝑅 𝐵 ) ) = ( 𝐴 𝑆 ( 𝑇 ‘ 𝐵 ) ) )