Theorem vcz

Description: Anything times the zero vector is the zero vector. Equation 1b of Kreyszig p. 51. (Contributed by NM, 24-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	vc0.1	⊢ 𝐺 = ( 1st ‘ 𝑊 )
	vc0.2	⊢ 𝑆 = ( 2nd ‘ 𝑊 )
	vc0.3	⊢ 𝑋 = ran 𝐺
	vc0.4	⊢ 𝑍 = ( GId ‘ 𝐺 )
Assertion	vcz	⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ ℂ ) → ( 𝐴 𝑆 𝑍 ) = 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		vc0.1	⊢ 𝐺 = ( 1st ‘ 𝑊 )
2		vc0.2	⊢ 𝑆 = ( 2nd ‘ 𝑊 )
3		vc0.3	⊢ 𝑋 = ran 𝐺
4		vc0.4	⊢ 𝑍 = ( GId ‘ 𝐺 )
5	1 3 4	vczcl	⊢ ( 𝑊 ∈ CVecOLD → 𝑍 ∈ 𝑋 )
6	5	anim2i	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑊 ∈ CVecOLD ) → ( 𝐴 ∈ ℂ ∧ 𝑍 ∈ 𝑋 ) )
7	6	ancoms	⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ ℂ ) → ( 𝐴 ∈ ℂ ∧ 𝑍 ∈ 𝑋 ) )
8		0cn	⊢ 0 ∈ ℂ
9	1 2 3	vcass	⊢ ( ( 𝑊 ∈ CVecOLD ∧ ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ∧ 𝑍 ∈ 𝑋 ) ) → ( ( 𝐴 · 0 ) 𝑆 𝑍 ) = ( 𝐴 𝑆 ( 0 𝑆 𝑍 ) ) )
10	8 9	mp3anr2	⊢ ( ( 𝑊 ∈ CVecOLD ∧ ( 𝐴 ∈ ℂ ∧ 𝑍 ∈ 𝑋 ) ) → ( ( 𝐴 · 0 ) 𝑆 𝑍 ) = ( 𝐴 𝑆 ( 0 𝑆 𝑍 ) ) )
11	7 10	syldan	⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ ℂ ) → ( ( 𝐴 · 0 ) 𝑆 𝑍 ) = ( 𝐴 𝑆 ( 0 𝑆 𝑍 ) ) )
12		mul01	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 0 ) = 0 )
13	12	oveq1d	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 · 0 ) 𝑆 𝑍 ) = ( 0 𝑆 𝑍 ) )
14	1 2 3 4	vc0	⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝑍 ∈ 𝑋 ) → ( 0 𝑆 𝑍 ) = 𝑍 )
15	5 14	mpdan	⊢ ( 𝑊 ∈ CVecOLD → ( 0 𝑆 𝑍 ) = 𝑍 )
16	13 15	sylan9eqr	⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ ℂ ) → ( ( 𝐴 · 0 ) 𝑆 𝑍 ) = 𝑍 )
17	15	oveq2d	⊢ ( 𝑊 ∈ CVecOLD → ( 𝐴 𝑆 ( 0 𝑆 𝑍 ) ) = ( 𝐴 𝑆 𝑍 ) )
18	17	adantr	⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ ℂ ) → ( 𝐴 𝑆 ( 0 𝑆 𝑍 ) ) = ( 𝐴 𝑆 𝑍 ) )
19	11 16 18	3eqtr3rd	⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ ℂ ) → ( 𝐴 𝑆 𝑍 ) = 𝑍 )