Metamath Proof Explorer

Theorem normpar

Description: Parallelogram law for norms. Remark 3.4(B) of Beran p. 98. (Contributed by NM, 15-Apr-2007) (New usage is discouraged.)

Ref Expression
Assertion normpar ⊢A∈ℋ∧B∈ℋ→normℎ⁡A-ℎB2+normℎ⁡A+ℎB2=2⁢normℎ⁡A2+2⁢normℎ⁡B2

Proof

Step Hyp Ref Expression
1 fvoveq1 ⊢A=ifA∈ℋA0ℎ→normℎ⁡A-ℎB=normℎ⁡ifA∈ℋA0ℎ-ℎB
2 1 oveq1d ⊢A=ifA∈ℋA0ℎ→normℎ⁡A-ℎB2=normℎ⁡ifA∈ℋA0ℎ-ℎB2
3 fvoveq1 ⊢A=ifA∈ℋA0ℎ→normℎ⁡A+ℎB=normℎ⁡ifA∈ℋA0ℎ+ℎB
4 3 oveq1d ⊢A=ifA∈ℋA0ℎ→normℎ⁡A+ℎB2=normℎ⁡ifA∈ℋA0ℎ+ℎB2
5 2 4 oveq12d ⊢A=ifA∈ℋA0ℎ→normℎ⁡A-ℎB2+normℎ⁡A+ℎB2=normℎ⁡ifA∈ℋA0ℎ-ℎB2+normℎ⁡ifA∈ℋA0ℎ+ℎB2
6 fveq2 ⊢A=ifA∈ℋA0ℎ→normℎ⁡A=normℎ⁡ifA∈ℋA0ℎ
7 6 oveq1d ⊢A=ifA∈ℋA0ℎ→normℎ⁡A2=normℎ⁡ifA∈ℋA0ℎ2
8 7 oveq2d ⊢A=ifA∈ℋA0ℎ→2⁢normℎ⁡A2=2⁢normℎ⁡ifA∈ℋA0ℎ2
9 8 oveq1d ⊢A=ifA∈ℋA0ℎ→2⁢normℎ⁡A2+2⁢normℎ⁡B2=2⁢normℎ⁡ifA∈ℋA0ℎ2+2⁢normℎ⁡B2
10 5 9 eqeq12d ⊢A=ifA∈ℋA0ℎ→normℎ⁡A-ℎB2+normℎ⁡A+ℎB2=2⁢normℎ⁡A2+2⁢normℎ⁡B2↔normℎ⁡ifA∈ℋA0ℎ-ℎB2+normℎ⁡ifA∈ℋA0ℎ+ℎB2=2⁢normℎ⁡ifA∈ℋA0ℎ2+2⁢normℎ⁡B2
11 oveq2 ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ-ℎB=ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ
12 11 fveq2d ⊢B=ifB∈ℋB0ℎ→normℎ⁡ifA∈ℋA0ℎ-ℎB=normℎ⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ
13 12 oveq1d ⊢B=ifB∈ℋB0ℎ→normℎ⁡ifA∈ℋA0ℎ-ℎB2=normℎ⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ2
14 oveq2 ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ+ℎB=ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ
15 14 fveq2d ⊢B=ifB∈ℋB0ℎ→normℎ⁡ifA∈ℋA0ℎ+ℎB=normℎ⁡ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ
16 15 oveq1d ⊢B=ifB∈ℋB0ℎ→normℎ⁡ifA∈ℋA0ℎ+ℎB2=normℎ⁡ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ2
17 13 16 oveq12d ⊢B=ifB∈ℋB0ℎ→normℎ⁡ifA∈ℋA0ℎ-ℎB2+normℎ⁡ifA∈ℋA0ℎ+ℎB2=normℎ⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ2+normℎ⁡ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ2
18 fveq2 ⊢B=ifB∈ℋB0ℎ→normℎ⁡B=normℎ⁡ifB∈ℋB0ℎ
19 18 oveq1d ⊢B=ifB∈ℋB0ℎ→normℎ⁡B2=normℎ⁡ifB∈ℋB0ℎ2
20 19 oveq2d ⊢B=ifB∈ℋB0ℎ→2⁢normℎ⁡B2=2⁢normℎ⁡ifB∈ℋB0ℎ2
21 20 oveq2d ⊢B=ifB∈ℋB0ℎ→2⁢normℎ⁡ifA∈ℋA0ℎ2+2⁢normℎ⁡B2=2⁢normℎ⁡ifA∈ℋA0ℎ2+2⁢normℎ⁡ifB∈ℋB0ℎ2
22 17 21 eqeq12d ⊢B=ifB∈ℋB0ℎ→normℎ⁡ifA∈ℋA0ℎ-ℎB2+normℎ⁡ifA∈ℋA0ℎ+ℎB2=2⁢normℎ⁡ifA∈ℋA0ℎ2+2⁢normℎ⁡B2↔normℎ⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ2+normℎ⁡ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ2=2⁢normℎ⁡ifA∈ℋA0ℎ2+2⁢normℎ⁡ifB∈ℋB0ℎ2
23 ifhvhv0 ⊢ifA∈ℋA0ℎ∈ℋ
24 ifhvhv0 ⊢ifB∈ℋB0ℎ∈ℋ
25 23 24 normpari ⊢normℎ⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ2+normℎ⁡ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ2=2⁢normℎ⁡ifA∈ℋA0ℎ2+2⁢normℎ⁡ifB∈ℋB0ℎ2
26 10 22 25 dedth2h ⊢A∈ℋ∧B∈ℋ→normℎ⁡A-ℎB2+normℎ⁡A+ℎB2=2⁢normℎ⁡A2+2⁢normℎ⁡B2