This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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