let AFV be WeakAffVect; for o being Element of AFV
for a being Element of (GroupVect (AFV,o))
for a9 being Element of AFV st a = a9 holds
- a = (Pcom o) . a9
let o be Element of AFV; for a being Element of (GroupVect (AFV,o))
for a9 being Element of AFV st a = a9 holds
- a = (Pcom o) . a9
let a be Element of (GroupVect (AFV,o)); for a9 being Element of AFV st a = a9 holds
- a = (Pcom o) . a9
let a9 be Element of AFV; ( a = a9 implies - a = (Pcom o) . a9 )
assume A1:
a = a9
; - a = (Pcom o) . a9
reconsider aa = (Pcom o) . a9 as Element of (GroupVect (AFV,o)) ;
( Pcom (o,o) = o & o,a9 // Pcom (o,a9), Pcom (o,o) )
by Th28, Th32;
then A2:
Padd (o,a9,(Pcom (o,a9))) = o
by Def5;
a + aa =
(Padd o) . (a,(Pcom (o,a9)))
by Def7
.=
0. (GroupVect (AFV,o))
by A1, A2, Def6
;
hence
- a = (Pcom o) . a9
by RLVECT_1:def 10; verum