let V be ComplexAlgebra; :: thesis: for V1 being ComplexSubAlgebra of V holds
( ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 + w1 = v + w ) & ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 * w1 = v * w ) & ( for v1 being Element of V1
for v being Element of V
for a being Complex st v1 = v holds
a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )
let V1 be ComplexSubAlgebra of V; :: thesis: ( ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 + w1 = v + w ) & ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 * w1 = v * w ) & ( for v1 being Element of V1
for v being Element of V
for a being Complex st v1 = v holds
a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )
hereby :: thesis: ( ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 * w1 = v * w ) & ( for v1 being Element of V1
for v being Element of V
for a being Complex st v1 = v holds
a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )
let x1, y1 be Element of V1; :: thesis: for x, y being Element of V st x1 = x & y1 = y holds
x1 + y1 = x + y
let x, y be Element of V; :: thesis: ( x1 = x & y1 = y implies x1 + y1 = x + y )
assume A1: ( x1 = x & y1 = y ) ; :: thesis: x1 + y1 = x + y
x1 + y1 = ( the addF of V || the carrier of V1) . [x1,y1] by Def1;
hence x1 + y1 = x + y by A1, FUNCT_1:49; :: thesis: verum
end;
hereby :: thesis: ( ( for v1 being Element of V1
for v being Element of V
for a being Complex st v1 = v holds
a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )
let x1, y1 be Element of V1; :: thesis: for x, y being Element of V st x1 = x & y1 = y holds
x1 * y1 = x * y
let x, y be Element of V; :: thesis: ( x1 = x & y1 = y implies x1 * y1 = x * y )
assume A2: ( x1 = x & y1 = y ) ; :: thesis: x1 * y1 = x * y
x1 * y1 = ( the multF of V || the carrier of V1) . [x1,y1] by Def1;
hence x1 * y1 = x * y by A2, FUNCT_1:49; :: thesis: verum
end;
hereby :: thesis: ( 1_ V1 = 1_ V & 0. V1 = 0. V )
let v1 be Element of V1; :: thesis: for v being Element of V
for a being Complex st v1 = v holds
a * v1 = a * v
let v be Element of V; :: thesis: for a being Complex st v1 = v holds
a * v1 = a * v
let a be Complex; :: thesis: ( v1 = v implies a * v1 = a * v )
assume A3: v1 = v ; :: thesis: a * v1 = a * v
reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def 2;
a1 * v1 = ( the Mult of V | [:COMPLEX, the carrier of V1:]) . [a1,v1] by Def1;
then a1 * v1 = a1 * v by A3, FUNCT_1:49;
hence a * v1 = a * v ; :: thesis: verum
end;
thus ( 1_ V1 = 1_ V & 0. V1 = 0. V ) by Def1; :: thesis: verum