Metamath Proof Explorer

Theorem vc0

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

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

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 vc0rid ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 𝑍 ) = 𝐴 )
6 1p0e1 ⊢ ( 1 + 0 ) = 1
7 6 oveq1i ⊢ ( ( 1 + 0 ) 𝑆 𝐴 ) = ( 1 𝑆 𝐴 )
8 0cn ⊢ 0 ∈ ℂ
9 ax-1cn ⊢ 1 ∈ ℂ
10 1 2 3 vcdir ⊢ ( ( 𝑊 ∈ CVecOLD ∧ ( 1 ∈ ℂ ∧ 0 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 1 + 0 ) 𝑆 𝐴 ) = ( ( 1 𝑆 𝐴 ) 𝐺 ( 0 𝑆 𝐴 ) ) )
11 9 10 mp3anr1 ⊢ ( ( 𝑊 ∈ CVecOLD ∧ ( 0 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 1 + 0 ) 𝑆 𝐴 ) = ( ( 1 𝑆 𝐴 ) 𝐺 ( 0 𝑆 𝐴 ) ) )
12 8 11 mpanr1 ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 + 0 ) 𝑆 𝐴 ) = ( ( 1 𝑆 𝐴 ) 𝐺 ( 0 𝑆 𝐴 ) ) )
13 1 2 3 vcidOLD ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( 1 𝑆 𝐴 ) = 𝐴 )
14 7 12 13 3eqtr3a ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 𝑆 𝐴 ) 𝐺 ( 0 𝑆 𝐴 ) ) = 𝐴 )
15 13 oveq1d ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 𝑆 𝐴 ) 𝐺 ( 0 𝑆 𝐴 ) ) = ( 𝐴 𝐺 ( 0 𝑆 𝐴 ) ) )
16 5 14 15 3eqtr2rd ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 ( 0 𝑆 𝐴 ) ) = ( 𝐴 𝐺 𝑍 ) )
17 1 2 3 vccl ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 0 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( 0 𝑆 𝐴 ) ∈ 𝑋 )
18 8 17 mp3an2 ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( 0 𝑆 𝐴 ) ∈ 𝑋 )
19 1 3 4 vczcl ⊢ ( 𝑊 ∈ CVecOLD → 𝑍 ∈ 𝑋 )
20 19 adantr ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → 𝑍 ∈ 𝑋 )
21 simpr ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
22 18 20 21 3jca ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( 0 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) )
23 1 3 vclcan ⊢ ( ( 𝑊 ∈ CVecOLD ∧ ( ( 0 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 ( 0 𝑆 𝐴 ) ) = ( 𝐴 𝐺 𝑍 ) ↔ ( 0 𝑆 𝐴 ) = 𝑍 ) )
24 22 23 syldan ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( 0 𝑆 𝐴 ) ) = ( 𝐴 𝐺 𝑍 ) ↔ ( 0 𝑆 𝐴 ) = 𝑍 ) )
25 16 24 mpbid ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( 0 𝑆 𝐴 ) = 𝑍 )