isph

Description: The predicate "is an inner product space." (Contributed by NM, 1-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	isph.1	$⊢ X = BaseSet (U)$
	isph.2	$⊢ G = +_{v} (U)$
	isph.3	$⊢ M = -_{v} (U)$
	isph.6	$⊢ N = {norm}_{CV} (U)$
Assertion	isph	$⊢ U \in {CPreHil}_{OLD} \leftrightarrow (U \in NrmCVec \land \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x M y)}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2}))$

Proof

Step	Hyp	Ref	Expression
1		isph.1	$⊢ X = BaseSet (U)$
2		isph.2	$⊢ G = +_{v} (U)$
3		isph.3	$⊢ M = -_{v} (U)$
4		isph.6	$⊢ N = {norm}_{CV} (U)$
5		phnv	$⊢ U \in {CPreHil}_{OLD} \to U \in NrmCVec$
6		eqid	$⊢ \cdot_{𝑠OLD} (U) = \cdot_{𝑠OLD} (U)$
7	2 6 4	nvop	$⊢ U \in NrmCVec \to U = ⟨⟨G, \cdot_{𝑠OLD} (U)⟩, N⟩$
8		eleq1	$⊢ U = ⟨⟨G, \cdot_{𝑠OLD} (U)⟩, N⟩ \to (U \in {CPreHil}_{OLD} \leftrightarrow ⟨⟨G, \cdot_{𝑠OLD} (U)⟩, N⟩ \in {CPreHil}_{OLD})$
9	2	fvexi	$⊢ G \in V$
10		fvex	$⊢ \cdot_{𝑠OLD} (U) \in V$
11	4	fvexi	$⊢ N \in V$
12	1 2	bafval	$⊢ X = ran G$
13	12	isphg	$⊢ (G \in V \land \cdot_{𝑠OLD} (U) \in V \land N \in V) \to (⟨⟨G, \cdot_{𝑠OLD} (U)⟩, N⟩ \in {CPreHil}_{OLD} \leftrightarrow (⟨⟨G, \cdot_{𝑠OLD} (U)⟩, N⟩ \in NrmCVec \land \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x G (-1 \cdot_{𝑠OLD} (U) y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2})))$
14	9 10 11 13	mp3an	$⊢ ⟨⟨G, \cdot_{𝑠OLD} (U)⟩, N⟩ \in {CPreHil}_{OLD} \leftrightarrow (⟨⟨G, \cdot_{𝑠OLD} (U)⟩, N⟩ \in NrmCVec \land \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x G (-1 \cdot_{𝑠OLD} (U) y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2}))$
15	1 2 6 3	nvmval	$⊢ (U \in NrmCVec \land x \in X \land y \in X) \to x M y = x G (-1 \cdot_{𝑠OLD} (U) y)$
16	15	3expa	$⊢ ((U \in NrmCVec \land x \in X) \land y \in X) \to x M y = x G (-1 \cdot_{𝑠OLD} (U) y)$
17	16	fveq2d	$⊢ ((U \in NrmCVec \land x \in X) \land y \in X) \to N (x M y) = N (x G (-1 \cdot_{𝑠OLD} (U) y))$
18	17	oveq1d	$⊢ ((U \in NrmCVec \land x \in X) \land y \in X) \to {N (x M y)}^{2} = {N (x G (-1 \cdot_{𝑠OLD} (U) y))}^{2}$
19	18	oveq2d	$⊢ ((U \in NrmCVec \land x \in X) \land y \in X) \to {N (x G y)}^{2} + {N (x M y)}^{2} = {N (x G y)}^{2} + {N (x G (-1 \cdot_{𝑠OLD} (U) y))}^{2}$
20	19	eqeq1d	$⊢ ((U \in NrmCVec \land x \in X) \land y \in X) \to ({N (x G y)}^{2} + {N (x M y)}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2}) \leftrightarrow {N (x G y)}^{2} + {N (x G (-1 \cdot_{𝑠OLD} (U) y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2}))$
21	20	ralbidva	$⊢ (U \in NrmCVec \land x \in X) \to (\forall y \in X {N (x G y)}^{2} + {N (x M y)}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2}) \leftrightarrow \forall y \in X {N (x G y)}^{2} + {N (x G (-1 \cdot_{𝑠OLD} (U) y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2}))$
22	21	ralbidva	$⊢ U \in NrmCVec \to (\forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x M y)}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2}) \leftrightarrow \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x G (-1 \cdot_{𝑠OLD} (U) y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2}))$
23	22	pm5.32i	$⊢ (U \in NrmCVec \land \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x M y)}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2})) \leftrightarrow (U \in NrmCVec \land \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x G (-1 \cdot_{𝑠OLD} (U) y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2}))$
24		eleq1	$⊢ U = ⟨⟨G, \cdot_{𝑠OLD} (U)⟩, N⟩ \to (U \in NrmCVec \leftrightarrow ⟨⟨G, \cdot_{𝑠OLD} (U)⟩, N⟩ \in NrmCVec)$
25	24	anbi1d	$⊢ U = ⟨⟨G, \cdot_{𝑠OLD} (U)⟩, N⟩ \to ((U \in NrmCVec \land \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x G (-1 \cdot_{𝑠OLD} (U) y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2})) \leftrightarrow (⟨⟨G, \cdot_{𝑠OLD} (U)⟩, N⟩ \in NrmCVec \land \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x G (-1 \cdot_{𝑠OLD} (U) y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2})))$
26	23 25	bitr2id	$⊢ U = ⟨⟨G, \cdot_{𝑠OLD} (U)⟩, N⟩ \to ((⟨⟨G, \cdot_{𝑠OLD} (U)⟩, N⟩ \in NrmCVec \land \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x G (-1 \cdot_{𝑠OLD} (U) y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2})) \leftrightarrow (U \in NrmCVec \land \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x M y)}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2})))$
27	14 26	syl5bb	$⊢ U = ⟨⟨G, \cdot_{𝑠OLD} (U)⟩, N⟩ \to (⟨⟨G, \cdot_{𝑠OLD} (U)⟩, N⟩ \in {CPreHil}_{OLD} \leftrightarrow (U \in NrmCVec \land \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x M y)}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2})))$
28	8 27	bitrd	$⊢ U = ⟨⟨G, \cdot_{𝑠OLD} (U)⟩, N⟩ \to (U \in {CPreHil}_{OLD} \leftrightarrow (U \in NrmCVec \land \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x M y)}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2})))$
29	7 28	syl	$⊢ U \in NrmCVec \to (U \in {CPreHil}_{OLD} \leftrightarrow (U \in NrmCVec \land \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x M y)}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2})))$
30	29	bianabs	$⊢ U \in NrmCVec \to (U \in {CPreHil}_{OLD} \leftrightarrow \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x M y)}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2}))$
31	5 30	biadanii	$⊢ U \in {CPreHil}_{OLD} \leftrightarrow (U \in NrmCVec \land \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x M y)}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2}))$

Metamath Proof Explorer

Theorem isph

Proof