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 ⊢G=1st⁡W
vc0.2 ⊢S=2nd⁡W
vc0.3 ⊢X=ran⁡G
vc0.4 ⊢Z=GId⁡G
Assertion vc0 ⊢W∈CVecOLD∧A∈X→0SA=Z

Proof

Step Hyp Ref Expression
1 vc0.1 ⊢G=1st⁡W
2 vc0.2 ⊢S=2nd⁡W
3 vc0.3 ⊢X=ran⁡G
4 vc0.4 ⊢Z=GId⁡G
5 1 3 4 vc0rid ⊢W∈CVecOLD∧A∈X→AGZ=A
6 1p0e1 ⊢1+0=1
7 6 oveq1i ⊢1+0SA=1SA
8 0cn ⊢0∈ℂ
9 ax-1cn ⊢1∈ℂ
10 1 2 3 vcdir ⊢W∈CVecOLD∧1∈ℂ∧0∈ℂ∧A∈X→1+0SA=1SAG0SA
11 9 10 mp3anr1 ⊢W∈CVecOLD∧0∈ℂ∧A∈X→1+0SA=1SAG0SA
12 8 11 mpanr1 ⊢W∈CVecOLD∧A∈X→1+0SA=1SAG0SA
13 1 2 3 vcidOLD ⊢W∈CVecOLD∧A∈X→1SA=A
14 7 12 13 3eqtr3a ⊢W∈CVecOLD∧A∈X→1SAG0SA=A
15 13 oveq1d ⊢W∈CVecOLD∧A∈X→1SAG0SA=AG0SA
16 5 14 15 3eqtr2rd ⊢W∈CVecOLD∧A∈X→AG0SA=AGZ
17 1 2 3 vccl ⊢W∈CVecOLD∧0∈ℂ∧A∈X→0SA∈X
18 8 17 mp3an2 ⊢W∈CVecOLD∧A∈X→0SA∈X
19 1 3 4 vczcl ⊢W∈CVecOLD→Z∈X
20 19 adantr ⊢W∈CVecOLD∧A∈X→Z∈X
21 simpr ⊢W∈CVecOLD∧A∈X→A∈X
22 18 20 21 3jca ⊢W∈CVecOLD∧A∈X→0SA∈X∧Z∈X∧A∈X
23 1 3 vclcan ⊢W∈CVecOLD∧0SA∈X∧Z∈X∧A∈X→AG0SA=AGZ↔0SA=Z
24 22 23 syldan ⊢W∈CVecOLD∧A∈X→AG0SA=AGZ↔0SA=Z
25 16 24 mpbid ⊢W∈CVecOLD∧A∈X→0SA=Z