Metamath Proof Explorer

Theorem lnoadd

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

Ref Expression
Hypotheses lnoadd.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
lnoadd.5 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
lnoadd.6 ⊢ 𝐻 = ( +𝑣 ‘ 𝑊 )
lnoadd.7 ⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
Assertion lnoadd ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( 𝐴 𝐺 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) 𝐻 ( 𝑇 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 lnoadd.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 lnoadd.5 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 lnoadd.6 ⊢ 𝐻 = ( +𝑣 ‘ 𝑊 )
4 lnoadd.7 ⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
5 ax-1cn ⊢ 1 ∈ ℂ
6 eqid ⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
7 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
8 eqid ⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
9 1 6 2 3 7 8 4 lnolin ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( ( 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) 𝐺 𝐵 ) ) = ( ( 1 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) 𝐻 ( 𝑇 ‘ 𝐵 ) ) )
10 5 9 mp3anr1 ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( ( 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) 𝐺 𝐵 ) ) = ( ( 1 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) 𝐻 ( 𝑇 ‘ 𝐵 ) ) )
11 simp1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑈 ∈ NrmCVec )
12 simpl ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
13 1 7 nvsid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) = 𝐴 )
14 11 12 13 syl2an ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) = 𝐴 )
15 14 fvoveq1d ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( ( 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) 𝐺 𝐵 ) ) = ( 𝑇 ‘ ( 𝐴 𝐺 𝐵 ) ) )
16 simpl2 ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝑊 ∈ NrmCVec )
17 1 6 4 lnof ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
18 ffvelcdm ⊢ ( ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝑇 ‘ 𝐴 ) ∈ ( BaseSet ‘ 𝑊 ) )
19 17 12 18 syl2an ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑇 ‘ 𝐴 ) ∈ ( BaseSet ‘ 𝑊 ) )
20 6 8 nvsid ⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑇 ‘ 𝐴 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( 1 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) = ( 𝑇 ‘ 𝐴 ) )
21 16 19 20 syl2anc ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 1 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) = ( 𝑇 ‘ 𝐴 ) )
22 21 oveq1d ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 1 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) 𝐻 ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) 𝐻 ( 𝑇 ‘ 𝐵 ) ) )
23 10 15 22 3eqtr3d ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( 𝐴 𝐺 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) 𝐻 ( 𝑇 ‘ 𝐵 ) ) )