Metamath Proof Explorer

Theorem lno0

Description: The value of a linear operator at zero is zero. (Contributed by NM, 4-Dec-2007) (Revised by Mario Carneiro, 18-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses lno0.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
lno0.2 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
lno0.5 ⊢ 𝑄 = ( 0vec ‘ 𝑈 )
lno0.z ⊢ 𝑍 = ( 0vec ‘ 𝑊 )
lno0.7 ⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
Assertion lno0 ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ‘ 𝑄 ) = 𝑍 )

Proof

Step Hyp Ref Expression
1 lno0.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 lno0.2 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3 lno0.5 ⊢ 𝑄 = ( 0vec ‘ 𝑈 )
4 lno0.z ⊢ 𝑍 = ( 0vec ‘ 𝑊 )
5 lno0.7 ⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
6 neg1cn ⊢ - 1 ∈ ℂ
7 6 a1i ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → - 1 ∈ ℂ )
8 1 3 nvzcl ⊢ ( 𝑈 ∈ NrmCVec → 𝑄 ∈ 𝑋 )
9 8 3ad2ant1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑄 ∈ 𝑋 )
10 7 9 9 3jca ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( - 1 ∈ ℂ ∧ 𝑄 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) )
11 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
12 eqid ⊢ ( +𝑣 ‘ 𝑊 ) = ( +𝑣 ‘ 𝑊 )
13 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
14 eqid ⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
15 1 2 11 12 13 14 5 lnolin ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( - 1 ∈ ℂ ∧ 𝑄 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑄 ) ( +𝑣 ‘ 𝑈 ) 𝑄 ) ) = ( ( - 1 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝑄 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑄 ) ) )
16 10 15 mpdan ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ‘ ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑄 ) ( +𝑣 ‘ 𝑈 ) 𝑄 ) ) = ( ( - 1 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝑄 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑄 ) ) )
17 1 11 13 3 nvlinv ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑄 ∈ 𝑋 ) → ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑄 ) ( +𝑣 ‘ 𝑈 ) 𝑄 ) = 𝑄 )
18 8 17 mpdan ⊢ ( 𝑈 ∈ NrmCVec → ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑄 ) ( +𝑣 ‘ 𝑈 ) 𝑄 ) = 𝑄 )
19 18 fveq2d ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑇 ‘ ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑄 ) ( +𝑣 ‘ 𝑈 ) 𝑄 ) ) = ( 𝑇 ‘ 𝑄 ) )
20 19 3ad2ant1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ‘ ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑄 ) ( +𝑣 ‘ 𝑈 ) 𝑄 ) ) = ( 𝑇 ‘ 𝑄 ) )
21 simp2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑊 ∈ NrmCVec )
22 1 2 5 lnof ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑇 : 𝑋 ⟶ 𝑌 )
23 22 9 ffvelcdmd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ‘ 𝑄 ) ∈ 𝑌 )
24 2 12 14 4 nvlinv ⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑇 ‘ 𝑄 ) ∈ 𝑌 ) → ( ( - 1 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝑄 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑄 ) ) = 𝑍 )
25 21 23 24 syl2anc ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( ( - 1 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝑄 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑄 ) ) = 𝑍 )
26 16 20 25 3eqtr3d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ‘ 𝑄 ) = 𝑍 )