Metamath Proof Explorer

Theorem 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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
phpar.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
phpar.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
phpar.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
Assertion phpar ( ( 𝑈 ∈ CPreHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 phpar.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 phpar.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 phpar.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
4 phpar.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
5 2 fvexi ⊢ 𝐺 ∈ V
6 3 fvexi ⊢ 𝑆 ∈ V
7 4 fvexi ⊢ 𝑁 ∈ V
8 5 6 7 3pm3.2i ⊢ ( 𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V )
9 2 3 4 phop ⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ )
10 9 eleq1d ⊢ ( 𝑈 ∈ CPreHilOLD → ( 𝑈 ∈ CPreHilOLD ↔ ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ CPreHilOLD ) )
11 10 ibi ⊢ ( 𝑈 ∈ CPreHilOLD → ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ CPreHilOLD )
12 1 2 bafval ⊢ 𝑋 = ran 𝐺
13 12 isphg ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V ) → ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ CPreHilOLD ↔ ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) ) )
14 13 simplbda ⊢ ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V ) ∧ ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ CPreHilOLD ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) )
15 8 11 14 sylancr ⊢ ( 𝑈 ∈ CPreHilOLD → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) )
16 15 3ad2ant1 ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) )
17 fvoveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) )
18 17 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) ↑ 2 ) )
19 fvoveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝑦 ) ) ) )
20 19 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) )
21 18 20 oveq12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) )
22 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ 𝐴 ) )
23 22 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) = ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) )
24 23 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) )
25 24 oveq2d ⊢ ( 𝑥 = 𝐴 → ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) )
26 21 25 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ↔ ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
27 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐺 𝑦 ) = ( 𝐴 𝐺 𝐵 ) )
28 27 fveq2d ⊢ ( 𝑦 = 𝐵 → ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) )
29 28 oveq1d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) )
30 oveq2 ⊢ ( 𝑦 = 𝐵 → ( - 1 𝑆 𝑦 ) = ( - 1 𝑆 𝐵 ) )
31 30 oveq2d ⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐺 ( - 1 𝑆 𝑦 ) ) = ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) )
32 31 fveq2d ⊢ ( 𝑦 = 𝐵 → ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝑦 ) ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) )
33 32 oveq1d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) )
34 29 33 oveq12d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) )
35 fveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝑁 ‘ 𝑦 ) = ( 𝑁 ‘ 𝐵 ) )
36 35 oveq1d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) = ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) )
37 36 oveq2d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
38 37 oveq2d ⊢ ( 𝑦 = 𝐵 → ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )
39 34 38 eqeq12d ⊢ ( 𝑦 = 𝐵 → ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ↔ ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) )
40 26 39 rspc2v ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) → ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) )
41 40 3adant1 ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) → ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) )
42 16 41 mpd ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )