Theorem lnosub

Description: Subtraction 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	lnosub.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	lnosub.5	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
	lnosub.6	⊢ 𝑁 = ( −𝑣 ‘ 𝑊 )
	lnosub.7	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
Assertion	lnosub	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( 𝐴 𝑀 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) 𝑁 ( 𝑇 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lnosub.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		lnosub.5	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3		lnosub.6	⊢ 𝑁 = ( −𝑣 ‘ 𝑊 )
4		lnosub.7	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
5		neg1cn	⊢ - 1 ∈ ℂ
6		eqid	⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
7		eqid	⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
8		eqid	⊢ ( +𝑣 ‘ 𝑊 ) = ( +𝑣 ‘ 𝑊 )
9		eqid	⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
10		eqid	⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
11	1 6 7 8 9 10 4	lnolin	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( - 1 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ( +𝑣 ‘ 𝑈 ) 𝐴 ) ) = ( ( - 1 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐵 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) )
12	5 11	mp3anr1	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ( +𝑣 ‘ 𝑈 ) 𝐴 ) ) = ( ( - 1 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐵 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) )
13	12	ancom2s	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ( +𝑣 ‘ 𝑈 ) 𝐴 ) ) = ( ( - 1 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐵 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) )
14	1 7 9 2	nvmval2	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐵 ) = ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ( +𝑣 ‘ 𝑈 ) 𝐴 ) )
15	14	3expb	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝑀 𝐵 ) = ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ( +𝑣 ‘ 𝑈 ) 𝐴 ) )
16	15	3ad2antl1	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝑀 𝐵 ) = ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ( +𝑣 ‘ 𝑈 ) 𝐴 ) )
17	16	fveq2d	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( 𝐴 𝑀 𝐵 ) ) = ( 𝑇 ‘ ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ( +𝑣 ‘ 𝑈 ) 𝐴 ) ) )
18		simpl2	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝑊 ∈ NrmCVec )
19	1 6 4	lnof	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
20		simpl	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
21		ffvelcdm	⊢ ( ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝑇 ‘ 𝐴 ) ∈ ( BaseSet ‘ 𝑊 ) )
22	19 20 21	syl2an	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑇 ‘ 𝐴 ) ∈ ( BaseSet ‘ 𝑊 ) )
23		simpr	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
24		ffvelcdm	⊢ ( ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝐵 ∈ 𝑋 ) → ( 𝑇 ‘ 𝐵 ) ∈ ( BaseSet ‘ 𝑊 ) )
25	19 23 24	syl2an	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑇 ‘ 𝐵 ) ∈ ( BaseSet ‘ 𝑊 ) )
26	6 8 10 3	nvmval2	⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑇 ‘ 𝐴 ) ∈ ( BaseSet ‘ 𝑊 ) ∧ ( 𝑇 ‘ 𝐵 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( ( 𝑇 ‘ 𝐴 ) 𝑁 ( 𝑇 ‘ 𝐵 ) ) = ( ( - 1 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐵 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) )
27	18 22 25 26	syl3anc	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝑇 ‘ 𝐴 ) 𝑁 ( 𝑇 ‘ 𝐵 ) ) = ( ( - 1 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐵 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) )
28	13 17 27	3eqtr4d	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( 𝐴 𝑀 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) 𝑁 ( 𝑇 ‘ 𝐵 ) ) )