environ
vocabularies HIDDEN, NUMBERS, RLVECT_1, STRUCT_0, SUBSET_1, ALGSTR_0, BINOP_1, FUNCT_1, ZFMISC_1, XBOOLE_0, REAL_1, PRE_TOPC, SUPINF_2, PROB_2, RLSUB_1, FUNCOP_1, CARD_1, ARYTM_3, RELAT_1, XXREAL_0, ARYTM_1, COMPLEX1, SQUARE_1, FUNCT_3, RVSUM_1, NORMSP_1, METRIC_1, NAT_1, BHSP_1, PARTFUN1, FUNCT_7;
notations HIDDEN, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1, NAT_1, STRUCT_0, ALGSTR_0, DOMAIN_1, PRE_TOPC, RLVECT_1, RLSUB_1, SQUARE_1, VFUNCT_1, NORMSP_1, QUIN_1, XXREAL_0;
definitions STRUCT_0, ALGSTR_0, RLVECT_1, VALUED_0, FUNCT_2;
theorems TARSKI, SQUARE_1, ABSVALUE, RLVECT_1, RLSUB_1, QUIN_1, FUNCT_2, NORMSP_1, COMPLEX1, FUNCOP_1, XREAL_1, XXREAL_0, ALGSTR_0, ORDINAL1, VFUNCT_1, PARTFUN1;
schemes FUNCT_2;
registrations SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, STRUCT_0, XBOOLE_0, ALGSTR_0, FUNCT_2, VFUNCT_1, QUIN_1;
constructors HIDDEN, BINOP_1, DOMAIN_1, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, MEMBERED, COMPLEX1, QUIN_1, RLSUB_1, NORMSP_1, RELSET_1, VFUNCT_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities STRUCT_0, SQUARE_1, ALGSTR_0, RLVECT_1;
expansions VALUED_0;
deffunc H1( UNITSTR ) -> Element of the carrier of $1 = 0. $1;
set V0 = the RealLinearSpace;
Lm1:
the carrier of ((0). the RealLinearSpace) = {(0. the RealLinearSpace)}
by RLSUB_1:def 3;
reconsider nilfunc = [: the carrier of ((0). the RealLinearSpace), the carrier of ((0). the RealLinearSpace):] --> (In (0,REAL)) as Function of [: the carrier of ((0). the RealLinearSpace), the carrier of ((0). the RealLinearSpace):],REAL ;
( ( for x, y being VECTOR of ((0). the RealLinearSpace) holds nilfunc . [x,y] = 0 ) & 0. the RealLinearSpace in the carrier of ((0). the RealLinearSpace) )
by Lm1, FUNCOP_1:7, TARSKI:def 1;
then Lm2:
nilfunc . [(0. the RealLinearSpace),(0. the RealLinearSpace)] = 0
;
Lm3:
for u, v being VECTOR of ((0). the RealLinearSpace) holds nilfunc . [u,v] = nilfunc . [v,u]
Lm4:
for u, v, w being VECTOR of ((0). the RealLinearSpace) holds nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w])
Lm5:
for u, v being VECTOR of ((0). the RealLinearSpace)
for a being Real holds nilfunc . [(a * u),v] = a * (nilfunc . [u,v])
set X0 = UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #);
Lm6:
now for x, y, z being Point of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)
for a being Real holds
( ( x .|. x = In (0,REAL) implies x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) ) & ( x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) implies x .|. x = In (0,REAL) ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
let x,
y,
z be
Point of
UNITSTR(# the
carrier of
((0). the RealLinearSpace),
(0. ((0). the RealLinearSpace)), the
addF of
((0). the RealLinearSpace), the
Mult of
((0). the RealLinearSpace),
nilfunc #);
for a being Real holds
( ( x .|. x = In (0,REAL) implies x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) ) & ( x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) implies x .|. x = In (0,REAL) ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )let a be
Real;
( ( x .|. x = In (0,REAL) implies x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) ) & ( x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) implies x .|. x = In (0,REAL) ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
H1(
UNITSTR(# the
carrier of
((0). the RealLinearSpace),
(0. ((0). the RealLinearSpace)), the
addF of
((0). the RealLinearSpace), the
Mult of
((0). the RealLinearSpace),
nilfunc #))
= 0. the
RealLinearSpace
by RLSUB_1:11;
hence
(
x .|. x = In (
0,
REAL) iff
x = H1(
UNITSTR(# the
carrier of
((0). the RealLinearSpace),
(0. ((0). the RealLinearSpace)), the
addF of
((0). the RealLinearSpace), the
Mult of
((0). the RealLinearSpace),
nilfunc #)) )
by Lm1, FUNCOP_1:7, TARSKI:def 1;
( 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
0 <= x .|. x
by FUNCOP_1:7;
( x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
x .|. y = y .|. x
by Lm3;
( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
(x + y) .|. z = (x .|. z) + (y .|. z)
(a * x) .|. y = a * (x .|. y)
thus
(a * x) .|. y = a * (x .|. y)
verum
end;