spansncol

Description: The singletons of collinear vectors have the same span. (Contributed by NM, 6-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	spansncol	$⊢ (A \in ℋ \land B \in ℂ \land B \neq 0) \to span (\{B \cdot_{ℎ} A\}) = span (\{A\})$

Proof

Step	Hyp	Ref	Expression
1		mulcl	$⊢ (y \in ℂ \land B \in ℂ) \to y B \in ℂ$
2	1	ancoms	$⊢ (B \in ℂ \land y \in ℂ) \to y B \in ℂ$
3	2	adantll	$⊢ ((A \in ℋ \land B \in ℂ) \land y \in ℂ) \to y B \in ℂ$
4		ax-hvmulass	$⊢ (y \in ℂ \land B \in ℂ \land A \in ℋ) \to y B \cdot_{ℎ} A = y \cdot_{ℎ} (B \cdot_{ℎ} A)$
5	4	3com13	$⊢ (A \in ℋ \land B \in ℂ \land y \in ℂ) \to y B \cdot_{ℎ} A = y \cdot_{ℎ} (B \cdot_{ℎ} A)$
6	5	3expa	$⊢ ((A \in ℋ \land B \in ℂ) \land y \in ℂ) \to y B \cdot_{ℎ} A = y \cdot_{ℎ} (B \cdot_{ℎ} A)$
7	6	eqeq2d	$⊢ ((A \in ℋ \land B \in ℂ) \land y \in ℂ) \to (x = y B \cdot_{ℎ} A \leftrightarrow x = y \cdot_{ℎ} (B \cdot_{ℎ} A))$
8	7	biimprd	$⊢ ((A \in ℋ \land B \in ℂ) \land y \in ℂ) \to (x = y \cdot_{ℎ} (B \cdot_{ℎ} A) \to x = y B \cdot_{ℎ} A)$
9		oveq1	$⊢ z = y B \to z \cdot_{ℎ} A = y B \cdot_{ℎ} A$
10	9	rspceeqv	$⊢ (y B \in ℂ \land x = y B \cdot_{ℎ} A) \to \exists z \in ℂ x = z \cdot_{ℎ} A$
11	3 8 10	syl6an	$⊢ ((A \in ℋ \land B \in ℂ) \land y \in ℂ) \to (x = y \cdot_{ℎ} (B \cdot_{ℎ} A) \to \exists z \in ℂ x = z \cdot_{ℎ} A)$
12	11	rexlimdva	$⊢ (A \in ℋ \land B \in ℂ) \to (\exists y \in ℂ x = y \cdot_{ℎ} (B \cdot_{ℎ} A) \to \exists z \in ℂ x = z \cdot_{ℎ} A)$
13	12	3adant3	$⊢ (A \in ℋ \land B \in ℂ \land B \neq 0) \to (\exists y \in ℂ x = y \cdot_{ℎ} (B \cdot_{ℎ} A) \to \exists z \in ℂ x = z \cdot_{ℎ} A)$
14		divcl	$⊢ (z \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{z}{B} \in ℂ$
15	14	3expb	$⊢ (z \in ℂ \land (B \in ℂ \land B \neq 0)) \to \frac{z}{B} \in ℂ$
16	15	adantlr	$⊢ ((z \in ℂ \land A \in ℋ) \land (B \in ℂ \land B \neq 0)) \to \frac{z}{B} \in ℂ$
17		simprl	$⊢ ((z \in ℂ \land A \in ℋ) \land (B \in ℂ \land B \neq 0)) \to B \in ℂ$
18		simplr	$⊢ ((z \in ℂ \land A \in ℋ) \land (B \in ℂ \land B \neq 0)) \to A \in ℋ$
19		ax-hvmulass	$⊢ (\frac{z}{B} \in ℂ \land B \in ℂ \land A \in ℋ) \to (\frac{z}{B}) B \cdot_{ℎ} A = (\frac{z}{B}) \cdot_{ℎ} (B \cdot_{ℎ} A)$
20	16 17 18 19	syl3anc	$⊢ ((z \in ℂ \land A \in ℋ) \land (B \in ℂ \land B \neq 0)) \to (\frac{z}{B}) B \cdot_{ℎ} A = (\frac{z}{B}) \cdot_{ℎ} (B \cdot_{ℎ} A)$
21		divcan1	$⊢ (z \in ℂ \land B \in ℂ \land B \neq 0) \to (\frac{z}{B}) B = z$
22	21	3expb	$⊢ (z \in ℂ \land (B \in ℂ \land B \neq 0)) \to (\frac{z}{B}) B = z$
23	22	adantlr	$⊢ ((z \in ℂ \land A \in ℋ) \land (B \in ℂ \land B \neq 0)) \to (\frac{z}{B}) B = z$
24	23	oveq1d	$⊢ ((z \in ℂ \land A \in ℋ) \land (B \in ℂ \land B \neq 0)) \to (\frac{z}{B}) B \cdot_{ℎ} A = z \cdot_{ℎ} A$
25	20 24	eqtr3d	$⊢ ((z \in ℂ \land A \in ℋ) \land (B \in ℂ \land B \neq 0)) \to (\frac{z}{B}) \cdot_{ℎ} (B \cdot_{ℎ} A) = z \cdot_{ℎ} A$
26	25	eqeq2d	$⊢ ((z \in ℂ \land A \in ℋ) \land (B \in ℂ \land B \neq 0)) \to (x = (\frac{z}{B}) \cdot_{ℎ} (B \cdot_{ℎ} A) \leftrightarrow x = z \cdot_{ℎ} A)$
27	26	biimprd	$⊢ ((z \in ℂ \land A \in ℋ) \land (B \in ℂ \land B \neq 0)) \to (x = z \cdot_{ℎ} A \to x = (\frac{z}{B}) \cdot_{ℎ} (B \cdot_{ℎ} A))$
28		oveq1	$⊢ y = \frac{z}{B} \to y \cdot_{ℎ} (B \cdot_{ℎ} A) = (\frac{z}{B}) \cdot_{ℎ} (B \cdot_{ℎ} A)$
29	28	rspceeqv	$⊢ (\frac{z}{B} \in ℂ \land x = (\frac{z}{B}) \cdot_{ℎ} (B \cdot_{ℎ} A)) \to \exists y \in ℂ x = y \cdot_{ℎ} (B \cdot_{ℎ} A)$
30	16 27 29	syl6an	$⊢ ((z \in ℂ \land A \in ℋ) \land (B \in ℂ \land B \neq 0)) \to (x = z \cdot_{ℎ} A \to \exists y \in ℂ x = y \cdot_{ℎ} (B \cdot_{ℎ} A))$
31	30	exp43	$⊢ z \in ℂ \to (A \in ℋ \to (B \in ℂ \to (B \neq 0 \to (x = z \cdot_{ℎ} A \to \exists y \in ℂ x = y \cdot_{ℎ} (B \cdot_{ℎ} A)))))$
32	31	com4l	$⊢ A \in ℋ \to (B \in ℂ \to (B \neq 0 \to (z \in ℂ \to (x = z \cdot_{ℎ} A \to \exists y \in ℂ x = y \cdot_{ℎ} (B \cdot_{ℎ} A)))))$
33	32	3imp	$⊢ (A \in ℋ \land B \in ℂ \land B \neq 0) \to (z \in ℂ \to (x = z \cdot_{ℎ} A \to \exists y \in ℂ x = y \cdot_{ℎ} (B \cdot_{ℎ} A)))$
34	33	rexlimdv	$⊢ (A \in ℋ \land B \in ℂ \land B \neq 0) \to (\exists z \in ℂ x = z \cdot_{ℎ} A \to \exists y \in ℂ x = y \cdot_{ℎ} (B \cdot_{ℎ} A))$
35	13 34	impbid	$⊢ (A \in ℋ \land B \in ℂ \land B \neq 0) \to (\exists y \in ℂ x = y \cdot_{ℎ} (B \cdot_{ℎ} A) \leftrightarrow \exists z \in ℂ x = z \cdot_{ℎ} A)$
36		hvmulcl	$⊢ (B \in ℂ \land A \in ℋ) \to B \cdot_{ℎ} A \in ℋ$
37	36	ancoms	$⊢ (A \in ℋ \land B \in ℂ) \to B \cdot_{ℎ} A \in ℋ$
38		elspansn	$⊢ B \cdot_{ℎ} A \in ℋ \to (x \in span (\{B \cdot_{ℎ} A\}) \leftrightarrow \exists y \in ℂ x = y \cdot_{ℎ} (B \cdot_{ℎ} A))$
39	37 38	syl	$⊢ (A \in ℋ \land B \in ℂ) \to (x \in span (\{B \cdot_{ℎ} A\}) \leftrightarrow \exists y \in ℂ x = y \cdot_{ℎ} (B \cdot_{ℎ} A))$
40	39	3adant3	$⊢ (A \in ℋ \land B \in ℂ \land B \neq 0) \to (x \in span (\{B \cdot_{ℎ} A\}) \leftrightarrow \exists y \in ℂ x = y \cdot_{ℎ} (B \cdot_{ℎ} A))$
41		elspansn	$⊢ A \in ℋ \to (x \in span (\{A\}) \leftrightarrow \exists z \in ℂ x = z \cdot_{ℎ} A)$
42	41	3ad2ant1	$⊢ (A \in ℋ \land B \in ℂ \land B \neq 0) \to (x \in span (\{A\}) \leftrightarrow \exists z \in ℂ x = z \cdot_{ℎ} A)$
43	35 40 42	3bitr4d	$⊢ (A \in ℋ \land B \in ℂ \land B \neq 0) \to (x \in span (\{B \cdot_{ℎ} A\}) \leftrightarrow x \in span (\{A\}))$
44	43	eqrdv	$⊢ (A \in ℋ \land B \in ℂ \land B \neq 0) \to span (\{B \cdot_{ℎ} A\}) = span (\{A\})$

Metamath Proof Explorer

Theorem spansncol

Proof