set f = InnerProduct L;
for v being Vector of L holds (curry' (InnerProduct L)) . v is additive
proof
let v be Vector of L; :: thesis: (curry' (InnerProduct L)) . v is additive
set g = (curry' (InnerProduct L)) . v;
for w1, w2 being Vector of L holds ((curry' (InnerProduct L)) . v) . (w1 + w2) = (((curry' (InnerProduct L)) . v) . w1) + (((curry' (InnerProduct L)) . v) . w2)
proof
let w1, w2 be Vector of L; :: thesis: ((curry' (InnerProduct L)) . v) . (w1 + w2) = (((curry' (InnerProduct L)) . v) . w1) + (((curry' (InnerProduct L)) . v) . w2)
thus ((curry' (InnerProduct L)) . v) . (w1 + w2) = (InnerProduct L) . ((w1 + w2),v) by FUNCT_5:70
.= <;(w1 + w2),v;>
.= <;v,(w1 + w2);> by defZLattice
.= <;v,w1;> + <;v,w2;> by ThSc2
.= <;w1,v;> + <;v,w2;> by defZLattice
.= <;w1,v;> + <;w2,v;> by defZLattice
.= ((InnerProduct L) . (w1,v)) + ((InnerProduct L) . (w2,v))
.= (((curry' (InnerProduct L)) . v) . w1) + ((InnerProduct L) . (w2,v)) by FUNCT_5:70
.= (((curry' (InnerProduct L)) . v) . w1) + (((curry' (InnerProduct L)) . v) . w2) by FUNCT_5:70 ; :: thesis: verum
end;
hence (curry' (InnerProduct L)) . v is additive ; :: thesis: verum
end;
hence InnerProduct L is additiveSAF ; :: thesis: ( InnerProduct L is homogeneousSAF & InnerProduct L is additiveFAF & InnerProduct L is homogeneousFAF )
for v being Vector of L holds (curry' (InnerProduct L)) . v is homogeneous
proof
let v be Vector of L; :: thesis: (curry' (InnerProduct L)) . v is homogeneous
set g = (curry' (InnerProduct L)) . v;
for w being Vector of L
for i being Element of INT.Ring holds ((curry' (InnerProduct L)) . v) . (i * w) = i * (((curry' (InnerProduct L)) . v) . w)
proof
let w be Vector of L; :: thesis: for i being Element of INT.Ring holds ((curry' (InnerProduct L)) . v) . (i * w) = i * (((curry' (InnerProduct L)) . v) . w)
let i be Element of INT.Ring; :: thesis: ((curry' (InnerProduct L)) . v) . (i * w) = i * (((curry' (InnerProduct L)) . v) . w)
thus ((curry' (InnerProduct L)) . v) . (i * w) = (InnerProduct L) . ((i * w),v) by FUNCT_5:70
.= <;(i * w),v;>
.= <;v,(i * w);> by defZLattice
.= i * <;v,w;> by ThSc3
.= i * <;w,v;> by defZLattice
.= i * ((InnerProduct L) . (w,v))
.= i * (((curry' (InnerProduct L)) . v) . w) by FUNCT_5:70 ; :: thesis: verum
end;
hence (curry' (InnerProduct L)) . v is homogeneous ; :: thesis: verum
end;
hence InnerProduct L is homogeneousSAF ; :: thesis: ( InnerProduct L is additiveFAF & InnerProduct L is homogeneousFAF )
for v being Vector of L holds (curry (InnerProduct L)) . v is additive
proof
let v be Vector of L; :: thesis: (curry (InnerProduct L)) . v is additive
set g = (curry (InnerProduct L)) . v;
for w1, w2 being Vector of L holds ((curry (InnerProduct L)) . v) . (w1 + w2) = (((curry (InnerProduct L)) . v) . w1) + (((curry (InnerProduct L)) . v) . w2)
proof
let w1, w2 be Vector of L; :: thesis: ((curry (InnerProduct L)) . v) . (w1 + w2) = (((curry (InnerProduct L)) . v) . w1) + (((curry (InnerProduct L)) . v) . w2)
thus ((curry (InnerProduct L)) . v) . (w1 + w2) = (InnerProduct L) . (v,(w1 + w2)) by FUNCT_5:69
.= <;v,(w1 + w2);>
.= <;v,w1;> + <;v,w2;> by ThSc2
.= ((InnerProduct L) . (v,w1)) + ((InnerProduct L) . (v,w2))
.= (((curry (InnerProduct L)) . v) . w1) + ((InnerProduct L) . (v,w2)) by FUNCT_5:69
.= (((curry (InnerProduct L)) . v) . w1) + (((curry (InnerProduct L)) . v) . w2) by FUNCT_5:69 ; :: thesis: verum
end;
hence (curry (InnerProduct L)) . v is additive ; :: thesis: verum
end;
hence InnerProduct L is additiveFAF ; :: thesis: InnerProduct L is homogeneousFAF
for v being Vector of L holds (curry (InnerProduct L)) . v is homogeneous
proof
let v be Vector of L; :: thesis: (curry (InnerProduct L)) . v is homogeneous
set g = (curry (InnerProduct L)) . v;
for w being Vector of L
for i being Element of INT.Ring holds ((curry (InnerProduct L)) . v) . (i * w) = i * (((curry (InnerProduct L)) . v) . w)
proof
let w be Vector of L; :: thesis: for i being Element of INT.Ring holds ((curry (InnerProduct L)) . v) . (i * w) = i * (((curry (InnerProduct L)) . v) . w)
let i be Element of INT.Ring; :: thesis: ((curry (InnerProduct L)) . v) . (i * w) = i * (((curry (InnerProduct L)) . v) . w)
thus ((curry (InnerProduct L)) . v) . (i * w) = (InnerProduct L) . (v,(i * w)) by FUNCT_5:69
.= <;v,(i * w);>
.= i * <;v,w;> by ThSc3
.= i * ((InnerProduct L) . (v,w))
.= i * (((curry (InnerProduct L)) . v) . w) by FUNCT_5:69 ; :: thesis: verum
end;
hence (curry (InnerProduct L)) . v is homogeneous ; :: thesis: verum
end;
hence InnerProduct L is homogeneousFAF ; :: thesis: verum