This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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