This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ip0i

Description: A slight variant of Equation 6.46 of Ponnusamy p. 362, where J is either 1 or -1 to represent +-1. (Contributed by NM, 23-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ip1i.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
ip1i.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
ip1i.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
ip1i.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
ip1i.9 ⊢ 𝑈 ∈ CPreHilOLD
ip1i.a ⊢ 𝐴 ∈ 𝑋
ip1i.b ⊢ 𝐵 ∈ 𝑋
ip1i.c ⊢ 𝐶 ∈ 𝑋
ip1i.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
ip0i.j ⊢ 𝐽 ∈ ℂ
Assertion ip0i ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 ip1i.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 ip1i.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 ip1i.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
4 ip1i.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
5 ip1i.9 ⊢ 𝑈 ∈ CPreHilOLD
6 ip1i.a ⊢ 𝐴 ∈ 𝑋
7 ip1i.b ⊢ 𝐵 ∈ 𝑋
8 ip1i.c ⊢ 𝐶 ∈ 𝑋
9 ip1i.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
10 ip0i.j ⊢ 𝐽 ∈ ℂ
11 2cn ⊢ 2 ∈ ℂ
12 5 phnvi ⊢ 𝑈 ∈ NrmCVec
13 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐽 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) → ( 𝐽 𝑆 𝐶 ) ∈ 𝑋 )
14 12 10 8 13 mp3an ⊢ ( 𝐽 𝑆 𝐶 ) ∈ 𝑋
15 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) → ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ∈ 𝑋 )
16 12 6 14 15 mp3an ⊢ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ∈ 𝑋
17 1 9 12 16 nvcli ⊢ ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ∈ ℝ
18 17 recni ⊢ ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ∈ ℂ
19 18 sqcli ⊢ ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
20 10 negcli ⊢ - 𝐽 ∈ ℂ
21 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 𝐽 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) → ( - 𝐽 𝑆 𝐶 ) ∈ 𝑋 )
22 12 20 8 21 mp3an ⊢ ( - 𝐽 𝑆 𝐶 ) ∈ 𝑋
23 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( - 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ∈ 𝑋 )
24 12 6 22 23 mp3an ⊢ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ∈ 𝑋
25 1 9 12 24 nvcli ⊢ ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ∈ ℝ
26 25 recni ⊢ ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ∈ ℂ
27 26 sqcli ⊢ ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
28 11 19 27 subdii ⊢ ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) = ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) − ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) )
29 11 19 mulcli ⊢ ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ∈ ℂ
30 11 27 mulcli ⊢ ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ∈ ℂ
31 1 9 12 7 nvcli ⊢ ( 𝑁 ‘ 𝐵 ) ∈ ℝ
32 31 recni ⊢ ( 𝑁 ‘ 𝐵 ) ∈ ℂ
33 32 sqcli ⊢ ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ∈ ℂ
34 11 33 mulcli ⊢ ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ∈ ℂ
35 pnpcan2 ⊢ ( ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ∈ ℂ ∧ ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ∈ ℂ ∧ ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ∈ ℂ ) → ( ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) − ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) = ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) − ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) )
36 29 30 34 35 mp3an ⊢ ( ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) − ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) = ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) − ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) )
37 28 36 eqtr4i ⊢ ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) = ( ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) − ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )
38 eqid ⊢ ( 1st ‘ 𝑈 ) = ( 1st ‘ 𝑈 )
39 38 nvvc ⊢ ( 𝑈 ∈ NrmCVec → ( 1st ‘ 𝑈 ) ∈ CVecOLD )
40 2 vafval ⊢ 𝐺 = ( 1st ‘ ( 1st ‘ 𝑈 ) )
41 40 vcablo ⊢ ( ( 1st ‘ 𝑈 ) ∈ CVecOLD → 𝐺 ∈ AbelOp )
42 12 39 41 mp2b ⊢ 𝐺 ∈ AbelOp
43 6 7 14 3pm3.2i ⊢ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐽 𝑆 𝐶 ) ∈ 𝑋 )
44 1 2 bafval ⊢ 𝑋 = ran 𝐺
45 44 ablo32 ⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) = ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) )
46 42 43 45 mp2an ⊢ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) = ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 )
47 46 fveq2i ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) = ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) )
48 47 oveq1i ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) ) ↑ 2 )
49 neg1cn ⊢ - 1 ∈ ℂ
50 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 𝐵 ) ∈ 𝑋 )
51 12 49 7 50 mp3an ⊢ ( - 1 𝑆 𝐵 ) ∈ 𝑋
52 6 51 14 3pm3.2i ⊢ ( 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 ∧ ( 𝐽 𝑆 𝐶 ) ∈ 𝑋 )
53 44 ablo32 ⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 ∧ ( 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) = ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) )
54 42 52 53 mp2an ⊢ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) = ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) )
55 54 fveq2i ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) = ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) )
56 55 oveq1i ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 )
57 48 56 oveq12i ⊢ ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) )
58 1 2 3 9 phpar ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )
59 5 16 7 58 mp3an ⊢ ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
60 11 19 33 adddii ⊢ ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) = ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
61 57 59 60 3eqtri ⊢ ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) = ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
62 6 7 22 3pm3.2i ⊢ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( - 𝐽 𝑆 𝐶 ) ∈ 𝑋 )
63 44 ablo32 ⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( - 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) = ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) )
64 42 62 63 mp2an ⊢ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) = ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 )
65 64 fveq2i ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) = ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) )
66 65 oveq1i ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) ) ↑ 2 )
67 6 51 22 3pm3.2i ⊢ ( 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 ∧ ( - 𝐽 𝑆 𝐶 ) ∈ 𝑋 )
68 44 ablo32 ⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 ∧ ( - 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) = ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) )
69 42 67 68 mp2an ⊢ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) = ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) )
70 69 fveq2i ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) = ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) )
71 70 oveq1i ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 )
72 66 71 oveq12i ⊢ ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) )
73 1 2 3 9 phpar ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )
74 5 24 7 73 mp3an ⊢ ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
75 11 27 33 adddii ⊢ ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) = ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
76 72 74 75 3eqtri ⊢ ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) = ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
77 61 76 oveq12i ⊢ ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) − ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) = ( ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) − ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )
78 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
79 12 6 7 78 mp3an ⊢ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋
80 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ ( 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ∈ 𝑋 )
81 12 79 14 80 mp3an ⊢ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ∈ 𝑋
82 1 9 12 81 nvcli ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ∈ ℝ
83 82 recni ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ∈ ℂ
84 83 sqcli ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
85 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 )
86 12 6 51 85 mp3an ⊢ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋
87 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 ∧ ( 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ∈ 𝑋 )
88 12 86 14 87 mp3an ⊢ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ∈ 𝑋
89 1 9 12 88 nvcli ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ∈ ℝ
90 89 recni ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ∈ ℂ
91 90 sqcli ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
92 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ ( - 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ∈ 𝑋 )
93 12 79 22 92 mp3an ⊢ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ∈ 𝑋
94 1 9 12 93 nvcli ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ∈ ℝ
95 94 recni ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ∈ ℂ
96 95 sqcli ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
97 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 ∧ ( - 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ∈ 𝑋 )
98 12 86 22 97 mp3an ⊢ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ∈ 𝑋
99 1 9 12 98 nvcli ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ∈ ℝ
100 99 recni ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ∈ ℂ
101 100 sqcli ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
102 84 91 96 101 addsub4i ⊢ ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) − ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) = ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) )
103 37 77 102 3eqtr2ri ⊢ ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) )