begin
Lm1:
for L being non empty multLoopStr st L is well-unital holds
1. L = 1_ L
:: deftheorem VECTSP_2:def 1 :
canceled;
:: deftheorem VECTSP_2:def 2 :
canceled;
:: deftheorem VECTSP_2:def 3 :
canceled;
:: deftheorem VECTSP_2:def 4 :
canceled;
:: deftheorem Def5 defines domRing-like VECTSP_2:def 5 :
for IT being non empty multLoopStr_0 holds
( IT is domRing-like iff for x, y being Element of IT holds
( not x * y = 0. IT or x = 0. IT or y = 0. IT ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
Lm2:
for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for x, y, z being Scalar of R st x + y = z holds
x = z - y
Lm3:
for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for x, z, y being Scalar of R st x = z - y holds
x + y = z
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th34:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem Th40:
theorem Th41:
theorem Th42:
:: deftheorem VECTSP_2:def 6 :
canceled;
:: deftheorem Def7 defines " VECTSP_2:def 7 :
for SF being non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed doubleLoopStr
for x being Element of SF st x <> 0. SF holds
for b3 being Element of the carrier of SF holds
( b3 = x " iff b3 * x = 1. SF );
:: deftheorem defines / VECTSP_2:def 8 :
for SF being Skew-Field
for x, y being Scalar of SF holds x / y = x * (y ");
theorem Th43:
theorem
canceled;
theorem Th45:
theorem Th46:
theorem
theorem Th48:
theorem Th49:
theorem Th50:
theorem
theorem
theorem Th53:
theorem Th54:
theorem
theorem
theorem
registration
let FS1,
FS2 be
1-sorted ;
let A be non
empty set ;
let a be
BinOp of
A;
let Z be
Element of
A;
let l be
Function of
[: the carrier of FS1,A:],
A;
let r be
Function of
[:A, the carrier of FS2:],
A;
cluster BiModStr(#
A,
a,
Z,
l,
r #)
-> non
empty ;
coherence
not BiModStr(# A,a,Z,l,r #) is empty
;
end;
:: deftheorem defines AbGr VECTSP_2:def 9 :
for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds AbGr R = addLoopStr(# the carrier of R, the addF of R,(0. R) #);
deffunc H1( Ring) -> VectSpStr of $1 = VectSpStr(# the carrier of $1, the addF of $1,(0. $1), the multF of $1 #);
Lm4:
for R being Ring holds
( H1(R) is Abelian & H1(R) is add-associative & H1(R) is right_zeroed & H1(R) is right_complementable )
:: deftheorem VECTSP_2:def 10 :
canceled;
:: deftheorem defines LeftModule VECTSP_2:def 11 :
for R being Ring holds LeftModule R = VectSpStr(# the carrier of R, the addF of R,(0. R), the multF of R #);
deffunc H2( Ring) -> RightModStr of $1 = RightModStr(# the carrier of $1, the addF of $1,(0. $1), the multF of $1 #);
Lm5:
for R being Ring holds
( H2(R) is Abelian & H2(R) is add-associative & H2(R) is right_zeroed & H2(R) is right_complementable )
:: deftheorem VECTSP_2:def 12 :
canceled;
:: deftheorem VECTSP_2:def 13 :
canceled;
:: deftheorem defines RightModule VECTSP_2:def 14 :
for R being Ring holds RightModule R = RightModStr(# the carrier of R, the addF of R,(0. R), the multF of R #);
:: deftheorem defines * VECTSP_2:def 15 :
for R being non empty 1-sorted
for V being non empty RightModStr of R
for x being Element of R
for v being Element of V holds v * x = the rmult of V . (v,x);
deffunc H3( Ring, Ring) -> BiModStr of $1,$2 = BiModStr(# 1,op2,op0,(pr2 ( the carrier of $1,1)),(pr1 (1, the carrier of $2)) #);
Lm6:
for R1, R2 being Ring holds
( H3(R1,R2) is Abelian & H3(R1,R2) is add-associative & H3(R1,R2) is right_zeroed & H3(R1,R2) is right_complementable )
definition
let R1,
R2 be
Ring;
canceled;canceled;canceled;canceled;canceled;func BiModule (
R1,
R2)
-> non
empty right_complementable Abelian add-associative right_zeroed strict BiModStr of
R1,
R2 equals
BiModStr(# 1,
op2,
op0,
(pr2 ( the carrier of R1,1)),
(pr1 (1, the carrier of R2)) #);
coherence
BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #) is non empty right_complementable Abelian add-associative right_zeroed strict BiModStr of R1,R2
by Lm6;
end;
:: deftheorem VECTSP_2:def 16 :
canceled;
:: deftheorem VECTSP_2:def 17 :
canceled;
:: deftheorem VECTSP_2:def 18 :
canceled;
:: deftheorem VECTSP_2:def 19 :
canceled;
:: deftheorem VECTSP_2:def 20 :
canceled;
:: deftheorem defines BiModule VECTSP_2:def 21 :
for R1, R2 being Ring holds BiModule (R1,R2) = BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #);
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th71:
Lm7:
for R being Ring holds
( LeftModule R is vector-distributive & LeftModule R is scalar-distributive & LeftModule R is scalar-associative & LeftModule R is scalar-unital )
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th77:
:: deftheorem VECTSP_2:def 22 :
canceled;
:: deftheorem Def23 defines RightMod-like VECTSP_2:def 23 :
for R being non empty doubleLoopStr
for IT being non empty RightModStr of R holds
( IT is RightMod-like iff for x, y being Scalar of R
for v, w being Vector of IT holds
( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v ) );
Lm8:
for R being Ring holds RightModule R is RightMod-like
Lm9:
for R1, R2 being Ring
for x, y being Scalar of R1
for p, q being Scalar of R2
for v, w being Vector of (BiModule (R1,R2)) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ R1) * v = v & (v + w) * p = (v * p) + (w * p) & v * (p + q) = (v * p) + (v * q) & v * (q * p) = (v * q) * p & v * (1_ R2) = v & x * (v * p) = (x * v) * p )
:: deftheorem Def24 defines BiMod-like VECTSP_2:def 24 :
for R1, R2 being Ring
for IT being non empty BiModStr of R1,R2 holds
( IT is BiMod-like iff for x being Scalar of R1
for p being Scalar of R2
for v being Vector of IT holds x * (v * p) = (x * v) * p );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
for
R1,
R2 being
Ring for
V being non
empty BiModStr of
R1,
R2 holds
( ( for
x,
y being
Scalar of
R1 for
p,
q being
Scalar of
R2 for
v,
w being
Vector of
V holds
(
x * (v + w) = (x * v) + (x * w) &
(x + y) * v = (x * v) + (y * v) &
(x * y) * v = x * (y * v) &
(1_ R1) * v = v &
(v + w) * p = (v * p) + (w * p) &
v * (p + q) = (v * p) + (v * q) &
v * (q * p) = (v * q) * p &
v * (1_ R2) = v &
x * (v * p) = (x * v) * p ) ) iff (
V is
RightMod-like &
V is
vector-distributive &
V is
scalar-distributive &
V is
scalar-associative &
V is
scalar-unital &
V is
BiMod-like ) )
by Def23, Def24, VECTSP_1:def 26, VECTSP_1:def 27, VECTSP_1:def 28, VECTSP_1:def 29;
theorem Th84:
registration
let R1,
R2 be
Ring;
cluster BiModule (
R1,
R2)
-> non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed strict RightMod-like BiMod-like ;
coherence
( BiModule (R1,R2) is Abelian & BiModule (R1,R2) is add-associative & BiModule (R1,R2) is right_zeroed & BiModule (R1,R2) is right_complementable & BiModule (R1,R2) is RightMod-like & BiModule (R1,R2) is vector-distributive & BiModule (R1,R2) is scalar-distributive & BiModule (R1,R2) is scalar-associative & BiModule (R1,R2) is scalar-unital & BiModule (R1,R2) is BiMod-like )
by Th84;
end;
theorem
begin
theorem
theorem
theorem
theorem
theorem Th90:
theorem Th91:
theorem Th92:
theorem
theorem
theorem