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 ffvelrn ( ( 𝑇 : 𝑋 ⟶ ( 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 ∧ 𝑇𝐿 ) ∧ ( 𝐴𝑋𝐵𝑋 ) ) → ( 𝑇 ‘ ( 𝐴 𝐺 𝐵 ) ) = ( ( 𝑇𝐴 ) 𝐻 ( 𝑇𝐵 ) ) )