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