nvs

Description: Proportionality property of the norm of a scalar product in a normed complex vector space. (Contributed by NM, 11-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvs.1	$⊢ X = BaseSet (U)$
	nvs.4	$⊢ S = \cdot_{𝑠OLD} (U)$
	nvs.6	$⊢ N = {norm}_{CV} (U)$
Assertion	nvs	$⊢ (U \in NrmCVec \land A \in ℂ \land B \in X) \to N (A S B) = \|A\| N (B)$

Proof

Step	Hyp	Ref	Expression
1		nvs.1	$⊢ X = BaseSet (U)$
2		nvs.4	$⊢ S = \cdot_{𝑠OLD} (U)$
3		nvs.6	$⊢ N = {norm}_{CV} (U)$
4		eqid	$⊢ +_{v} (U) = +_{v} (U)$
5		eqid	$⊢ 0_{vec} (U) = 0_{vec} (U)$
6	1 4 2 5 3	nvi	$⊢ U \in NrmCVec \to (⟨+_{v} (U), S⟩ \in {CVec}_{OLD} \land N : X ⟶ ℝ \land \forall x \in X ((N (x) = 0 \to x = 0_{vec} (U)) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x +_{v} (U) y) \leq N (x) + N (y)))$
7	6	simp3d	$⊢ U \in NrmCVec \to \forall x \in X ((N (x) = 0 \to x = 0_{vec} (U)) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x +_{v} (U) y) \leq N (x) + N (y))$
8		simp2	$⊢ ((N (x) = 0 \to x = 0_{vec} (U)) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x +_{v} (U) y) \leq N (x) + N (y)) \to \forall y \in ℂ N (y S x) = \|y\| N (x)$
9	8	ralimi	$⊢ \forall x \in X ((N (x) = 0 \to x = 0_{vec} (U)) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x +_{v} (U) y) \leq N (x) + N (y)) \to \forall x \in X \forall y \in ℂ N (y S x) = \|y\| N (x)$
10	7 9	syl	$⊢ U \in NrmCVec \to \forall x \in X \forall y \in ℂ N (y S x) = \|y\| N (x)$
11		oveq2	$⊢ x = B \to y S x = y S B$
12	11	fveq2d	$⊢ x = B \to N (y S x) = N (y S B)$
13		fveq2	$⊢ x = B \to N (x) = N (B)$
14	13	oveq2d	$⊢ x = B \to \|y\| N (x) = \|y\| N (B)$
15	12 14	eqeq12d	$⊢ x = B \to (N (y S x) = \|y\| N (x) \leftrightarrow N (y S B) = \|y\| N (B))$
16		fvoveq1	$⊢ y = A \to N (y S B) = N (A S B)$
17		fveq2	$⊢ y = A \to \|y\| = \|A\|$
18	17	oveq1d	$⊢ y = A \to \|y\| N (B) = \|A\| N (B)$
19	16 18	eqeq12d	$⊢ y = A \to (N (y S B) = \|y\| N (B) \leftrightarrow N (A S B) = \|A\| N (B))$
20	15 19	rspc2v	$⊢ (B \in X \land A \in ℂ) \to (\forall x \in X \forall y \in ℂ N (y S x) = \|y\| N (x) \to N (A S B) = \|A\| N (B))$
21	10 20	syl5	$⊢ (B \in X \land A \in ℂ) \to (U \in NrmCVec \to N (A S B) = \|A\| N (B))$
22	21	3impia	$⊢ (B \in X \land A \in ℂ \land U \in NrmCVec) \to N (A S B) = \|A\| N (B)$
23	22	3com13	$⊢ (U \in NrmCVec \land A \in ℂ \land B \in X) \to N (A S B) = \|A\| N (B)$

Metamath Proof Explorer

Theorem nvs

Proof