let F be Field; for S being SymSp of F
for b, a, x being Element of S
for l being Element of F st not a _|_ & l <> 0. F holds
ProJ ((l * a),b,x) = ProJ (a,b,x)
let S be SymSp of F; for b, a, x being Element of S
for l being Element of F st not a _|_ & l <> 0. F holds
ProJ ((l * a),b,x) = ProJ (a,b,x)
let b, a, x be Element of S; for l being Element of F st not a _|_ & l <> 0. F holds
ProJ ((l * a),b,x) = ProJ (a,b,x)
let l be Element of F; ( not a _|_ & l <> 0. F implies ProJ ((l * a),b,x) = ProJ (a,b,x) )
assume that
A1:
not a _|_
and
A2:
l <> 0. F
; ProJ ((l * a),b,x) = ProJ (a,b,x)
not l * a _|_
by A1, A2, Th15;
then
l * a _|_
by Th27;
then
x - ((ProJ ((l * a),b,x)) * b) _|_
by Th12;
then
x - ((ProJ ((l * a),b,x)) * b) _|_
by Def1;
then
x - ((ProJ ((l * a),b,x)) * b) _|_
by VECTSP_1:def 16;
then
x - ((ProJ ((l * a),b,x)) * b) _|_
by A2, VECTSP_1:def 10;
then
x - ((ProJ ((l * a),b,x)) * b) _|_
by VECTSP_1:def 17;
then A3:
a _|_
by Th12;
a _|_
by A1, Th27;
hence
ProJ ((l * a),b,x) = ProJ (a,b,x)
by A1, A3, Th24; verum