phpar2

Description: The parallelogram law for an inner product space. (Contributed by NM, 2-Apr-2007) (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	phpar2	$⊢ (U \in {CPreHil}_{OLD} \land A \in X \land B \in X) \to {N (A G B)}^{2} + {N (A M B)}^{2} = 2 ({N (A)}^{2} + {N (B)}^{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	1 2 3 4	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}))$
6	5	simprbi	$⊢ U \in {CPreHil}_{OLD} \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})$
7	6	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 M y)}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2})$
8		fvoveq1	$⊢ x = A \to N (x G y) = N (A G y)$
9	8	oveq1d	$⊢ x = A \to {N (x G y)}^{2} = {N (A G y)}^{2}$
10		fvoveq1	$⊢ x = A \to N (x M y) = N (A M y)$
11	10	oveq1d	$⊢ x = A \to {N (x M y)}^{2} = {N (A M y)}^{2}$
12	9 11	oveq12d	$⊢ x = A \to {N (x G y)}^{2} + {N (x M y)}^{2} = {N (A G y)}^{2} + {N (A M y)}^{2}$
13		fveq2	$⊢ x = A \to N (x) = N (A)$
14	13	oveq1d	$⊢ x = A \to {N (x)}^{2} = {N (A)}^{2}$
15	14	oveq1d	$⊢ x = A \to {N (x)}^{2} + {N (y)}^{2} = {N (A)}^{2} + {N (y)}^{2}$
16	15	oveq2d	$⊢ x = A \to 2 ({N (x)}^{2} + {N (y)}^{2}) = 2 ({N (A)}^{2} + {N (y)}^{2})$
17	12 16	eqeq12d	$⊢ x = A \to ({N (x G y)}^{2} + {N (x M y)}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2}) \leftrightarrow {N (A G y)}^{2} + {N (A M y)}^{2} = 2 ({N (A)}^{2} + {N (y)}^{2}))$
18		oveq2	$⊢ y = B \to A G y = A G B$
19	18	fveq2d	$⊢ y = B \to N (A G y) = N (A G B)$
20	19	oveq1d	$⊢ y = B \to {N (A G y)}^{2} = {N (A G B)}^{2}$
21		oveq2	$⊢ y = B \to A M y = A M B$
22	21	fveq2d	$⊢ y = B \to N (A M y) = N (A M B)$
23	22	oveq1d	$⊢ y = B \to {N (A M y)}^{2} = {N (A M B)}^{2}$
24	20 23	oveq12d	$⊢ y = B \to {N (A G y)}^{2} + {N (A M y)}^{2} = {N (A G B)}^{2} + {N (A M B)}^{2}$
25		fveq2	$⊢ y = B \to N (y) = N (B)$
26	25	oveq1d	$⊢ y = B \to {N (y)}^{2} = {N (B)}^{2}$
27	26	oveq2d	$⊢ y = B \to {N (A)}^{2} + {N (y)}^{2} = {N (A)}^{2} + {N (B)}^{2}$
28	27	oveq2d	$⊢ y = B \to 2 ({N (A)}^{2} + {N (y)}^{2}) = 2 ({N (A)}^{2} + {N (B)}^{2})$
29	24 28	eqeq12d	$⊢ y = B \to ({N (A G y)}^{2} + {N (A M y)}^{2} = 2 ({N (A)}^{2} + {N (y)}^{2}) \leftrightarrow {N (A G B)}^{2} + {N (A M B)}^{2} = 2 ({N (A)}^{2} + {N (B)}^{2}))$
30	17 29	rspc2v	$⊢ (A \in X \land B \in X) \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}) \to {N (A G B)}^{2} + {N (A M B)}^{2} = 2 ({N (A)}^{2} + {N (B)}^{2}))$
31	30	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 M y)}^{2} = 2 ({N (x)}^{2} + {N (y)}^{2}) \to {N (A G B)}^{2} + {N (A M B)}^{2} = 2 ({N (A)}^{2} + {N (B)}^{2}))$
32	7 31	mpd	$⊢ (U \in {CPreHil}_{OLD} \land A \in X \land B \in X) \to {N (A G B)}^{2} + {N (A M B)}^{2} = 2 ({N (A)}^{2} + {N (B)}^{2})$

Metamath Proof Explorer

Theorem phpar2

Proof