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 ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ‘ 𝑄 ) = 𝑍 )