environ
vocabularies HIDDEN, FUNCSDOM, VECTSP_1, VECTSP_2, SUBSET_1, RLVECT_2, RLSUB_1, RMOD_3, RLSUB_2, STRUCT_0, RELAT_1, FUNCT_1, SUPINF_2, ZFMISC_1, ALGSTR_0, REALSET1, GROUP_1, QC_LANG1, TARSKI, XBOOLE_0, RLVECT_3, CARD_3, PARTFUN1, ARYTM_3, ARYTM_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, BINOP_1, REALSET1, DOMAIN_1, STRUCT_0, ALGSTR_0, GROUP_1, VECTSP_1, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7;
definitions TARSKI, XBOOLE_0;
theorems FUNCT_2, MOD_3, TARSKI, VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_6, XBOOLE_1, RELAT_1;
schemes ;
registrations RELSET_1, STRUCT_0, VECTSP_1, VECTSP_4, VECTSP_7;
constructors HIDDEN, BINOP_1, REALSET2, VECTSP_5, VECTSP_6, VECTSP_7, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities XBOOLE_0, REALSET1, STRUCT_0;
expansions STRUCT_0;
theorem
for
K being
Ring for
r being
Scalar of
K for
M,
N being
LeftMod of
K for
m,
m1,
m2 being
Vector of
M for
n,
n1,
n2 being
Vector of
N st
M c= N holds
(
0. M = 0. N & (
m1 = n1 &
m2 = n2 implies
m1 + m2 = n1 + n2 ) & (
m = n implies
r * m = r * n ) & (
m = n implies
- n = - m ) & (
m1 = n1 &
m2 = n2 implies
m1 - m2 = n1 - n2 ) &
0. N in M &
0. M in N & (
n1 in M &
n2 in M implies
n1 + n2 in M ) & (
n in M implies
r * n in M ) & (
n in M implies
- n in M ) & (
n1 in M &
n2 in M implies
n1 - n2 in M ) )
by VECTSP_4:11, VECTSP_4:13, VECTSP_4:14, VECTSP_4:15, VECTSP_4:16, VECTSP_4:17, VECTSP_4:19, VECTSP_4:20, VECTSP_4:21, VECTSP_4:22, VECTSP_4:23;