let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
for u, v being VECTOR of V
for a being Real holds
( PProJ (w,y,(a * u),v) = a * (PProJ (w,y,u,v)) & PProJ (w,y,u,(a * v)) = a * (PProJ (w,y,u,v)) & PProJ (w,y,(a * u),v) = (PProJ (w,y,u,v)) * a & PProJ (w,y,u,(a * v)) = (PProJ (w,y,u,v)) * a )
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies for u, v being VECTOR of V
for a being Real holds
( PProJ (w,y,(a * u),v) = a * (PProJ (w,y,u,v)) & PProJ (w,y,u,(a * v)) = a * (PProJ (w,y,u,v)) & PProJ (w,y,(a * u),v) = (PProJ (w,y,u,v)) * a & PProJ (w,y,u,(a * v)) = (PProJ (w,y,u,v)) * a ) )
assume A1: Gen w,y ; :: thesis: for u, v being VECTOR of V
for a being Real holds
( PProJ (w,y,(a * u),v) = a * (PProJ (w,y,u,v)) & PProJ (w,y,u,(a * v)) = a * (PProJ (w,y,u,v)) & PProJ (w,y,(a * u),v) = (PProJ (w,y,u,v)) * a & PProJ (w,y,u,(a * v)) = (PProJ (w,y,u,v)) * a )
A2: now :: thesis: for u, v being VECTOR of V
for a being Real holds PProJ (w,y,(a * u),v) = a * (PProJ (w,y,u,v))
let u, v be VECTOR of V; :: thesis: for a being Real holds PProJ (w,y,(a * u),v) = a * (PProJ (w,y,u,v))
let a be Real; :: thesis: PProJ (w,y,(a * u),v) = a * (PProJ (w,y,u,v))
PProJ (w,y,(a * u),v) = ((a * (pr1 (w,y,u))) * (pr1 (w,y,v))) + ((pr2 (w,y,(a * u))) * (pr2 (w,y,v))) by A1, Lm17
.= ((a * (pr1 (w,y,u))) * (pr1 (w,y,v))) + ((a * (pr2 (w,y,u))) * (pr2 (w,y,v))) by A1, Lm17
.= a * (PProJ (w,y,u,v)) ;
hence PProJ (w,y,(a * u),v) = a * (PProJ (w,y,u,v)) ; :: thesis: verum
end;
let u, v be VECTOR of V; :: thesis: for a being Real holds
( PProJ (w,y,(a * u),v) = a * (PProJ (w,y,u,v)) & PProJ (w,y,u,(a * v)) = a * (PProJ (w,y,u,v)) & PProJ (w,y,(a * u),v) = (PProJ (w,y,u,v)) * a & PProJ (w,y,u,(a * v)) = (PProJ (w,y,u,v)) * a )
let a be Real; :: thesis: ( PProJ (w,y,(a * u),v) = a * (PProJ (w,y,u,v)) & PProJ (w,y,u,(a * v)) = a * (PProJ (w,y,u,v)) & PProJ (w,y,(a * u),v) = (PProJ (w,y,u,v)) * a & PProJ (w,y,u,(a * v)) = (PProJ (w,y,u,v)) * a )
thus PProJ (w,y,(a * u),v) = a * (PProJ (w,y,u,v)) by A2; :: thesis: ( PProJ (w,y,u,(a * v)) = a * (PProJ (w,y,u,v)) & PProJ (w,y,(a * u),v) = (PProJ (w,y,u,v)) * a & PProJ (w,y,u,(a * v)) = (PProJ (w,y,u,v)) * a )
thus PProJ (w,y,u,(a * v)) = PProJ (w,y,(a * v),u)
.= a * (PProJ (w,y,v,u)) by A2
.= a * (PProJ (w,y,u,v)) ; :: thesis: ( PProJ (w,y,(a * u),v) = (PProJ (w,y,u,v)) * a & PProJ (w,y,u,(a * v)) = (PProJ (w,y,u,v)) * a )
thus PProJ (w,y,(a * u),v) = (PProJ (w,y,u,v)) * a by A2; :: thesis: PProJ (w,y,u,(a * v)) = (PProJ (w,y,u,v)) * a
thus PProJ (w,y,u,(a * v)) = PProJ (w,y,(a * v),u)
.= a * (PProJ (w,y,v,u)) by A2
.= (PProJ (w,y,u,v)) * a ; :: thesis: verum