Metamath Proof Explorer

Theorem dipcj

Description: The complex conjugate of an inner product reverses its arguments. Equation I1 of Ponnusamy p. 362. (Contributed by NM, 1-Feb-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ipcl.1 ⊢ X = BaseSet ⁡ U
ipcl.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
Assertion dipcj ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A P B ‾ = B P A

Proof

Step Hyp Ref Expression
1 ipcl.1 ⊢ X = BaseSet ⁡ U
2 ipcl.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
3 eqid ⊢ + v ⁡ U = + v ⁡ U
4 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
5 eqid ⊢ norm CV ⁡ U = norm CV ⁡ U
6 1 3 4 5 2 ipval2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A P B = norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 4
7 6 fveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A P B ‾ = norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 4 ‾
8 1 3 4 5 2 ipval2 ⊢ U ∈ NrmCVec ∧ B ∈ X ∧ A ∈ X → B P A = norm CV ⁡ U ⁡ B + v ⁡ U A 2 - norm CV ⁡ U ⁡ B + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A 2 + i ⁢ norm CV ⁡ U ⁡ B + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − norm CV ⁡ U ⁡ B + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2 4
9 8 3com23 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → B P A = norm CV ⁡ U ⁡ B + v ⁡ U A 2 - norm CV ⁡ U ⁡ B + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A 2 + i ⁢ norm CV ⁡ U ⁡ B + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − norm CV ⁡ U ⁡ B + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2 4
10 1 3 4 5 2 ipval2lem3 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U B 2 ∈ ℝ
11 10 recnd ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U B 2 ∈ ℂ
12 neg1cn ⊢ − 1 ∈ ℂ
13 1 3 4 5 2 ipval2lem4 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ − 1 ∈ ℂ → norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 ∈ ℂ
14 12 13 mpan2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 ∈ ℂ
15 11 14 subcld ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 ∈ ℂ
16 ax-icn ⊢ i ∈ ℂ
17 1 3 4 5 2 ipval2lem4 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ i ∈ ℂ → norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 ∈ ℂ
18 16 17 mpan2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 ∈ ℂ
19 negicn ⊢ − i ∈ ℂ
20 1 3 4 5 2 ipval2lem4 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ − i ∈ ℂ → norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ∈ ℂ
21 19 20 mpan2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ∈ ℂ
22 18 21 subcld ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ∈ ℂ
23 mulcl ⊢ i ∈ ℂ ∧ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ∈ ℂ → i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ∈ ℂ
24 16 22 23 sylancr ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ∈ ℂ
25 15 24 addcld ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ∈ ℂ
26 4cn ⊢ 4 ∈ ℂ
27 4ne0 ⊢ 4 ≠ 0
28 cjdiv ⊢ norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ∈ ℂ ∧ 4 ∈ ℂ ∧ 4 ≠ 0 → norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 4 ‾ = norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ‾ 4 ‾
29 26 27 28 mp3an23 ⊢ norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ∈ ℂ → norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 4 ‾ = norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ‾ 4 ‾
30 25 29 syl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 4 ‾ = norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ‾ 4 ‾
31 4re ⊢ 4 ∈ ℝ
32 cjre ⊢ 4 ∈ ℝ → 4 ‾ = 4
33 31 32 ax-mp ⊢ 4 ‾ = 4
34 33 oveq2i ⊢ norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ‾ 4 ‾ = norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ‾ 4
35 1 3 4 5 2 ipval2lem2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ − 1 ∈ ℂ → norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 ∈ ℝ
36 12 35 mpan2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 ∈ ℝ
37 10 36 resubcld ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 ∈ ℝ
38 1 3 4 5 2 ipval2lem2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ i ∈ ℂ → norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 ∈ ℝ
39 16 38 mpan2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 ∈ ℝ
40 1 3 4 5 2 ipval2lem2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ − i ∈ ℂ → norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ∈ ℝ
41 19 40 mpan2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ∈ ℝ
42 39 41 resubcld ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ∈ ℝ
43 cjreim ⊢ norm CV ⁡ U ⁡ A + v ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 ∈ ℝ ∧ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ∈ ℝ → norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ‾ = norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 - i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2
44 37 42 43 syl2anc ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ‾ = norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 - i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2
45 submul2 ⊢ norm CV ⁡ U ⁡ A + v ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 ∈ ℂ ∧ i ∈ ℂ ∧ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ∈ ℂ → norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 - i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 = norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ − norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2
46 16 45 mp3an2 ⊢ norm CV ⁡ U ⁡ A + v ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 ∈ ℂ ∧ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ∈ ℂ → norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 - i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 = norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ − norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2
47 15 22 46 syl2anc ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 - i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 = norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ − norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2
48 1 3 nvcom ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A + v ⁡ U B = B + v ⁡ U A
49 48 fveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U B = norm CV ⁡ U ⁡ B + v ⁡ U A
50 49 oveq1d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U B 2 = norm CV ⁡ U ⁡ B + v ⁡ U A 2
51 1 3 4 5 nvdif ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B = norm CV ⁡ U ⁡ B + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A
52 51 oveq1d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 = norm CV ⁡ U ⁡ B + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A 2
53 50 52 oveq12d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 = norm CV ⁡ U ⁡ B + v ⁡ U A 2 − norm CV ⁡ U ⁡ B + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A 2
54 18 21 negsubdi2d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → − norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 = norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2
55 1 3 4 5 nvpi ⊢ U ∈ NrmCVec ∧ B ∈ X ∧ A ∈ X → norm CV ⁡ U ⁡ B + v ⁡ U i ⋅ 𝑠OLD ⁡ U A = norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B
56 55 3com23 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ B + v ⁡ U i ⋅ 𝑠OLD ⁡ U A = norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B
57 56 eqcomd ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B = norm CV ⁡ U ⁡ B + v ⁡ U i ⋅ 𝑠OLD ⁡ U A
58 57 oveq1d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 = norm CV ⁡ U ⁡ B + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2
59 1 3 4 5 nvpi ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B = norm CV ⁡ U ⁡ B + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A
60 59 oveq1d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 = norm CV ⁡ U ⁡ B + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2
61 58 60 oveq12d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 = norm CV ⁡ U ⁡ B + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − norm CV ⁡ U ⁡ B + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2
62 54 61 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → − norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 = norm CV ⁡ U ⁡ B + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − norm CV ⁡ U ⁡ B + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2
63 62 oveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → i ⁢ − norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 = i ⁢ norm CV ⁡ U ⁡ B + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − norm CV ⁡ U ⁡ B + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2
64 53 63 oveq12d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ − norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 = norm CV ⁡ U ⁡ B + v ⁡ U A 2 - norm CV ⁡ U ⁡ B + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A 2 + i ⁢ norm CV ⁡ U ⁡ B + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − norm CV ⁡ U ⁡ B + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2
65 44 47 64 3eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ‾ = norm CV ⁡ U ⁡ B + v ⁡ U A 2 - norm CV ⁡ U ⁡ B + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A 2 + i ⁢ norm CV ⁡ U ⁡ B + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − norm CV ⁡ U ⁡ B + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2
66 65 oveq1d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ‾ 4 = norm CV ⁡ U ⁡ B + v ⁡ U A 2 - norm CV ⁡ U ⁡ B + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A 2 + i ⁢ norm CV ⁡ U ⁡ B + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − norm CV ⁡ U ⁡ B + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2 4
67 34 66 syl5eq ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 ‾ 4 ‾ = norm CV ⁡ U ⁡ B + v ⁡ U A 2 - norm CV ⁡ U ⁡ B + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A 2 + i ⁢ norm CV ⁡ U ⁡ B + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − norm CV ⁡ U ⁡ B + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2 4
68 30 67 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 4 ‾ = norm CV ⁡ U ⁡ B + v ⁡ U A 2 - norm CV ⁡ U ⁡ B + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A 2 + i ⁢ norm CV ⁡ U ⁡ B + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − norm CV ⁡ U ⁡ B + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2 4
69 9 68 eqtr4d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → B P A = norm CV ⁡ U ⁡ A + v ⁡ U B 2 - norm CV ⁡ U ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B 2 + i ⁢ norm CV ⁡ U ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U B 2 − norm CV ⁡ U ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U B 2 4 ‾
70 7 69 eqtr4d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A P B ‾ = B P A