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

Proof

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