environ
vocabularies HIDDEN, NUMBERS, REAL_1, SUBSET_1, PRE_TOPC, EUCLID, FINSEQ_1, STRUCT_0, FINSEQ_2, MCART_1, FUNCT_1, SUPINF_2, CARD_1, ARYTM_3, RELAT_1, ARYTM_1, RVSUM_1, BINOP_2, CARD_3, EUCLID_5;
notations HIDDEN, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, FUNCT_1, BINOP_1, BINOP_2, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSEQOP, PRE_TOPC, RVSUM_1, RLVECT_1, EUCLID, STRUCT_0, REAL_1;
definitions ;
theorems EUCLID, RVSUM_1, FINSEQ_2, FINSEQ_1, BINOP_2, XREAL_0, VALUED_1, CARD_1, RLVECT_1;
schemes ;
registrations RELSET_1, NUMBERS, XREAL_0, MEMBERED, MONOID_0, EUCLID, VALUED_0, FINSEQ_2, RVSUM_1, FINSEQ_1;
constructors HIDDEN, REAL_1, BINOP_2, FINSEQOP, FINSEQ_4, MONOID_0, EUCLID, BINOP_1;
requirements HIDDEN, REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
equalities ALGSTR_0;
expansions ;
theorem Th6:
for
x1,
x2,
y1,
y2,
z1,
z2 being
Real holds
|[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]|
theorem Th13:
for
x1,
x2,
y1,
y2,
z1,
z2 being
Real holds
|[x1,y1,z1]| - |[x2,y2,z2]| = |[(x1 - x2),(y1 - y2),(z1 - z2)]|
theorem Th15:
for
x1,
x2,
y1,
y2,
z1,
z2 being
Real holds
|[x1,y1,z1]| <X> |[x2,y2,z2]| = |[((y1 * z2) - (z1 * y2)),((z1 * x2) - (x1 * z2)),((x1 * y2) - (y1 * x2))]|
theorem Th30:
for
x3,
y3,
x1,
x2,
y1,
y2 being
Real holds
|(|[x1,x2,x3]|,|[y1,y2,y3]|)| = ((x1 * y1) + (x2 * y2)) + (x3 * y3)
:: Inner Product for Point of TOP-REAL 3
::