Metamath Proof Explorer

Theorem ip1ilem

Description: Lemma for ip1i . (Contributed by NM, 21-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 ip1ilem ( ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) + ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝑃 𝐶 ) ) = ( 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 5 phnvi ⊢ 𝑈 ∈ NrmCVec
12 1 2 3 9 4 4ipval2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 4 · ( 𝐴 𝑃 𝐶 ) ) = ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) )
13 11 6 8 12 mp3an ⊢ ( 4 · ( 𝐴 𝑃 𝐶 ) ) = ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) )
14 13 oveq2i ⊢ ( 2 · ( 4 · ( 𝐴 𝑃 𝐶 ) ) ) = ( 2 · ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) )
15 2cn ⊢ 2 ∈ ℂ
16 4cn ⊢ 4 ∈ ℂ
17 1 4 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐶 ) ∈ ℂ )
18 11 6 8 17 mp3an ⊢ ( 𝐴 𝑃 𝐶 ) ∈ ℂ
19 15 16 18 mul12i ⊢ ( 2 · ( 4 · ( 𝐴 𝑃 𝐶 ) ) ) = ( 4 · ( 2 · ( 𝐴 𝑃 𝐶 ) ) )
20 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐶 ) ∈ 𝑋 )
21 11 6 8 20 mp3an ⊢ ( 𝐴 𝐺 𝐶 ) ∈ 𝑋
22 1 9 11 21 nvcli ⊢ ( 𝑁 ‘ ( 𝐴 𝐺 𝐶 ) ) ∈ ℝ
23 22 resqcli ⊢ ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐶 ) ) ↑ 2 ) ∈ ℝ
24 23 recni ⊢ ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐶 ) ) ↑ 2 ) ∈ ℂ
25 ax-1cn ⊢ 1 ∈ ℂ
26 25 negcli ⊢ - 1 ∈ ℂ
27 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) → ( - 1 𝑆 𝐶 ) ∈ 𝑋 )
28 11 26 8 27 mp3an ⊢ ( - 1 𝑆 𝐶 ) ∈ 𝑋
29 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐶 ) ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ∈ 𝑋 )
30 11 6 28 29 mp3an ⊢ ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ∈ 𝑋
31 1 9 11 30 nvcli ⊢ ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ) ∈ ℝ
32 31 resqcli ⊢ ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℝ
33 32 recni ⊢ ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
34 24 33 subcli ⊢ ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) ∈ ℂ
35 ax-icn ⊢ i ∈ ℂ
36 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ i ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) → ( i 𝑆 𝐶 ) ∈ 𝑋 )
37 11 35 8 36 mp3an ⊢ ( i 𝑆 𝐶 ) ∈ 𝑋
38 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( i 𝑆 𝐶 ) ∈ 𝑋 ) → ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ∈ 𝑋 )
39 11 6 37 38 mp3an ⊢ ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ∈ 𝑋
40 1 9 11 39 nvcli ⊢ ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ) ∈ ℝ
41 40 resqcli ⊢ ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℝ
42 41 recni ⊢ ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
43 35 negcli ⊢ - i ∈ ℂ
44 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - i ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) → ( - i 𝑆 𝐶 ) ∈ 𝑋 )
45 11 43 8 44 mp3an ⊢ ( - i 𝑆 𝐶 ) ∈ 𝑋
46 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( - i 𝑆 𝐶 ) ∈ 𝑋 ) → ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ∈ 𝑋 )
47 11 6 45 46 mp3an ⊢ ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ∈ 𝑋
48 1 9 11 47 nvcli ⊢ ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ) ∈ ℝ
49 48 resqcli ⊢ ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℝ
50 49 recni ⊢ ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
51 42 50 subcli ⊢ ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ∈ ℂ
52 35 51 mulcli ⊢ ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ∈ ℂ
53 15 34 52 adddii ⊢ ( 2 · ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) ) = ( ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) + ( 2 · ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) )
54 1 2 3 4 5 6 7 8 9 25 ip0i ⊢ ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 1 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 1 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 1 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) )
55 1 3 nvsid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐶 ∈ 𝑋 ) → ( 1 𝑆 𝐶 ) = 𝐶 )
56 11 8 55 mp2an ⊢ ( 1 𝑆 𝐶 ) = 𝐶
57 56 oveq2i ⊢ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 1 𝑆 𝐶 ) ) = ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 )
58 57 fveq2i ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 1 𝑆 𝐶 ) ) ) = ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) )
59 58 oveq1i ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 1 𝑆 𝐶 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) ) ↑ 2 )
60 59 oveq1i ⊢ ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 1 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) )
61 56 oveq2i ⊢ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 1 𝑆 𝐶 ) ) = ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 )
62 61 fveq2i ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 1 𝑆 𝐶 ) ) ) = ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 ) )
63 62 oveq1i ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 1 𝑆 𝐶 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 ) ) ↑ 2 )
64 63 oveq1i ⊢ ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 1 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) )
65 60 64 oveq12i ⊢ ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 1 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 1 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) = ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) )
66 56 oveq2i ⊢ ( 𝐴 𝐺 ( 1 𝑆 𝐶 ) ) = ( 𝐴 𝐺 𝐶 )
67 66 fveq2i ⊢ ( 𝑁 ‘ ( 𝐴 𝐺 ( 1 𝑆 𝐶 ) ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 𝐶 ) )
68 67 oveq1i ⊢ ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 1 𝑆 𝐶 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐶 ) ) ↑ 2 )
69 68 oveq1i ⊢ ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 1 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) )
70 69 oveq2i ⊢ ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 1 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) )
71 54 65 70 3eqtr3i ⊢ ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) )
72 1 2 3 4 5 6 7 8 9 35 ip0i ⊢ ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) )
73 72 oveq2i ⊢ ( i · ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) = ( i · ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) )
74 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
75 11 6 7 74 mp3an ⊢ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋
76 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ ( i 𝑆 𝐶 ) ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ∈ 𝑋 )
77 11 75 37 76 mp3an ⊢ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ∈ 𝑋
78 1 9 11 77 nvcli ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ) ∈ ℝ
79 78 resqcli ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℝ
80 79 recni ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
81 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ ( - i 𝑆 𝐶 ) ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ∈ 𝑋 )
82 11 75 45 81 mp3an ⊢ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ∈ 𝑋
83 1 9 11 82 nvcli ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ∈ ℝ
84 83 resqcli ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℝ
85 84 recni ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
86 80 85 subcli ⊢ ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ∈ ℂ
87 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 𝐵 ) ∈ 𝑋 )
88 11 26 7 87 mp3an ⊢ ( - 1 𝑆 𝐵 ) ∈ 𝑋
89 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 )
90 11 6 88 89 mp3an ⊢ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋
91 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 ∧ ( i 𝑆 𝐶 ) ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ∈ 𝑋 )
92 11 90 37 91 mp3an ⊢ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ∈ 𝑋
93 1 9 11 92 nvcli ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ) ∈ ℝ
94 93 resqcli ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℝ
95 94 recni ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
96 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 ∧ ( - i 𝑆 𝐶 ) ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ∈ 𝑋 )
97 11 90 45 96 mp3an ⊢ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ∈ 𝑋
98 1 9 11 97 nvcli ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ∈ ℝ
99 98 resqcli ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℝ
100 99 recni ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
101 95 100 subcli ⊢ ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ∈ ℂ
102 35 86 101 adddii ⊢ ( i · ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) = ( ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) + ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) )
103 35 15 51 mul12i ⊢ ( i · ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) = ( 2 · ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) )
104 73 102 103 3eqtr3i ⊢ ( ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) + ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) = ( 2 · ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) )
105 71 104 oveq12i ⊢ ( ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) + ( ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) + ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) ) = ( ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) + ( 2 · ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) )
106 53 105 eqtr4i ⊢ ( 2 · ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) ) = ( ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) + ( ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) + ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) )
107 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) ∈ 𝑋 )
108 11 75 8 107 mp3an ⊢ ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) ∈ 𝑋
109 1 9 11 108 nvcli ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) ) ∈ ℝ
110 109 resqcli ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) ) ↑ 2 ) ∈ ℝ
111 110 recni ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) ) ↑ 2 ) ∈ ℂ
112 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ ( - 1 𝑆 𝐶 ) ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ∈ 𝑋 )
113 11 75 28 112 mp3an ⊢ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ∈ 𝑋
114 1 9 11 113 nvcli ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ∈ ℝ
115 114 resqcli ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℝ
116 115 recni ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
117 111 116 subcli ⊢ ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) ∈ ℂ
118 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 ) ∈ 𝑋 )
119 11 90 8 118 mp3an ⊢ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 ) ∈ 𝑋
120 1 9 11 119 nvcli ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 ) ) ∈ ℝ
121 120 resqcli ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 ) ) ↑ 2 ) ∈ ℝ
122 121 recni ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 ) ) ↑ 2 ) ∈ ℂ
123 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 ∧ ( - 1 𝑆 𝐶 ) ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ∈ 𝑋 )
124 11 90 28 123 mp3an ⊢ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ∈ 𝑋
125 1 9 11 124 nvcli ⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ∈ ℝ
126 125 resqcli ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℝ
127 126 recni ⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
128 122 127 subcli ⊢ ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) ∈ ℂ
129 35 86 mulcli ⊢ ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ∈ ℂ
130 35 101 mulcli ⊢ ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ∈ ℂ
131 117 128 129 130 add4i ⊢ ( ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) + ( ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) + ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) ) = ( ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) + ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) )
132 1 4 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) ∈ ℂ )
133 11 75 8 132 mp3an ⊢ ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) ∈ ℂ
134 1 4 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝑃 𝐶 ) ∈ ℂ )
135 11 90 8 134 mp3an ⊢ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝑃 𝐶 ) ∈ ℂ
136 16 133 135 adddii ⊢ ( 4 · ( ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) + ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝑃 𝐶 ) ) ) = ( ( 4 · ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) ) + ( 4 · ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝑃 𝐶 ) ) )
137 1 2 3 9 4 4ipval2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 4 · ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) ) = ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) )
138 11 75 8 137 mp3an ⊢ ( 4 · ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) ) = ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) )
139 1 2 3 9 4 4ipval2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 4 · ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝑃 𝐶 ) ) = ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) )
140 11 90 8 139 mp3an ⊢ ( 4 · ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝑃 𝐶 ) ) = ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) )
141 138 140 oveq12i ⊢ ( ( 4 · ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) ) + ( 4 · ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝑃 𝐶 ) ) ) = ( ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) + ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) )
142 136 141 eqtr2i ⊢ ( ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) + ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) ) = ( 4 · ( ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) + ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝑃 𝐶 ) ) )
143 106 131 142 3eqtri ⊢ ( 2 · ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐶 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) ) ) = ( 4 · ( ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) + ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝑃 𝐶 ) ) )
144 14 19 143 3eqtr3ri ⊢ ( 4 · ( ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) + ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝑃 𝐶 ) ) ) = ( 4 · ( 2 · ( 𝐴 𝑃 𝐶 ) ) )
145 144 oveq1i ⊢ ( ( 4 · ( ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) + ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝑃 𝐶 ) ) ) / 4 ) = ( ( 4 · ( 2 · ( 𝐴 𝑃 𝐶 ) ) ) / 4 )
146 133 135 addcli ⊢ ( ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) + ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝑃 𝐶 ) ) ∈ ℂ
147 4ne0 ⊢ 4 ≠ 0
148 146 16 147 divcan3i ⊢ ( ( 4 · ( ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) + ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝑃 𝐶 ) ) ) / 4 ) = ( ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) + ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝑃 𝐶 ) )
149 15 18 mulcli ⊢ ( 2 · ( 𝐴 𝑃 𝐶 ) ) ∈ ℂ
150 149 16 147 divcan3i ⊢ ( ( 4 · ( 2 · ( 𝐴 𝑃 𝐶 ) ) ) / 4 ) = ( 2 · ( 𝐴 𝑃 𝐶 ) )
151 145 148 150 3eqtr3i ⊢ ( ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) + ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝑃 𝐶 ) ) = ( 2 · ( 𝐴 𝑃 𝐶 ) )