let E be RealNormSpace; :: thesis: for a being Point of E holds
( (a -reflection) . a = a & ( for b being Point of E st (a -reflection) . b = b holds
a = b ) )
let a be Point of E; :: thesis: ( (a -reflection) . a = a & ( for b being Point of E st (a -reflection) . b = b holds
a = b ) )
set R = a -reflection ;
thus (a -reflection) . a = (2 * a) - a by Def4
.= (a + a) - a by Th3
.= a + (a - a) by RLVECT_1:28
.= a + (0. E) by RLVECT_1:15
.= a ; :: thesis: for b being Point of E st (a -reflection) . b = b holds
a = b
let b be Point of E; :: thesis: ( (a -reflection) . b = b implies a = b )
assume (a -reflection) . b = b ; :: thesis: a = b
then A1: ((a -reflection) . b) + b = 2 * b by Th3;
(a -reflection) . b = (2 * a) - b by Def4;
then ((a -reflection) . b) + b = (2 * a) - (b - b) by RLVECT_1:29
.= (2 * a) - (0. E) by RLVECT_1:15
.= 2 * a ;
hence a = b by A1, RLVECT_1:36; :: thesis: verum