let F be Field; :: thesis: for S being SymSp of F
for a, b, x being Element of S
for l being Element of F st not a _|_ & l <> 0. F holds
ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))
let S be SymSp of F; :: thesis: for a, b, x being Element of S
for l being Element of F st not a _|_ & l <> 0. F holds
ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))
let a, b, x be Element of S; :: thesis: for l being Element of F st not a _|_ & l <> 0. F holds
ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))
let l be Element of F; :: thesis: ( not a _|_ & l <> 0. F implies ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x)) )
assume that
A1: not a _|_ and
A2: l <> 0. F ; :: thesis: ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))
set L = x - ((ProJ (a,(l * b),x)) * (l * b));
not a _|_ by A1, A2, Th5;
then A3: a _|_ by Th14;
A4: x - ((ProJ (a,(l * b),x)) * (l * b)) = x - (((ProJ (a,(l * b),x)) * l) * b) by VECTSP_1:def 16;
a _|_ by A1, Th14;
then (ProJ (a,b,x)) * (l ") = ((ProJ (a,(l * b),x)) * l) * (l ") by A1, A3, A4, Th12;
then (ProJ (a,b,x)) * (l ") = (ProJ (a,(l * b),x)) * (l * (l ")) by GROUP_1:def 3;
then (l ") * (ProJ (a,b,x)) = (ProJ (a,(l * b),x)) * (1_ F) by A2, VECTSP_1:def 10;
hence ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x)) ; :: thesis: verum