phpar

Description: The parallelogram law for an inner product space. (Contributed by NM, 2-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	phpar.1	$⊢ X = BaseSet (U)$
	phpar.2	$⊢ G = +_{v} (U)$
	phpar.4	$⊢ S = \cdot_{𝑠OLD} (U)$
	phpar.6	$⊢ N = {norm}_{CV} (U)$
Assertion	phpar	$⊢ (U \in {CPreHil}_{OLD} \land A \in X \land B \in X) \to {N (A G B)}^{2} + {N (A G (-1 S B))}^{2} = 2 ({N (A)}^{2} + {N (B)}^{2})$

Proof

Step	Hyp	Ref	Expression
1		phpar.1	$⊢ X = BaseSet (U)$
2		phpar.2	$⊢ G = +_{v} (U)$
3		phpar.4	$⊢ S = \cdot_{𝑠OLD} (U)$
4		phpar.6	$⊢ N = {norm}_{CV} (U)$
5	2	fvexi	$⊢ G \in V$
6	3	fvexi	$⊢ S \in V$
7	4	fvexi	$⊢ N \in V$
8	5 6 7	3pm3.2i	$⊢ (G \in V \land S \in V \land N \in V)$
9	2 3 4	phop	$⊢ U \in {CPreHil}_{OLD} \to U = ⟨⟨G, S⟩, N⟩$
10	9	eleq1d	$⊢ U \in {CPreHil}_{OLD} \to (U \in {CPreHil}_{OLD} \leftrightarrow ⟨⟨G, S⟩, N⟩ \in {CPreHil}_{OLD})$
11	10	ibi	$⊢ U \in {CPreHil}_{OLD} \to ⟨⟨G, S⟩, N⟩ \in {CPreHil}_{OLD}$
12	1 2	bafval	$⊢ X = ran G$
13	12	isphg	$⊢ (G \in V \land S \in V \land N \in V) \to (⟨⟨G, S⟩, N⟩ \in {CPreHil}_{OLD} \leftrightarrow (⟨⟨G, S⟩, N⟩ \in NrmCVec \land \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x G (-1 S y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2})))$
14	13	simplbda	$⊢ ((G \in V \land S \in V \land N \in V) \land ⟨⟨G, S⟩, N⟩ \in {CPreHil}_{OLD}) \to \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x G (-1 S y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2})$
15	8 11 14	sylancr	$⊢ U \in {CPreHil}_{OLD} \to \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x G (-1 S y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2})$
16	15	3ad2ant1	$⊢ (U \in {CPreHil}_{OLD} \land A \in X \land B \in X) \to \forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x G (-1 S y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2})$
17		fvoveq1	$⊢ x = A \to N (x G y) = N (A G y)$
18	17	oveq1d	$⊢ x = A \to {N (x G y)}^{2} = {N (A G y)}^{2}$
19		fvoveq1	$⊢ x = A \to N (x G (-1 S y)) = N (A G (-1 S y))$
20	19	oveq1d	$⊢ x = A \to {N (x G (-1 S y))}^{2} = {N (A G (-1 S y))}^{2}$
21	18 20	oveq12d	$⊢ x = A \to {N (x G y)}^{2} + {N (x G (-1 S y))}^{2} = {N (A G y)}^{2} + {N (A G (-1 S y))}^{2}$
22		fveq2	$⊢ x = A \to N (x) = N (A)$
23	22	oveq1d	$⊢ x = A \to {N (x)}^{2} = {N (A)}^{2}$
24	23	oveq1d	$⊢ x = A \to {N (x)}^{2} + {N (y)}^{2} = {N (A)}^{2} + {N (y)}^{2}$
25	24	oveq2d	$⊢ x = A \to 2 ({N (x)}^{2} + {N (y)}^{2}) = 2 ({N (A)}^{2} + {N (y)}^{2})$
26	21 25	eqeq12d	$⊢ x = A \to ({N (x G y)}^{2} + {N (x G (-1 S y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2}) \leftrightarrow {N (A G y)}^{2} + {N (A G (-1 S y))}^{2} = 2 ({N (A)}^{2} + {N (y)}^{2}))$
27		oveq2	$⊢ y = B \to A G y = A G B$
28	27	fveq2d	$⊢ y = B \to N (A G y) = N (A G B)$
29	28	oveq1d	$⊢ y = B \to {N (A G y)}^{2} = {N (A G B)}^{2}$
30		oveq2	$⊢ y = B \to -1 S y = -1 S B$
31	30	oveq2d	$⊢ y = B \to A G (-1 S y) = A G (-1 S B)$
32	31	fveq2d	$⊢ y = B \to N (A G (-1 S y)) = N (A G (-1 S B))$
33	32	oveq1d	$⊢ y = B \to {N (A G (-1 S y))}^{2} = {N (A G (-1 S B))}^{2}$
34	29 33	oveq12d	$⊢ y = B \to {N (A G y)}^{2} + {N (A G (-1 S y))}^{2} = {N (A G B)}^{2} + {N (A G (-1 S B))}^{2}$
35		fveq2	$⊢ y = B \to N (y) = N (B)$
36	35	oveq1d	$⊢ y = B \to {N (y)}^{2} = {N (B)}^{2}$
37	36	oveq2d	$⊢ y = B \to {N (A)}^{2} + {N (y)}^{2} = {N (A)}^{2} + {N (B)}^{2}$
38	37	oveq2d	$⊢ y = B \to 2 ({N (A)}^{2} + {N (y)}^{2}) = 2 ({N (A)}^{2} + {N (B)}^{2})$
39	34 38	eqeq12d	$⊢ y = B \to ({N (A G y)}^{2} + {N (A G (-1 S y))}^{2} = 2 ({N (A)}^{2} + {N (y)}^{2}) \leftrightarrow {N (A G B)}^{2} + {N (A G (-1 S B))}^{2} = 2 ({N (A)}^{2} + {N (B)}^{2}))$
40	26 39	rspc2v	$⊢ (A \in X \land B \in X) \to (\forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x G (-1 S y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2}) \to {N (A G B)}^{2} + {N (A G (-1 S B))}^{2} = 2 ({N (A)}^{2} + {N (B)}^{2}))$
41	40	3adant1	$⊢ (U \in {CPreHil}_{OLD} \land A \in X \land B \in X) \to (\forall x \in X \forall y \in X {N (x G y)}^{2} + {N (x G (-1 S y))}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2}) \to {N (A G B)}^{2} + {N (A G (-1 S B))}^{2} = 2 ({N (A)}^{2} + {N (B)}^{2}))$
42	16 41	mpd	$⊢ (U \in {CPreHil}_{OLD} \land A \in X \land B \in X) \to {N (A G B)}^{2} + {N (A G (-1 S B))}^{2} = 2 ({N (A)}^{2} + {N (B)}^{2})$

Metamath Proof Explorer

Theorem phpar

Proof