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→APB‾=BPA

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