Metamath Proof Explorer

Theorem 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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
isph.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
isph.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
isph.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
Assertion phpar2 ( ( 𝑈 ∈ CPreHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 isph.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 isph.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 isph.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
4 isph.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
5 1 2 3 4 isph ⊢ ( 𝑈 ∈ CPreHilOLD ↔ ( 𝑈 ∈ NrmCVec ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
6 5 simprbi ⊢ ( 𝑈 ∈ CPreHilOLD → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) )
7 6 3ad2ant1 ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) )
8 fvoveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) )
9 8 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) ↑ 2 ) )
10 fvoveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
11 10 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↑ 2 ) )
12 9 11 oveq12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↑ 2 ) ) )
13 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ 𝐴 ) )
14 13 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) = ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) )
15 14 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) )
16 15 oveq2d ⊢ ( 𝑥 = 𝐴 → ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) )
17 12 16 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ↔ ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
18 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐺 𝑦 ) = ( 𝐴 𝐺 𝐵 ) )
19 18 fveq2d ⊢ ( 𝑦 = 𝐵 → ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) )
20 19 oveq1d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) )
21 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝑀 𝑦 ) = ( 𝐴 𝑀 𝐵 ) )
22 21 fveq2d ⊢ ( 𝑦 = 𝐵 → ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) )
23 22 oveq1d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) ↑ 2 ) )
24 20 23 oveq12d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) ↑ 2 ) ) )
25 fveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝑁 ‘ 𝑦 ) = ( 𝑁 ‘ 𝐵 ) )
26 25 oveq1d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) = ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) )
27 26 oveq2d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
28 27 oveq2d ⊢ ( 𝑦 = 𝐵 → ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )
29 24 28 eqeq12d ⊢ ( 𝑦 = 𝐵 → ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) ↔ ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) )
30 17 29 rspc2v ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) → ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) )
31 30 3adant1 ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝑥 𝑀 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝑦 ) ↑ 2 ) ) ) → ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) )
32 7 31 mpd ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )