normcan

Description: Cancellation-type law that "extracts" a vector A from its inner product with a proportional vector B . (Contributed by NM, 18-Mar-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	normcan	$⊢ (B \in ℋ \land B \neq 0_{ℎ} \land A \in span (\{B\})) \to (\frac{A \cdot_{ih} B}{{{norm}_{ℎ} (B)}^{2}}) \cdot_{ℎ} B = A$

Proof

Step	Hyp	Ref	Expression
1		elspansn	$⊢ B \in ℋ \to (A \in span (\{B\}) \leftrightarrow \exists x \in ℂ A = x \cdot_{ℎ} B)$
2	1	adantr	$⊢ (B \in ℋ \land B \neq 0_{ℎ}) \to (A \in span (\{B\}) \leftrightarrow \exists x \in ℂ A = x \cdot_{ℎ} B)$
3		oveq1	$⊢ A = x \cdot_{ℎ} B \to A \cdot_{ih} B = (x \cdot_{ℎ} B) \cdot_{ih} B$
4		simpr	$⊢ (B \in ℋ \land x \in ℂ) \to x \in ℂ$
5		simpl	$⊢ (B \in ℋ \land x \in ℂ) \to B \in ℋ$
6		ax-his3	$⊢ (x \in ℂ \land B \in ℋ \land B \in ℋ) \to (x \cdot_{ℎ} B) \cdot_{ih} B = x (B \cdot_{ih} B)$
7	4 5 5 6	syl3anc	$⊢ (B \in ℋ \land x \in ℂ) \to (x \cdot_{ℎ} B) \cdot_{ih} B = x (B \cdot_{ih} B)$
8	3 7	sylan9eqr	$⊢ ((B \in ℋ \land x \in ℂ) \land A = x \cdot_{ℎ} B) \to A \cdot_{ih} B = x (B \cdot_{ih} B)$
9		normsq	$⊢ B \in ℋ \to {{norm}_{ℎ} (B)}^{2} = B \cdot_{ih} B$
10	9	ad2antrr	$⊢ ((B \in ℋ \land x \in ℂ) \land A = x \cdot_{ℎ} B) \to {{norm}_{ℎ} (B)}^{2} = B \cdot_{ih} B$
11	8 10	oveq12d	$⊢ ((B \in ℋ \land x \in ℂ) \land A = x \cdot_{ℎ} B) \to \frac{A \cdot_{ih} B}{{{norm}_{ℎ} (B)}^{2}} = \frac{x (B \cdot_{ih} B)}{B \cdot_{ih} B}$
12	11	adantllr	$⊢ (((B \in ℋ \land B \neq 0_{ℎ}) \land x \in ℂ) \land A = x \cdot_{ℎ} B) \to \frac{A \cdot_{ih} B}{{{norm}_{ℎ} (B)}^{2}} = \frac{x (B \cdot_{ih} B)}{B \cdot_{ih} B}$
13		simpr	$⊢ ((B \in ℋ \land B \neq 0_{ℎ}) \land x \in ℂ) \to x \in ℂ$
14		hicl	$⊢ (B \in ℋ \land B \in ℋ) \to B \cdot_{ih} B \in ℂ$
15	14	anidms	$⊢ B \in ℋ \to B \cdot_{ih} B \in ℂ$
16	15	ad2antrr	$⊢ ((B \in ℋ \land B \neq 0_{ℎ}) \land x \in ℂ) \to B \cdot_{ih} B \in ℂ$
17		his6	$⊢ B \in ℋ \to (B \cdot_{ih} B = 0 \leftrightarrow B = 0_{ℎ})$
18	17	necon3bid	$⊢ B \in ℋ \to (B \cdot_{ih} B \neq 0 \leftrightarrow B \neq 0_{ℎ})$
19	18	biimpar	$⊢ (B \in ℋ \land B \neq 0_{ℎ}) \to B \cdot_{ih} B \neq 0$
20	19	adantr	$⊢ ((B \in ℋ \land B \neq 0_{ℎ}) \land x \in ℂ) \to B \cdot_{ih} B \neq 0$
21	13 16 20	divcan4d	$⊢ ((B \in ℋ \land B \neq 0_{ℎ}) \land x \in ℂ) \to \frac{x (B \cdot_{ih} B)}{B \cdot_{ih} B} = x$
22	21	adantr	$⊢ (((B \in ℋ \land B \neq 0_{ℎ}) \land x \in ℂ) \land A = x \cdot_{ℎ} B) \to \frac{x (B \cdot_{ih} B)}{B \cdot_{ih} B} = x$
23	12 22	eqtrd	$⊢ (((B \in ℋ \land B \neq 0_{ℎ}) \land x \in ℂ) \land A = x \cdot_{ℎ} B) \to \frac{A \cdot_{ih} B}{{{norm}_{ℎ} (B)}^{2}} = x$
24	23	oveq1d	$⊢ (((B \in ℋ \land B \neq 0_{ℎ}) \land x \in ℂ) \land A = x \cdot_{ℎ} B) \to (\frac{A \cdot_{ih} B}{{{norm}_{ℎ} (B)}^{2}}) \cdot_{ℎ} B = x \cdot_{ℎ} B$
25		simpr	$⊢ (((B \in ℋ \land B \neq 0_{ℎ}) \land x \in ℂ) \land A = x \cdot_{ℎ} B) \to A = x \cdot_{ℎ} B$
26	24 25	eqtr4d	$⊢ (((B \in ℋ \land B \neq 0_{ℎ}) \land x \in ℂ) \land A = x \cdot_{ℎ} B) \to (\frac{A \cdot_{ih} B}{{{norm}_{ℎ} (B)}^{2}}) \cdot_{ℎ} B = A$
27	26	rexlimdva2	$⊢ (B \in ℋ \land B \neq 0_{ℎ}) \to (\exists x \in ℂ A = x \cdot_{ℎ} B \to (\frac{A \cdot_{ih} B}{{{norm}_{ℎ} (B)}^{2}}) \cdot_{ℎ} B = A)$
28	2 27	sylbid	$⊢ (B \in ℋ \land B \neq 0_{ℎ}) \to (A \in span (\{B\}) \to (\frac{A \cdot_{ih} B}{{{norm}_{ℎ} (B)}^{2}}) \cdot_{ℎ} B = A)$
29	28	3impia	$⊢ (B \in ℋ \land B \neq 0_{ℎ} \land A \in span (\{B\})) \to (\frac{A \cdot_{ih} B}{{{norm}_{ℎ} (B)}^{2}}) \cdot_{ℎ} B = A$

Metamath Proof Explorer

Theorem normcan

Proof