Metamath Proof Explorer

Theorem ipasslem10

Description: Lemma for ipassi . Show the inner product associative law for the imaginary number _i . (Contributed by NM, 24-Aug-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ip1i.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
ip1i.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
ip1i.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
ip1i.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
ip1i.9 ⊢ 𝑈 ∈ CPreHilOLD
ipasslem10.a ⊢ 𝐴 ∈ 𝑋
ipasslem10.b ⊢ 𝐵 ∈ 𝑋
ipasslem10.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
Assertion ipasslem10 ( ( i 𝑆 𝐴 ) 𝑃 𝐵 ) = ( i · ( 𝐴 𝑃 𝐵 ) )

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 ipasslem10.a ⊢ 𝐴 ∈ 𝑋
7 ipasslem10.b ⊢ 𝐵 ∈ 𝑋
8 ipasslem10.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
9 5 phnvi ⊢ 𝑈 ∈ NrmCVec
10 ax-icn ⊢ i ∈ ℂ
11 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ i ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( i 𝑆 𝐴 ) ∈ 𝑋 )
12 9 10 6 11 mp3an ⊢ ( i 𝑆 𝐴 ) ∈ 𝑋
13 1 2 3 8 4 4ipval2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ ( i 𝑆 𝐴 ) ∈ 𝑋 ) → ( 4 · ( 𝐵 𝑃 ( i 𝑆 𝐴 ) ) ) = ( ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) ) ) )
14 9 7 12 13 mp3an ⊢ ( 4 · ( 𝐵 𝑃 ( i 𝑆 𝐴 ) ) ) = ( ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) ) )
15 4cn ⊢ 4 ∈ ℂ
16 negicn ⊢ - i ∈ ℂ
17 1 4 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 𝑃 𝐴 ) ∈ ℂ )
18 9 7 6 17 mp3an ⊢ ( 𝐵 𝑃 𝐴 ) ∈ ℂ
19 15 16 18 mul12i ⊢ ( 4 · ( - i · ( 𝐵 𝑃 𝐴 ) ) ) = ( - i · ( 4 · ( 𝐵 𝑃 𝐴 ) ) )
20 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ ( i 𝑆 𝐴 ) ∈ 𝑋 ) → ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ∈ 𝑋 )
21 9 7 12 20 mp3an ⊢ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ∈ 𝑋
22 1 8 9 21 nvcli ⊢ ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ∈ ℝ
23 22 recni ⊢ ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ∈ ℂ
24 23 sqcli ⊢ ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) ∈ ℂ
25 neg1cn ⊢ - 1 ∈ ℂ
26 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ ( i 𝑆 𝐴 ) ∈ 𝑋 ) → ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ∈ 𝑋 )
27 9 25 12 26 mp3an ⊢ ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ∈ 𝑋
28 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ∈ 𝑋 ) → ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ∈ 𝑋 )
29 9 7 27 28 mp3an ⊢ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ∈ 𝑋
30 1 8 9 29 nvcli ⊢ ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ) ∈ ℝ
31 30 recni ⊢ ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ) ∈ ℂ
32 31 sqcli ⊢ ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ∈ ℂ
33 24 32 subcli ⊢ ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) ∈ ℂ
34 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ i ∈ ℂ ∧ ( i 𝑆 𝐴 ) ∈ 𝑋 ) → ( i 𝑆 ( i 𝑆 𝐴 ) ) ∈ 𝑋 )
35 9 10 12 34 mp3an ⊢ ( i 𝑆 ( i 𝑆 𝐴 ) ) ∈ 𝑋
36 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ ( i 𝑆 ( i 𝑆 𝐴 ) ) ∈ 𝑋 ) → ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ∈ 𝑋 )
37 9 7 35 36 mp3an ⊢ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ∈ 𝑋
38 1 8 9 37 nvcli ⊢ ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ∈ ℝ
39 38 recni ⊢ ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ∈ ℂ
40 39 sqcli ⊢ ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ∈ ℂ
41 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - i ∈ ℂ ∧ ( i 𝑆 𝐴 ) ∈ 𝑋 ) → ( - i 𝑆 ( i 𝑆 𝐴 ) ) ∈ 𝑋 )
42 9 16 12 41 mp3an ⊢ ( - i 𝑆 ( i 𝑆 𝐴 ) ) ∈ 𝑋
43 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ ( - i 𝑆 ( i 𝑆 𝐴 ) ) ∈ 𝑋 ) → ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ∈ 𝑋 )
44 9 7 42 43 mp3an ⊢ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ∈ 𝑋
45 1 8 9 44 nvcli ⊢ ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ∈ ℝ
46 45 recni ⊢ ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ∈ ℂ
47 46 sqcli ⊢ ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ∈ ℂ
48 40 47 subcli ⊢ ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) ∈ ℂ
49 10 48 mulcli ⊢ ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) ) ∈ ℂ
50 33 49 addcomi ⊢ ( ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) ) ) = ( ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) ) + ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) )
51 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 𝐺 𝐴 ) ∈ 𝑋 )
52 9 7 6 51 mp3an ⊢ ( 𝐵 𝐺 𝐴 ) ∈ 𝑋
53 1 8 9 52 nvcli ⊢ ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ∈ ℝ
54 53 recni ⊢ ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ∈ ℂ
55 54 sqcli ⊢ ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) ∈ ℂ
56 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 𝐴 ) ∈ 𝑋 )
57 9 25 6 56 mp3an ⊢ ( - 1 𝑆 𝐴 ) ∈ 𝑋
58 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ ( - 1 𝑆 𝐴 ) ∈ 𝑋 ) → ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ∈ 𝑋 )
59 9 7 57 58 mp3an ⊢ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ∈ 𝑋
60 1 8 9 59 nvcli ⊢ ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ∈ ℝ
61 60 recni ⊢ ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ∈ ℂ
62 61 sqcli ⊢ ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ∈ ℂ
63 55 62 subcli ⊢ ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ) ∈ ℂ
64 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - i ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( - i 𝑆 𝐴 ) ∈ 𝑋 )
65 9 16 6 64 mp3an ⊢ ( - i 𝑆 𝐴 ) ∈ 𝑋
66 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ ( - i 𝑆 𝐴 ) ∈ 𝑋 ) → ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ∈ 𝑋 )
67 9 7 65 66 mp3an ⊢ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ∈ 𝑋
68 1 8 9 67 nvcli ⊢ ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ∈ ℝ
69 68 recni ⊢ ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ∈ ℂ
70 69 sqcli ⊢ ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) ∈ ℂ
71 24 70 subcli ⊢ ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) ) ∈ ℂ
72 10 71 mulcli ⊢ ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) ∈ ℂ
73 16 63 72 adddii ⊢ ( - i · ( ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) ) ) = ( ( - i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) + ( - i · ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) ) )
74 10 10 6 3pm3.2i ⊢ ( i ∈ ℂ ∧ i ∈ ℂ ∧ 𝐴 ∈ 𝑋 )
75 1 3 nvsass ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( i ∈ ℂ ∧ i ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( i · i ) 𝑆 𝐴 ) = ( i 𝑆 ( i 𝑆 𝐴 ) ) )
76 9 74 75 mp2an ⊢ ( ( i · i ) 𝑆 𝐴 ) = ( i 𝑆 ( i 𝑆 𝐴 ) )
77 ixi ⊢ ( i · i ) = - 1
78 77 oveq1i ⊢ ( ( i · i ) 𝑆 𝐴 ) = ( - 1 𝑆 𝐴 )
79 76 78 eqtr3i ⊢ ( i 𝑆 ( i 𝑆 𝐴 ) ) = ( - 1 𝑆 𝐴 )
80 79 oveq2i ⊢ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) = ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) )
81 80 fveq2i ⊢ ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ) = ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) )
82 81 oveq1i ⊢ ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 )
83 10 10 mulneg1i ⊢ ( - i · i ) = - ( i · i )
84 77 negeqi ⊢ - ( i · i ) = - - 1
85 negneg1e1 ⊢ - - 1 = 1
86 83 84 85 3eqtri ⊢ ( - i · i ) = 1
87 86 oveq1i ⊢ ( ( - i · i ) 𝑆 𝐴 ) = ( 1 𝑆 𝐴 )
88 16 10 6 3pm3.2i ⊢ ( - i ∈ ℂ ∧ i ∈ ℂ ∧ 𝐴 ∈ 𝑋 )
89 1 3 nvsass ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( - i ∈ ℂ ∧ i ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( - i · i ) 𝑆 𝐴 ) = ( - i 𝑆 ( i 𝑆 𝐴 ) ) )
90 9 88 89 mp2an ⊢ ( ( - i · i ) 𝑆 𝐴 ) = ( - i 𝑆 ( i 𝑆 𝐴 ) )
91 1 3 nvsid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 1 𝑆 𝐴 ) = 𝐴 )
92 9 6 91 mp2an ⊢ ( 1 𝑆 𝐴 ) = 𝐴
93 87 90 92 3eqtr3i ⊢ ( - i 𝑆 ( i 𝑆 𝐴 ) ) = 𝐴
94 93 oveq2i ⊢ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) = ( 𝐵 𝐺 𝐴 )
95 94 fveq2i ⊢ ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ) = ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) )
96 95 oveq1i ⊢ ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 )
97 82 96 oveq12i ⊢ ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) )
98 97 oveq2i ⊢ ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) ) = ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) ) )
99 63 mulm1i ⊢ ( - 1 · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) = - ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) )
100 55 62 negsubdi2i ⊢ - ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) )
101 99 100 eqtr2i ⊢ ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) ) = ( - 1 · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ) )
102 101 oveq2i ⊢ ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) ) ) = ( i · ( - 1 · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) )
103 10 25 63 mulassi ⊢ ( ( i · - 1 ) · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) = ( i · ( - 1 · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) )
104 102 103 eqtr4i ⊢ ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) ) ) = ( ( i · - 1 ) · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ) )
105 10 mulm1i ⊢ ( - 1 · i ) = - i
106 25 10 105 mulcomli ⊢ ( i · - 1 ) = - i
107 106 oveq1i ⊢ ( ( i · - 1 ) · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) = ( - i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ) )
108 98 104 107 3eqtri ⊢ ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) ) = ( - i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ) )
109 25 10 6 3pm3.2i ⊢ ( - 1 ∈ ℂ ∧ i ∈ ℂ ∧ 𝐴 ∈ 𝑋 )
110 1 3 nvsass ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( - 1 ∈ ℂ ∧ i ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( - 1 · i ) 𝑆 𝐴 ) = ( - 1 𝑆 ( i 𝑆 𝐴 ) ) )
111 9 109 110 mp2an ⊢ ( ( - 1 · i ) 𝑆 𝐴 ) = ( - 1 𝑆 ( i 𝑆 𝐴 ) )
112 105 oveq1i ⊢ ( ( - 1 · i ) 𝑆 𝐴 ) = ( - i 𝑆 𝐴 )
113 111 112 eqtr3i ⊢ ( - 1 𝑆 ( i 𝑆 𝐴 ) ) = ( - i 𝑆 𝐴 )
114 113 oveq2i ⊢ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) = ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) )
115 114 fveq2i ⊢ ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ) = ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) )
116 115 oveq1i ⊢ ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 )
117 116 oveq2i ⊢ ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) )
118 71 mulid2i ⊢ ( 1 · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) = ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) )
119 117 118 eqtr4i ⊢ ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) = ( 1 · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) ) )
120 86 oveq1i ⊢ ( ( - i · i ) · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) = ( 1 · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) ) )
121 119 120 eqtr4i ⊢ ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) = ( ( - i · i ) · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) ) )
122 16 10 71 mulassi ⊢ ( ( - i · i ) · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) = ( - i · ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) )
123 121 122 eqtri ⊢ ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) = ( - i · ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) )
124 108 123 oveq12i ⊢ ( ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) ) + ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) ) = ( ( - i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) + ( - i · ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) ) )
125 73 124 eqtr4i ⊢ ( - i · ( ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) ) ) = ( ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) ) + ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) )
126 50 125 eqtr4i ⊢ ( ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) ) ) = ( - i · ( ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) ) )
127 1 2 3 8 4 4ipval2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 4 · ( 𝐵 𝑃 𝐴 ) ) = ( ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) ) )
128 9 7 6 127 mp3an ⊢ ( 4 · ( 𝐵 𝑃 𝐴 ) ) = ( ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) )
129 128 oveq2i ⊢ ( - i · ( 4 · ( 𝐵 𝑃 𝐴 ) ) ) = ( - i · ( ( ( ( 𝑁 ‘ ( 𝐵 𝐺 𝐴 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ↑ 2 ) ) ) ) )
130 126 129 eqtr4i ⊢ ( ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) ) ) = ( - i · ( 4 · ( 𝐵 𝑃 𝐴 ) ) )
131 19 130 eqtr4i ⊢ ( 4 · ( - i · ( 𝐵 𝑃 𝐴 ) ) ) = ( ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 𝐴 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐵 𝐺 ( i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 ( i 𝑆 𝐴 ) ) ) ) ↑ 2 ) ) ) )
132 14 131 eqtr4i ⊢ ( 4 · ( 𝐵 𝑃 ( i 𝑆 𝐴 ) ) ) = ( 4 · ( - i · ( 𝐵 𝑃 𝐴 ) ) )
133 1 4 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ ( i 𝑆 𝐴 ) ∈ 𝑋 ) → ( 𝐵 𝑃 ( i 𝑆 𝐴 ) ) ∈ ℂ )
134 9 7 12 133 mp3an ⊢ ( 𝐵 𝑃 ( i 𝑆 𝐴 ) ) ∈ ℂ
135 16 18 mulcli ⊢ ( - i · ( 𝐵 𝑃 𝐴 ) ) ∈ ℂ
136 4ne0 ⊢ 4 ≠ 0
137 134 135 15 136 mulcani ⊢ ( ( 4 · ( 𝐵 𝑃 ( i 𝑆 𝐴 ) ) ) = ( 4 · ( - i · ( 𝐵 𝑃 𝐴 ) ) ) ↔ ( 𝐵 𝑃 ( i 𝑆 𝐴 ) ) = ( - i · ( 𝐵 𝑃 𝐴 ) ) )
138 132 137 mpbi ⊢ ( 𝐵 𝑃 ( i 𝑆 𝐴 ) ) = ( - i · ( 𝐵 𝑃 𝐴 ) )
139 138 fveq2i ⊢ ( ∗ ‘ ( 𝐵 𝑃 ( i 𝑆 𝐴 ) ) ) = ( ∗ ‘ ( - i · ( 𝐵 𝑃 𝐴 ) ) )
140 1 4 dipcj ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ ( i 𝑆 𝐴 ) ∈ 𝑋 ) → ( ∗ ‘ ( 𝐵 𝑃 ( i 𝑆 𝐴 ) ) ) = ( ( i 𝑆 𝐴 ) 𝑃 𝐵 ) )
141 9 7 12 140 mp3an ⊢ ( ∗ ‘ ( 𝐵 𝑃 ( i 𝑆 𝐴 ) ) ) = ( ( i 𝑆 𝐴 ) 𝑃 𝐵 )
142 16 18 cjmuli ⊢ ( ∗ ‘ ( - i · ( 𝐵 𝑃 𝐴 ) ) ) = ( ( ∗ ‘ - i ) · ( ∗ ‘ ( 𝐵 𝑃 𝐴 ) ) )
143 25 10 cjmuli ⊢ ( ∗ ‘ ( - 1 · i ) ) = ( ( ∗ ‘ - 1 ) · ( ∗ ‘ i ) )
144 105 fveq2i ⊢ ( ∗ ‘ ( - 1 · i ) ) = ( ∗ ‘ - i )
145 neg1rr ⊢ - 1 ∈ ℝ
146 25 cjrebi ⊢ ( - 1 ∈ ℝ ↔ ( ∗ ‘ - 1 ) = - 1 )
147 145 146 mpbi ⊢ ( ∗ ‘ - 1 ) = - 1
148 cji ⊢ ( ∗ ‘ i ) = - i
149 147 148 oveq12i ⊢ ( ( ∗ ‘ - 1 ) · ( ∗ ‘ i ) ) = ( - 1 · - i )
150 ax-1cn ⊢ 1 ∈ ℂ
151 150 10 mul2negi ⊢ ( - 1 · - i ) = ( 1 · i )
152 10 mulid2i ⊢ ( 1 · i ) = i
153 149 151 152 3eqtri ⊢ ( ( ∗ ‘ - 1 ) · ( ∗ ‘ i ) ) = i
154 143 144 153 3eqtr3i ⊢ ( ∗ ‘ - i ) = i
155 1 4 dipcj ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ∗ ‘ ( 𝐵 𝑃 𝐴 ) ) = ( 𝐴 𝑃 𝐵 ) )
156 9 7 6 155 mp3an ⊢ ( ∗ ‘ ( 𝐵 𝑃 𝐴 ) ) = ( 𝐴 𝑃 𝐵 )
157 154 156 oveq12i ⊢ ( ( ∗ ‘ - i ) · ( ∗ ‘ ( 𝐵 𝑃 𝐴 ) ) ) = ( i · ( 𝐴 𝑃 𝐵 ) )
158 142 157 eqtri ⊢ ( ∗ ‘ ( - i · ( 𝐵 𝑃 𝐴 ) ) ) = ( i · ( 𝐴 𝑃 𝐵 ) )
159 139 141 158 3eqtr3i ⊢ ( ( i 𝑆 𝐴 ) 𝑃 𝐵 ) = ( i · ( 𝐴 𝑃 𝐵 ) )