# Metamath Proof Explorer

## Theorem ipdirilem

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

Ref Expression
Hypotheses ip1i.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
ip1i.2 ${⊢}{G}={+}_{v}\left({U}\right)$
ip1i.4 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
ip1i.7 ${⊢}{P}={\cdot }_{\mathrm{𝑖OLD}}\left({U}\right)$
ip1i.9 ${⊢}{U}\in {CPreHil}_{\mathrm{OLD}}$
ipdiri.8 ${⊢}{A}\in {X}$
ipdiri.9 ${⊢}{B}\in {X}$
ipdiri.10 ${⊢}{C}\in {X}$
Assertion ipdirilem ${⊢}\left({A}{G}{B}\right){P}{C}=\left({A}{P}{C}\right)+\left({B}{P}{C}\right)$

### Proof

Step Hyp Ref Expression
1 ip1i.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 ip1i.2 ${⊢}{G}={+}_{v}\left({U}\right)$
3 ip1i.4 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
4 ip1i.7 ${⊢}{P}={\cdot }_{\mathrm{𝑖OLD}}\left({U}\right)$
5 ip1i.9 ${⊢}{U}\in {CPreHil}_{\mathrm{OLD}}$
6 ipdiri.8 ${⊢}{A}\in {X}$
7 ipdiri.9 ${⊢}{B}\in {X}$
8 ipdiri.10 ${⊢}{C}\in {X}$
9 2cn ${⊢}2\in ℂ$
10 2ne0 ${⊢}2\ne 0$
11 9 10 recidi ${⊢}2\left(\frac{1}{2}\right)=1$
12 11 oveq1i ${⊢}2\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)=1{S}\left({A}{G}{B}\right)$
13 5 phnvi ${⊢}{U}\in \mathrm{NrmCVec}$
14 halfcn ${⊢}\frac{1}{2}\in ℂ$
15 1 2 nvgcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{G}{B}\in {X}$
16 13 6 7 15 mp3an ${⊢}{A}{G}{B}\in {X}$
17 9 14 16 3pm3.2i ${⊢}\left(2\in ℂ\wedge \frac{1}{2}\in ℂ\wedge {A}{G}{B}\in {X}\right)$
18 1 3 nvsass ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left(2\in ℂ\wedge \frac{1}{2}\in ℂ\wedge {A}{G}{B}\in {X}\right)\right)\to 2\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)=2{S}\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right)$
19 13 17 18 mp2an ${⊢}2\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)=2{S}\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right)$
20 1 3 nvsid ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}{G}{B}\in {X}\right)\to 1{S}\left({A}{G}{B}\right)={A}{G}{B}$
21 13 16 20 mp2an ${⊢}1{S}\left({A}{G}{B}\right)={A}{G}{B}$
22 12 19 21 3eqtr3i ${⊢}2{S}\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right)={A}{G}{B}$
23 22 oveq1i ${⊢}\left(2{S}\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right)\right){P}{C}=\left({A}{G}{B}\right){P}{C}$
24 1 3 nvscl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \frac{1}{2}\in ℂ\wedge {A}{G}{B}\in {X}\right)\to \left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\in {X}$
25 13 14 16 24 mp3an ${⊢}\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\in {X}$
26 1 2 3 4 5 25 8 ip2i ${⊢}\left(2{S}\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right)\right){P}{C}=2\left(\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right){P}{C}\right)$
27 23 26 eqtr3i ${⊢}\left({A}{G}{B}\right){P}{C}=2\left(\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right){P}{C}\right)$
28 neg1cn ${⊢}-1\in ℂ$
29 1 3 nvscl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge -1\in ℂ\wedge {B}\in {X}\right)\to -1{S}{B}\in {X}$
30 13 28 7 29 mp3an ${⊢}-1{S}{B}\in {X}$
31 1 2 nvgcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge -1{S}{B}\in {X}\right)\to {A}{G}\left(-1{S}{B}\right)\in {X}$
32 13 6 30 31 mp3an ${⊢}{A}{G}\left(-1{S}{B}\right)\in {X}$
33 1 3 nvscl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \frac{1}{2}\in ℂ\wedge {A}{G}\left(-1{S}{B}\right)\in {X}\right)\to \left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)\in {X}$
34 13 14 32 33 mp3an ${⊢}\left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)\in {X}$
35 1 2 3 4 5 25 34 8 ip1i ${⊢}\left(\left(\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right){G}\left(\left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)\right)\right){P}{C}\right)+\left(\left(\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right){G}\left(-1{S}\left(\left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)\right)\right)\right){P}{C}\right)=2\left(\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right){P}{C}\right)$
36 eqid ${⊢}{1}^{st}\left({U}\right)={1}^{st}\left({U}\right)$
37 36 nvvc ${⊢}{U}\in \mathrm{NrmCVec}\to {1}^{st}\left({U}\right)\in {CVec}_{\mathrm{OLD}}$
38 13 37 ax-mp ${⊢}{1}^{st}\left({U}\right)\in {CVec}_{\mathrm{OLD}}$
39 2 vafval ${⊢}{G}={1}^{st}\left({1}^{st}\left({U}\right)\right)$
40 39 vcablo ${⊢}{1}^{st}\left({U}\right)\in {CVec}_{\mathrm{OLD}}\to {G}\in \mathrm{AbelOp}$
41 38 40 ax-mp ${⊢}{G}\in \mathrm{AbelOp}$
42 6 7 pm3.2i ${⊢}\left({A}\in {X}\wedge {B}\in {X}\right)$
43 6 30 pm3.2i ${⊢}\left({A}\in {X}\wedge -1{S}{B}\in {X}\right)$
44 1 2 bafval ${⊢}{X}=\mathrm{ran}{G}$
45 44 ablo4 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({A}\in {X}\wedge -1{S}{B}\in {X}\right)\right)\to \left({A}{G}{B}\right){G}\left({A}{G}\left(-1{S}{B}\right)\right)=\left({A}{G}{A}\right){G}\left({B}{G}\left(-1{S}{B}\right)\right)$
46 41 42 43 45 mp3an ${⊢}\left({A}{G}{B}\right){G}\left({A}{G}\left(-1{S}{B}\right)\right)=\left({A}{G}{A}\right){G}\left({B}{G}\left(-1{S}{B}\right)\right)$
47 3 smfval ${⊢}{S}={2}^{nd}\left({1}^{st}\left({U}\right)\right)$
48 39 47 44 vc2OLD ${⊢}\left({1}^{st}\left({U}\right)\in {CVec}_{\mathrm{OLD}}\wedge {A}\in {X}\right)\to {A}{G}{A}=2{S}{A}$
49 38 6 48 mp2an ${⊢}{A}{G}{A}=2{S}{A}$
50 eqid ${⊢}{0}_{\mathrm{vec}}\left({U}\right)={0}_{\mathrm{vec}}\left({U}\right)$
51 1 2 3 50 nvrinv ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {B}\in {X}\right)\to {B}{G}\left(-1{S}{B}\right)={0}_{\mathrm{vec}}\left({U}\right)$
52 13 7 51 mp2an ${⊢}{B}{G}\left(-1{S}{B}\right)={0}_{\mathrm{vec}}\left({U}\right)$
53 49 52 oveq12i ${⊢}\left({A}{G}{A}\right){G}\left({B}{G}\left(-1{S}{B}\right)\right)=\left(2{S}{A}\right){G}{0}_{\mathrm{vec}}\left({U}\right)$
54 1 3 nvscl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge 2\in ℂ\wedge {A}\in {X}\right)\to 2{S}{A}\in {X}$
55 13 9 6 54 mp3an ${⊢}2{S}{A}\in {X}$
56 1 2 50 nv0rid ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge 2{S}{A}\in {X}\right)\to \left(2{S}{A}\right){G}{0}_{\mathrm{vec}}\left({U}\right)=2{S}{A}$
57 13 55 56 mp2an ${⊢}\left(2{S}{A}\right){G}{0}_{\mathrm{vec}}\left({U}\right)=2{S}{A}$
58 46 53 57 3eqtri ${⊢}\left({A}{G}{B}\right){G}\left({A}{G}\left(-1{S}{B}\right)\right)=2{S}{A}$
59 58 oveq2i ${⊢}\left(\frac{1}{2}\right){S}\left(\left({A}{G}{B}\right){G}\left({A}{G}\left(-1{S}{B}\right)\right)\right)=\left(\frac{1}{2}\right){S}\left(2{S}{A}\right)$
60 14 9 6 3pm3.2i ${⊢}\left(\frac{1}{2}\in ℂ\wedge 2\in ℂ\wedge {A}\in {X}\right)$
61 1 3 nvsass ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left(\frac{1}{2}\in ℂ\wedge 2\in ℂ\wedge {A}\in {X}\right)\right)\to \left(\frac{1}{2}\right)\cdot 2{S}{A}=\left(\frac{1}{2}\right){S}\left(2{S}{A}\right)$
62 13 60 61 mp2an ${⊢}\left(\frac{1}{2}\right)\cdot 2{S}{A}=\left(\frac{1}{2}\right){S}\left(2{S}{A}\right)$
63 59 62 eqtr4i ${⊢}\left(\frac{1}{2}\right){S}\left(\left({A}{G}{B}\right){G}\left({A}{G}\left(-1{S}{B}\right)\right)\right)=\left(\frac{1}{2}\right)\cdot 2{S}{A}$
64 14 16 32 3pm3.2i ${⊢}\left(\frac{1}{2}\in ℂ\wedge {A}{G}{B}\in {X}\wedge {A}{G}\left(-1{S}{B}\right)\in {X}\right)$
65 1 2 3 nvdi ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left(\frac{1}{2}\in ℂ\wedge {A}{G}{B}\in {X}\wedge {A}{G}\left(-1{S}{B}\right)\in {X}\right)\right)\to \left(\frac{1}{2}\right){S}\left(\left({A}{G}{B}\right){G}\left({A}{G}\left(-1{S}{B}\right)\right)\right)=\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right){G}\left(\left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)\right)$
66 13 64 65 mp2an ${⊢}\left(\frac{1}{2}\right){S}\left(\left({A}{G}{B}\right){G}\left({A}{G}\left(-1{S}{B}\right)\right)\right)=\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right){G}\left(\left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)\right)$
67 ax-1cn ${⊢}1\in ℂ$
68 67 9 10 divcan1i ${⊢}\left(\frac{1}{2}\right)\cdot 2=1$
69 68 oveq1i ${⊢}\left(\frac{1}{2}\right)\cdot 2{S}{A}=1{S}{A}$
70 1 3 nvsid ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\right)\to 1{S}{A}={A}$
71 13 6 70 mp2an ${⊢}1{S}{A}={A}$
72 69 71 eqtri ${⊢}\left(\frac{1}{2}\right)\cdot 2{S}{A}={A}$
73 63 66 72 3eqtr3i ${⊢}\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right){G}\left(\left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)\right)={A}$
74 73 oveq1i ${⊢}\left(\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right){G}\left(\left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)\right)\right){P}{C}={A}{P}{C}$
75 28 14 mulcomi ${⊢}-1\left(\frac{1}{2}\right)=\left(\frac{1}{2}\right)-1$
76 75 oveq1i ${⊢}-1\left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)=\left(\frac{1}{2}\right)-1{S}\left({A}{G}\left(-1{S}{B}\right)\right)$
77 28 14 32 3pm3.2i ${⊢}\left(-1\in ℂ\wedge \frac{1}{2}\in ℂ\wedge {A}{G}\left(-1{S}{B}\right)\in {X}\right)$
78 1 3 nvsass ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left(-1\in ℂ\wedge \frac{1}{2}\in ℂ\wedge {A}{G}\left(-1{S}{B}\right)\in {X}\right)\right)\to -1\left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)=-1{S}\left(\left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)\right)$
79 13 77 78 mp2an ${⊢}-1\left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)=-1{S}\left(\left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)\right)$
80 14 28 32 3pm3.2i ${⊢}\left(\frac{1}{2}\in ℂ\wedge -1\in ℂ\wedge {A}{G}\left(-1{S}{B}\right)\in {X}\right)$
81 1 3 nvsass ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left(\frac{1}{2}\in ℂ\wedge -1\in ℂ\wedge {A}{G}\left(-1{S}{B}\right)\in {X}\right)\right)\to \left(\frac{1}{2}\right)-1{S}\left({A}{G}\left(-1{S}{B}\right)\right)=\left(\frac{1}{2}\right){S}\left(-1{S}\left({A}{G}\left(-1{S}{B}\right)\right)\right)$
82 13 80 81 mp2an ${⊢}\left(\frac{1}{2}\right)-1{S}\left({A}{G}\left(-1{S}{B}\right)\right)=\left(\frac{1}{2}\right){S}\left(-1{S}\left({A}{G}\left(-1{S}{B}\right)\right)\right)$
83 28 6 30 3pm3.2i ${⊢}\left(-1\in ℂ\wedge {A}\in {X}\wedge -1{S}{B}\in {X}\right)$
84 1 2 3 nvdi ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left(-1\in ℂ\wedge {A}\in {X}\wedge -1{S}{B}\in {X}\right)\right)\to -1{S}\left({A}{G}\left(-1{S}{B}\right)\right)=\left(-1{S}{A}\right){G}\left(-1{S}\left(-1{S}{B}\right)\right)$
85 13 83 84 mp2an ${⊢}-1{S}\left({A}{G}\left(-1{S}{B}\right)\right)=\left(-1{S}{A}\right){G}\left(-1{S}\left(-1{S}{B}\right)\right)$
86 neg1mulneg1e1 ${⊢}-1-1=1$
87 86 oveq1i ${⊢}-1-1{S}{B}=1{S}{B}$
88 28 28 7 3pm3.2i ${⊢}\left(-1\in ℂ\wedge -1\in ℂ\wedge {B}\in {X}\right)$
89 1 3 nvsass ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left(-1\in ℂ\wedge -1\in ℂ\wedge {B}\in {X}\right)\right)\to -1-1{S}{B}=-1{S}\left(-1{S}{B}\right)$
90 13 88 89 mp2an ${⊢}-1-1{S}{B}=-1{S}\left(-1{S}{B}\right)$
91 1 3 nvsid ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {B}\in {X}\right)\to 1{S}{B}={B}$
92 13 7 91 mp2an ${⊢}1{S}{B}={B}$
93 87 90 92 3eqtr3i ${⊢}-1{S}\left(-1{S}{B}\right)={B}$
94 93 oveq2i ${⊢}\left(-1{S}{A}\right){G}\left(-1{S}\left(-1{S}{B}\right)\right)=\left(-1{S}{A}\right){G}{B}$
95 85 94 eqtri ${⊢}-1{S}\left({A}{G}\left(-1{S}{B}\right)\right)=\left(-1{S}{A}\right){G}{B}$
96 95 oveq2i ${⊢}\left(\frac{1}{2}\right){S}\left(-1{S}\left({A}{G}\left(-1{S}{B}\right)\right)\right)=\left(\frac{1}{2}\right){S}\left(\left(-1{S}{A}\right){G}{B}\right)$
97 82 96 eqtri ${⊢}\left(\frac{1}{2}\right)-1{S}\left({A}{G}\left(-1{S}{B}\right)\right)=\left(\frac{1}{2}\right){S}\left(\left(-1{S}{A}\right){G}{B}\right)$
98 76 79 97 3eqtr3i ${⊢}-1{S}\left(\left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)\right)=\left(\frac{1}{2}\right){S}\left(\left(-1{S}{A}\right){G}{B}\right)$
99 98 oveq2i ${⊢}\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right){G}\left(-1{S}\left(\left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)\right)\right)=\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right){G}\left(\left(\frac{1}{2}\right){S}\left(\left(-1{S}{A}\right){G}{B}\right)\right)$
100 1 3 nvscl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge -1\in ℂ\wedge {A}\in {X}\right)\to -1{S}{A}\in {X}$
101 13 28 6 100 mp3an ${⊢}-1{S}{A}\in {X}$
102 1 2 nvgcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge -1{S}{A}\in {X}\wedge {B}\in {X}\right)\to \left(-1{S}{A}\right){G}{B}\in {X}$
103 13 101 7 102 mp3an ${⊢}\left(-1{S}{A}\right){G}{B}\in {X}$
104 14 16 103 3pm3.2i ${⊢}\left(\frac{1}{2}\in ℂ\wedge {A}{G}{B}\in {X}\wedge \left(-1{S}{A}\right){G}{B}\in {X}\right)$
105 1 2 3 nvdi ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left(\frac{1}{2}\in ℂ\wedge {A}{G}{B}\in {X}\wedge \left(-1{S}{A}\right){G}{B}\in {X}\right)\right)\to \left(\frac{1}{2}\right){S}\left(\left({A}{G}{B}\right){G}\left(\left(-1{S}{A}\right){G}{B}\right)\right)=\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right){G}\left(\left(\frac{1}{2}\right){S}\left(\left(-1{S}{A}\right){G}{B}\right)\right)$
106 13 104 105 mp2an ${⊢}\left(\frac{1}{2}\right){S}\left(\left({A}{G}{B}\right){G}\left(\left(-1{S}{A}\right){G}{B}\right)\right)=\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right){G}\left(\left(\frac{1}{2}\right){S}\left(\left(-1{S}{A}\right){G}{B}\right)\right)$
107 99 106 eqtr4i ${⊢}\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right){G}\left(-1{S}\left(\left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)\right)\right)=\left(\frac{1}{2}\right){S}\left(\left({A}{G}{B}\right){G}\left(\left(-1{S}{A}\right){G}{B}\right)\right)$
108 101 7 pm3.2i ${⊢}\left(-1{S}{A}\in {X}\wedge {B}\in {X}\right)$
109 44 ablo4 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left(-1{S}{A}\in {X}\wedge {B}\in {X}\right)\right)\to \left({A}{G}{B}\right){G}\left(\left(-1{S}{A}\right){G}{B}\right)=\left({A}{G}\left(-1{S}{A}\right)\right){G}\left({B}{G}{B}\right)$
110 41 42 108 109 mp3an ${⊢}\left({A}{G}{B}\right){G}\left(\left(-1{S}{A}\right){G}{B}\right)=\left({A}{G}\left(-1{S}{A}\right)\right){G}\left({B}{G}{B}\right)$
111 1 2 3 50 nvrinv ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\right)\to {A}{G}\left(-1{S}{A}\right)={0}_{\mathrm{vec}}\left({U}\right)$
112 13 6 111 mp2an ${⊢}{A}{G}\left(-1{S}{A}\right)={0}_{\mathrm{vec}}\left({U}\right)$
113 112 oveq1i ${⊢}\left({A}{G}\left(-1{S}{A}\right)\right){G}\left({B}{G}{B}\right)={0}_{\mathrm{vec}}\left({U}\right){G}\left({B}{G}{B}\right)$
114 1 2 nvgcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {B}\in {X}\wedge {B}\in {X}\right)\to {B}{G}{B}\in {X}$
115 13 7 7 114 mp3an ${⊢}{B}{G}{B}\in {X}$
116 1 2 50 nv0lid ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {B}{G}{B}\in {X}\right)\to {0}_{\mathrm{vec}}\left({U}\right){G}\left({B}{G}{B}\right)={B}{G}{B}$
117 13 115 116 mp2an ${⊢}{0}_{\mathrm{vec}}\left({U}\right){G}\left({B}{G}{B}\right)={B}{G}{B}$
118 113 117 eqtri ${⊢}\left({A}{G}\left(-1{S}{A}\right)\right){G}\left({B}{G}{B}\right)={B}{G}{B}$
119 39 47 44 vc2OLD ${⊢}\left({1}^{st}\left({U}\right)\in {CVec}_{\mathrm{OLD}}\wedge {B}\in {X}\right)\to {B}{G}{B}=2{S}{B}$
120 38 7 119 mp2an ${⊢}{B}{G}{B}=2{S}{B}$
121 110 118 120 3eqtri ${⊢}\left({A}{G}{B}\right){G}\left(\left(-1{S}{A}\right){G}{B}\right)=2{S}{B}$
122 121 oveq2i ${⊢}\left(\frac{1}{2}\right){S}\left(\left({A}{G}{B}\right){G}\left(\left(-1{S}{A}\right){G}{B}\right)\right)=\left(\frac{1}{2}\right){S}\left(2{S}{B}\right)$
123 14 9 7 3pm3.2i ${⊢}\left(\frac{1}{2}\in ℂ\wedge 2\in ℂ\wedge {B}\in {X}\right)$
124 1 3 nvsass ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left(\frac{1}{2}\in ℂ\wedge 2\in ℂ\wedge {B}\in {X}\right)\right)\to \left(\frac{1}{2}\right)\cdot 2{S}{B}=\left(\frac{1}{2}\right){S}\left(2{S}{B}\right)$
125 13 123 124 mp2an ${⊢}\left(\frac{1}{2}\right)\cdot 2{S}{B}=\left(\frac{1}{2}\right){S}\left(2{S}{B}\right)$
126 68 oveq1i ${⊢}\left(\frac{1}{2}\right)\cdot 2{S}{B}=1{S}{B}$
127 122 125 126 3eqtr2i ${⊢}\left(\frac{1}{2}\right){S}\left(\left({A}{G}{B}\right){G}\left(\left(-1{S}{A}\right){G}{B}\right)\right)=1{S}{B}$
128 107 127 92 3eqtri ${⊢}\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right){G}\left(-1{S}\left(\left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)\right)\right)={B}$
129 128 oveq1i ${⊢}\left(\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right){G}\left(-1{S}\left(\left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)\right)\right)\right){P}{C}={B}{P}{C}$
130 74 129 oveq12i ${⊢}\left(\left(\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right){G}\left(\left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)\right)\right){P}{C}\right)+\left(\left(\left(\left(\frac{1}{2}\right){S}\left({A}{G}{B}\right)\right){G}\left(-1{S}\left(\left(\frac{1}{2}\right){S}\left({A}{G}\left(-1{S}{B}\right)\right)\right)\right)\right){P}{C}\right)=\left({A}{P}{C}\right)+\left({B}{P}{C}\right)$
131 27 35 130 3eqtr2i ${⊢}\left({A}{G}{B}\right){P}{C}=\left({A}{P}{C}\right)+\left({B}{P}{C}\right)$