Metamath Proof Explorer

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	$⊢ G = 1^{st} (W)$
		vc0.2	$⊢ S = 2^{nd} (W)$
		vc0.3	$⊢ X = ran G$
		vc0.4	$⊢ Z = GId (G)$
	Assertion	vcz	$⊢ (W \in {CVec}_{OLD} \land A \in ℂ) \to A S Z = 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	vczcl	$⊢ W \in {CVec}_{OLD} \to Z \in X$
6	5	anim2i	$⊢ (A \in ℂ \land W \in {CVec}_{OLD}) \to (A \in ℂ \land Z \in X)$
7	6	ancoms	$⊢ (W \in {CVec}_{OLD} \land A \in ℂ) \to (A \in ℂ \land Z \in X)$
8		0cn	$⊢ 0 \in ℂ$
9	1 2 3	vcass	$⊢ (W \in {CVec}_{OLD} \land (A \in ℂ \land 0 \in ℂ \land Z \in X)) \to A \cdot 0 S Z = A S (0 S Z)$
10	8 9	mp3anr2	$⊢ (W \in {CVec}_{OLD} \land (A \in ℂ \land Z \in X)) \to A \cdot 0 S Z = A S (0 S Z)$
11	7 10	syldan	$⊢ (W \in {CVec}_{OLD} \land A \in ℂ) \to A \cdot 0 S Z = A S (0 S Z)$
12		mul01	$⊢ A \in ℂ \to A \cdot 0 = 0$
13	12	oveq1d	$⊢ A \in ℂ \to A \cdot 0 S Z = 0 S Z$
14	1 2 3 4	vc0	$⊢ (W \in {CVec}_{OLD} \land Z \in X) \to 0 S Z = Z$
15	5 14	mpdan	$⊢ W \in {CVec}_{OLD} \to 0 S Z = Z$
16	13 15	sylan9eqr	$⊢ (W \in {CVec}_{OLD} \land A \in ℂ) \to A \cdot 0 S Z = Z$
17	15	oveq2d	$⊢ W \in {CVec}_{OLD} \to A S (0 S Z) = A S Z$
18	17	adantr	$⊢ (W \in {CVec}_{OLD} \land A \in ℂ) \to A S (0 S Z) = A S Z$
19	11 16 18	3eqtr3rd	$⊢ (W \in {CVec}_{OLD} \land A \in ℂ) \to A S Z = Z$