Metamath Proof Explorer

Theorem ipdirilem

Description: Lemma for ipdiri . (Contributed by NM, 26-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ip1i.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
ip1i.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
ip1i.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
ip1i.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
ip1i.9 ⊢ 𝑈 ∈ CPreHilOLD
ipdiri.8 ⊢ 𝐴 ∈ 𝑋
ipdiri.9 ⊢ 𝐵 ∈ 𝑋
ipdiri.10 ⊢ 𝐶 ∈ 𝑋
Assertion ipdirilem ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) )

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 ipdiri.8 ⊢ 𝐴 ∈ 𝑋
7 ipdiri.9 ⊢ 𝐵 ∈ 𝑋
8 ipdiri.10 ⊢ 𝐶 ∈ 𝑋
9 2thalfe1 ⊢ ( 2 · ( 1 / 2 ) ) = 1
10 9 oveq1i ⊢ ( ( 2 · ( 1 / 2 ) ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) = ( 1 𝑆 ( 𝐴 𝐺 𝐵 ) )
11 5 phnvi ⊢ 𝑈 ∈ NrmCVec
12 2cn ⊢ 2 ∈ ℂ
13 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
14 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
15 11 6 7 14 mp3an ⊢ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋
16 12 13 15 3pm3.2i ⊢ ( 2 ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
17 1 3 nvsass ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 2 ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ) ) → ( ( 2 · ( 1 / 2 ) ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) = ( 2 𝑆 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) ) )
18 11 16 17 mp2an ⊢ ( ( 2 · ( 1 / 2 ) ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) = ( 2 𝑆 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) )
19 1 3 nvsid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ) → ( 1 𝑆 ( 𝐴 𝐺 𝐵 ) ) = ( 𝐴 𝐺 𝐵 ) )
20 11 15 19 mp2an ⊢ ( 1 𝑆 ( 𝐴 𝐺 𝐵 ) ) = ( 𝐴 𝐺 𝐵 )
21 10 18 20 3eqtr3i ⊢ ( 2 𝑆 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) ) = ( 𝐴 𝐺 𝐵 )
22 21 oveq1i ⊢ ( ( 2 𝑆 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) ) 𝑃 𝐶 ) = ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 )
23 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 1 / 2 ) ∈ ℂ ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ) → ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) ∈ 𝑋 )
24 11 13 15 23 mp3an ⊢ ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) ∈ 𝑋
25 1 2 3 4 5 24 8 ip2i ⊢ ( ( 2 𝑆 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) ) 𝑃 𝐶 ) = ( 2 · ( ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) 𝑃 𝐶 ) )
26 22 25 eqtr3i ⊢ ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) = ( 2 · ( ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) 𝑃 𝐶 ) )
27 neg1cn ⊢ - 1 ∈ ℂ
28 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 𝐵 ) ∈ 𝑋 )
29 11 27 7 28 mp3an ⊢ ( - 1 𝑆 𝐵 ) ∈ 𝑋
30 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 )
31 11 6 29 30 mp3an ⊢ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋
32 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 1 / 2 ) ∈ ℂ ∧ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 ) → ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ∈ 𝑋 )
33 11 13 31 32 mp3an ⊢ ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ∈ 𝑋
34 1 2 3 4 5 24 33 8 ip1i ⊢ ( ( ( ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) 𝐺 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) 𝑃 𝐶 ) + ( ( ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) 𝐺 ( - 1 𝑆 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) ) 𝑃 𝐶 ) ) = ( 2 · ( ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) 𝑃 𝐶 ) )
35 eqid ⊢ ( 1st ‘ 𝑈 ) = ( 1st ‘ 𝑈 )
36 35 nvvc ⊢ ( 𝑈 ∈ NrmCVec → ( 1st ‘ 𝑈 ) ∈ CVecOLD )
37 11 36 ax-mp ⊢ ( 1st ‘ 𝑈 ) ∈ CVecOLD
38 2 vafval ⊢ 𝐺 = ( 1st ‘ ( 1st ‘ 𝑈 ) )
39 38 vcablo ⊢ ( ( 1st ‘ 𝑈 ) ∈ CVecOLD → 𝐺 ∈ AbelOp )
40 37 39 ax-mp ⊢ 𝐺 ∈ AbelOp
41 6 7 pm3.2i ⊢ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 )
42 6 29 pm3.2i ⊢ ( 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 )
43 1 2 bafval ⊢ 𝑋 = ran 𝐺
44 43 ablo4 ⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) = ( ( 𝐴 𝐺 𝐴 ) 𝐺 ( 𝐵 𝐺 ( - 1 𝑆 𝐵 ) ) ) )
45 40 41 42 44 mp3an ⊢ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) = ( ( 𝐴 𝐺 𝐴 ) 𝐺 ( 𝐵 𝐺 ( - 1 𝑆 𝐵 ) ) )
46 3 smfval ⊢ 𝑆 = ( 2nd ‘ ( 1st ‘ 𝑈 ) )
47 38 46 43 vc2OLD ⊢ ( ( ( 1st ‘ 𝑈 ) ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐴 ) = ( 2 𝑆 𝐴 ) )
48 37 6 47 mp2an ⊢ ( 𝐴 𝐺 𝐴 ) = ( 2 𝑆 𝐴 )
49 eqid ⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
50 1 2 3 49 nvrinv ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝐺 ( - 1 𝑆 𝐵 ) ) = ( 0vec ‘ 𝑈 ) )
51 11 7 50 mp2an ⊢ ( 𝐵 𝐺 ( - 1 𝑆 𝐵 ) ) = ( 0vec ‘ 𝑈 )
52 48 51 oveq12i ⊢ ( ( 𝐴 𝐺 𝐴 ) 𝐺 ( 𝐵 𝐺 ( - 1 𝑆 𝐵 ) ) ) = ( ( 2 𝑆 𝐴 ) 𝐺 ( 0vec ‘ 𝑈 ) )
53 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 2 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( 2 𝑆 𝐴 ) ∈ 𝑋 )
54 11 12 6 53 mp3an ⊢ ( 2 𝑆 𝐴 ) ∈ 𝑋
55 1 2 49 nv0rid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 2 𝑆 𝐴 ) ∈ 𝑋 ) → ( ( 2 𝑆 𝐴 ) 𝐺 ( 0vec ‘ 𝑈 ) ) = ( 2 𝑆 𝐴 ) )
56 11 54 55 mp2an ⊢ ( ( 2 𝑆 𝐴 ) 𝐺 ( 0vec ‘ 𝑈 ) ) = ( 2 𝑆 𝐴 )
57 45 52 56 3eqtri ⊢ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) = ( 2 𝑆 𝐴 )
58 57 oveq2i ⊢ ( ( 1 / 2 ) 𝑆 ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) = ( ( 1 / 2 ) 𝑆 ( 2 𝑆 𝐴 ) )
59 13 12 6 3pm3.2i ⊢ ( ( 1 / 2 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐴 ∈ 𝑋 )
60 1 3 nvsass ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( ( 1 / 2 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( ( 1 / 2 ) · 2 ) 𝑆 𝐴 ) = ( ( 1 / 2 ) 𝑆 ( 2 𝑆 𝐴 ) ) )
61 11 59 60 mp2an ⊢ ( ( ( 1 / 2 ) · 2 ) 𝑆 𝐴 ) = ( ( 1 / 2 ) 𝑆 ( 2 𝑆 𝐴 ) )
62 58 61 eqtr4i ⊢ ( ( 1 / 2 ) 𝑆 ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) = ( ( ( 1 / 2 ) · 2 ) 𝑆 𝐴 )
63 13 15 31 3pm3.2i ⊢ ( ( 1 / 2 ) ∈ ℂ ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 )
64 1 2 3 nvdi ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( ( 1 / 2 ) ∈ ℂ ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 ) ) → ( ( 1 / 2 ) 𝑆 ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) = ( ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) 𝐺 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) )
65 11 63 64 mp2an ⊢ ( ( 1 / 2 ) 𝑆 ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) = ( ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) 𝐺 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) )
66 ax-1cn ⊢ 1 ∈ ℂ
67 2ne0 ⊢ 2 ≠ 0
68 66 12 67 divcan1i ⊢ ( ( 1 / 2 ) · 2 ) = 1
69 68 oveq1i ⊢ ( ( ( 1 / 2 ) · 2 ) 𝑆 𝐴 ) = ( 1 𝑆 𝐴 )
70 1 3 nvsid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 1 𝑆 𝐴 ) = 𝐴 )
71 11 6 70 mp2an ⊢ ( 1 𝑆 𝐴 ) = 𝐴
72 69 71 eqtri ⊢ ( ( ( 1 / 2 ) · 2 ) 𝑆 𝐴 ) = 𝐴
73 62 65 72 3eqtr3i ⊢ ( ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) 𝐺 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) = 𝐴
74 73 oveq1i ⊢ ( ( ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) 𝐺 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) 𝑃 𝐶 ) = ( 𝐴 𝑃 𝐶 )
75 27 13 mulcomi ⊢ ( - 1 · ( 1 / 2 ) ) = ( ( 1 / 2 ) · - 1 )
76 75 oveq1i ⊢ ( ( - 1 · ( 1 / 2 ) ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) = ( ( ( 1 / 2 ) · - 1 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) )
77 27 13 31 3pm3.2i ⊢ ( - 1 ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ∧ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 )
78 1 3 nvsass ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( - 1 ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ∧ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 ) ) → ( ( - 1 · ( 1 / 2 ) ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) = ( - 1 𝑆 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) )
79 11 77 78 mp2an ⊢ ( ( - 1 · ( 1 / 2 ) ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) = ( - 1 𝑆 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) )
80 13 27 31 3pm3.2i ⊢ ( ( 1 / 2 ) ∈ ℂ ∧ - 1 ∈ ℂ ∧ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 )
81 1 3 nvsass ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( ( 1 / 2 ) ∈ ℂ ∧ - 1 ∈ ℂ ∧ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 ) ) → ( ( ( 1 / 2 ) · - 1 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) = ( ( 1 / 2 ) 𝑆 ( - 1 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) )
82 11 80 81 mp2an ⊢ ( ( ( 1 / 2 ) · - 1 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) = ( ( 1 / 2 ) 𝑆 ( - 1 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) )
83 27 6 29 3pm3.2i ⊢ ( - 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 )
84 1 2 3 nvdi ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( - 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 ) ) → ( - 1 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) = ( ( - 1 𝑆 𝐴 ) 𝐺 ( - 1 𝑆 ( - 1 𝑆 𝐵 ) ) ) )
85 11 83 84 mp2an ⊢ ( - 1 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) = ( ( - 1 𝑆 𝐴 ) 𝐺 ( - 1 𝑆 ( - 1 𝑆 𝐵 ) ) )
86 neg1mulneg1e1 ⊢ ( - 1 · - 1 ) = 1
87 86 oveq1i ⊢ ( ( - 1 · - 1 ) 𝑆 𝐵 ) = ( 1 𝑆 𝐵 )
88 27 27 7 3pm3.2i ⊢ ( - 1 ∈ ℂ ∧ - 1 ∈ ℂ ∧ 𝐵 ∈ 𝑋 )
89 1 3 nvsass ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( - 1 ∈ ℂ ∧ - 1 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( ( - 1 · - 1 ) 𝑆 𝐵 ) = ( - 1 𝑆 ( - 1 𝑆 𝐵 ) ) )
90 11 88 89 mp2an ⊢ ( ( - 1 · - 1 ) 𝑆 𝐵 ) = ( - 1 𝑆 ( - 1 𝑆 𝐵 ) )
91 1 3 nvsid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( 1 𝑆 𝐵 ) = 𝐵 )
92 11 7 91 mp2an ⊢ ( 1 𝑆 𝐵 ) = 𝐵
93 87 90 92 3eqtr3i ⊢ ( - 1 𝑆 ( - 1 𝑆 𝐵 ) ) = 𝐵
94 93 oveq2i ⊢ ( ( - 1 𝑆 𝐴 ) 𝐺 ( - 1 𝑆 ( - 1 𝑆 𝐵 ) ) ) = ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 )
95 85 94 eqtri ⊢ ( - 1 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) = ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 )
96 95 oveq2i ⊢ ( ( 1 / 2 ) 𝑆 ( - 1 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) = ( ( 1 / 2 ) 𝑆 ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 ) )
97 82 96 eqtri ⊢ ( ( ( 1 / 2 ) · - 1 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) = ( ( 1 / 2 ) 𝑆 ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 ) )
98 76 79 97 3eqtr3i ⊢ ( - 1 𝑆 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) = ( ( 1 / 2 ) 𝑆 ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 ) )
99 98 oveq2i ⊢ ( ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) 𝐺 ( - 1 𝑆 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) ) = ( ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) 𝐺 ( ( 1 / 2 ) 𝑆 ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 ) ) )
100 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 𝐴 ) ∈ 𝑋 )
101 11 27 6 100 mp3an ⊢ ( - 1 𝑆 𝐴 ) ∈ 𝑋
102 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( - 1 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 ) ∈ 𝑋 )
103 11 101 7 102 mp3an ⊢ ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 ) ∈ 𝑋
104 13 15 103 3pm3.2i ⊢ ( ( 1 / 2 ) ∈ ℂ ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 ) ∈ 𝑋 )
105 1 2 3 nvdi ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( ( 1 / 2 ) ∈ ℂ ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 ) ∈ 𝑋 ) ) → ( ( 1 / 2 ) 𝑆 ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 ) ) ) = ( ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) 𝐺 ( ( 1 / 2 ) 𝑆 ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 ) ) ) )
106 11 104 105 mp2an ⊢ ( ( 1 / 2 ) 𝑆 ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 ) ) ) = ( ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) 𝐺 ( ( 1 / 2 ) 𝑆 ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 ) ) )
107 99 106 eqtr4i ⊢ ( ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) 𝐺 ( - 1 𝑆 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) ) = ( ( 1 / 2 ) 𝑆 ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 ) ) )
108 101 7 pm3.2i ⊢ ( ( - 1 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 )
109 43 ablo4 ⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( ( - 1 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 ) ) = ( ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) 𝐺 ( 𝐵 𝐺 𝐵 ) ) )
110 40 41 108 109 mp3an ⊢ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 ) ) = ( ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) 𝐺 ( 𝐵 𝐺 𝐵 ) )
111 1 2 3 49 nvrinv ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) = ( 0vec ‘ 𝑈 ) )
112 11 6 111 mp2an ⊢ ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) = ( 0vec ‘ 𝑈 )
113 112 oveq1i ⊢ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) 𝐺 ( 𝐵 𝐺 𝐵 ) ) = ( ( 0vec ‘ 𝑈 ) 𝐺 ( 𝐵 𝐺 𝐵 ) )
114 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝐺 𝐵 ) ∈ 𝑋 )
115 11 7 7 114 mp3an ⊢ ( 𝐵 𝐺 𝐵 ) ∈ 𝑋
116 1 2 49 nv0lid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐵 𝐺 𝐵 ) ∈ 𝑋 ) → ( ( 0vec ‘ 𝑈 ) 𝐺 ( 𝐵 𝐺 𝐵 ) ) = ( 𝐵 𝐺 𝐵 ) )
117 11 115 116 mp2an ⊢ ( ( 0vec ‘ 𝑈 ) 𝐺 ( 𝐵 𝐺 𝐵 ) ) = ( 𝐵 𝐺 𝐵 )
118 113 117 eqtri ⊢ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) 𝐺 ( 𝐵 𝐺 𝐵 ) ) = ( 𝐵 𝐺 𝐵 )
119 38 46 43 vc2OLD ⊢ ( ( ( 1st ‘ 𝑈 ) ∈ CVecOLD ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝐺 𝐵 ) = ( 2 𝑆 𝐵 ) )
120 37 7 119 mp2an ⊢ ( 𝐵 𝐺 𝐵 ) = ( 2 𝑆 𝐵 )
121 110 118 120 3eqtri ⊢ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 ) ) = ( 2 𝑆 𝐵 )
122 121 oveq2i ⊢ ( ( 1 / 2 ) 𝑆 ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 ) ) ) = ( ( 1 / 2 ) 𝑆 ( 2 𝑆 𝐵 ) )
123 13 12 7 3pm3.2i ⊢ ( ( 1 / 2 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐵 ∈ 𝑋 )
124 1 3 nvsass ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( ( 1 / 2 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ( 1 / 2 ) · 2 ) 𝑆 𝐵 ) = ( ( 1 / 2 ) 𝑆 ( 2 𝑆 𝐵 ) ) )
125 11 123 124 mp2an ⊢ ( ( ( 1 / 2 ) · 2 ) 𝑆 𝐵 ) = ( ( 1 / 2 ) 𝑆 ( 2 𝑆 𝐵 ) )
126 68 oveq1i ⊢ ( ( ( 1 / 2 ) · 2 ) 𝑆 𝐵 ) = ( 1 𝑆 𝐵 )
127 122 125 126 3eqtr2i ⊢ ( ( 1 / 2 ) 𝑆 ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( - 1 𝑆 𝐴 ) 𝐺 𝐵 ) ) ) = ( 1 𝑆 𝐵 )
128 107 127 92 3eqtri ⊢ ( ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) 𝐺 ( - 1 𝑆 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) ) = 𝐵
129 128 oveq1i ⊢ ( ( ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) 𝐺 ( - 1 𝑆 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) ) 𝑃 𝐶 ) = ( 𝐵 𝑃 𝐶 )
130 74 129 oveq12i ⊢ ( ( ( ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) 𝐺 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) 𝑃 𝐶 ) + ( ( ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 𝐵 ) ) 𝐺 ( - 1 𝑆 ( ( 1 / 2 ) 𝑆 ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) ) 𝑃 𝐶 ) ) = ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) )
131 26 34 130 3eqtr2i ⊢ ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) )