Metamath Proof Explorer

Theorem nmparlem

Description: Lemma for nmpar . (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses nmpar.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
nmpar.p ⊢ + = ( +g ‘ 𝑊 )
nmpar.m ⊢ − = ( -g ‘ 𝑊 )
nmpar.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
nmpar.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
nmpar.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
nmpar.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
nmpar.1 ⊢ ( 𝜑 → 𝑊 ∈ ℂPreHil )
nmpar.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
nmpar.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
Assertion nmparlem ( 𝜑 → ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 nmpar.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 nmpar.p ⊢ + = ( +g ‘ 𝑊 )
3 nmpar.m ⊢ − = ( -g ‘ 𝑊 )
4 nmpar.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
5 nmpar.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
6 nmpar.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
7 nmpar.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
8 nmpar.1 ⊢ ( 𝜑 → 𝑊 ∈ ℂPreHil )
9 nmpar.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
10 nmpar.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
11 5 1 2 8 9 10 9 10 cph2di ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) , ( 𝐴 + 𝐵 ) ) = ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) )
12 5 1 3 8 9 10 9 10 cph2subdi ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) , ( 𝐴 − 𝐵 ) ) = ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) − ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) )
13 11 12 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) , ( 𝐴 + 𝐵 ) ) + ( ( 𝐴 − 𝐵 ) , ( 𝐴 − 𝐵 ) ) ) = ( ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) + ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) − ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) ) )
14 cphclm ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )
15 8 14 syl ⊢ ( 𝜑 → 𝑊 ∈ ℂMod )
16 6 7 clmsscn ⊢ ( 𝑊 ∈ ℂMod → 𝐾 ⊆ ℂ )
17 15 16 syl ⊢ ( 𝜑 → 𝐾 ⊆ ℂ )
18 cphphl ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil )
19 8 18 syl ⊢ ( 𝜑 → 𝑊 ∈ PreHil )
20 6 5 1 7 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 , 𝐴 ) ∈ 𝐾 )
21 19 9 9 20 syl3anc ⊢ ( 𝜑 → ( 𝐴 , 𝐴 ) ∈ 𝐾 )
22 6 5 1 7 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐵 , 𝐵 ) ∈ 𝐾 )
23 19 10 10 22 syl3anc ⊢ ( 𝜑 → ( 𝐵 , 𝐵 ) ∈ 𝐾 )
24 6 7 clmacl ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 , 𝐴 ) ∈ 𝐾 ∧ ( 𝐵 , 𝐵 ) ∈ 𝐾 ) → ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) ∈ 𝐾 )
25 15 21 23 24 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) ∈ 𝐾 )
26 17 25 sseldd ⊢ ( 𝜑 → ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) ∈ ℂ )
27 6 5 1 7 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 , 𝐵 ) ∈ 𝐾 )
28 19 9 10 27 syl3anc ⊢ ( 𝜑 → ( 𝐴 , 𝐵 ) ∈ 𝐾 )
29 6 5 1 7 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐵 , 𝐴 ) ∈ 𝐾 )
30 19 10 9 29 syl3anc ⊢ ( 𝜑 → ( 𝐵 , 𝐴 ) ∈ 𝐾 )
31 6 7 clmacl ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 , 𝐵 ) ∈ 𝐾 ∧ ( 𝐵 , 𝐴 ) ∈ 𝐾 ) → ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ∈ 𝐾 )
32 15 28 30 31 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ∈ 𝐾 )
33 17 32 sseldd ⊢ ( 𝜑 → ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ∈ ℂ )
34 26 33 26 ppncand ⊢ ( 𝜑 → ( ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) + ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) − ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) ) = ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) + ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) ) )
35 13 34 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) , ( 𝐴 + 𝐵 ) ) + ( ( 𝐴 − 𝐵 ) , ( 𝐴 − 𝐵 ) ) ) = ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) + ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) ) )
36 cphlmod ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod )
37 8 36 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
38 1 2 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 + 𝐵 ) ∈ 𝑉 )
39 37 9 10 38 syl3anc ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ 𝑉 )
40 1 5 4 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 + 𝐵 ) ∈ 𝑉 ) → ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 + 𝐵 ) , ( 𝐴 + 𝐵 ) ) )
41 8 39 40 syl2anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 + 𝐵 ) , ( 𝐴 + 𝐵 ) ) )
42 1 3 lmodvsubcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 − 𝐵 ) ∈ 𝑉 )
43 37 9 10 42 syl3anc ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ 𝑉 )
44 1 5 4 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 − 𝐵 ) ∈ 𝑉 ) → ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 − 𝐵 ) , ( 𝐴 − 𝐵 ) ) )
45 8 43 44 syl2anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 − 𝐵 ) , ( 𝐴 − 𝐵 ) ) )
46 41 45 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝐴 + 𝐵 ) , ( 𝐴 + 𝐵 ) ) + ( ( 𝐴 − 𝐵 ) , ( 𝐴 − 𝐵 ) ) ) )
47 1 5 4 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 , 𝐴 ) )
48 8 9 47 syl2anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 , 𝐴 ) )
49 1 5 4 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) = ( 𝐵 , 𝐵 ) )
50 8 10 49 syl2anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) = ( 𝐵 , 𝐵 ) )
51 48 50 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) = ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) )
52 51 oveq2d ⊢ ( 𝜑 → ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) = ( 2 · ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) ) )
53 26 2timesd ⊢ ( 𝜑 → ( 2 · ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) ) = ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) + ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) ) )
54 52 53 eqtrd ⊢ ( 𝜑 → ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) = ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) + ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) ) )
55 35 46 54 3eqtr4d ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )