:: VECTSP_2 semantic presentation

definition
let c1 be non empty multLoopStr ;
canceled;
attr a1 is well-unital means :Def2: :: VECTSP_2:def 2
for b1 being Element of a1 holds
( b1 * (1_ a1) = b1 & (1_ a1) * b1 = b1 );
end;

:: deftheorem Def1 VECTSP_2:def 1 :
canceled;

:: deftheorem Def2 defines well-unital VECTSP_2:def 2 :
for b1 being non empty multLoopStr holds
( b1 is well-unital iff for b2 being Element of b1 holds
( b2 * (1_ b1) = b2 & (1_ b1) * b2 = b2 ) );

Lemma2: for b1 being non empty multLoopStr st b1 is well-unital holds
b1 is unital
proof end;

registration
cluster non empty well-unital -> non empty unital multLoopStr ;
coherence
for b1 being non empty multLoopStr st b1 is well-unital holds
b1 is unital by Lemma2;
end;

Lemma3: for b1 being non empty multLoopStr st b1 is well-unital holds
1_ b1 = 1. b1
proof end;

registration
cluster non empty Abelian add-associative right_zeroed right_complementable unital strict distributive doubleLoopStr ;
existence
ex b1 being non empty doubleLoopStr st
( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is unital & b1 is distributive )
proof end;
end;

theorem Th1: :: VECTSP_2:1
for b1 being non empty doubleLoopStr holds
( ( for b2, b3, b4 being Scalar of b1 holds
( b2 + b3 = b3 + b2 & (b2 + b3) + b4 = b2 + (b3 + b4) & b2 + (0. b1) = b2 & b2 + (- b2) = 0. b1 & b2 * (1. b1) = b2 & (1. b1) * b2 = b2 & (b2 * b3) * b4 = b2 * (b3 * b4) & b2 * (b3 + b4) = (b2 * b3) + (b2 * b4) & (b3 + b4) * b2 = (b3 * b2) + (b4 * b2) ) ) iff b1 is Ring )
proof end;

registration
cluster strict doubleLoopStr ;
existence
ex b1 being Ring st b1 is strict
proof end;
end;

registration
cluster commutative doubleLoopStr ;
existence
ex b1 being Ring st b1 is commutative
proof end;
end;

definition
mode comRing is commutative Ring;
end;

registration
cluster strict doubleLoopStr ;
existence
ex b1 being comRing st b1 is strict
proof end;
end;

definition
let c1 be non empty multLoopStr_0 ;
canceled;
canceled;
attr a1 is domRing-like means :Def5: :: VECTSP_2:def 5
for b1, b2 being Element of a1 holds
( not b1 * b2 = 0. a1 or b1 = 0. a1 or b2 = 0. a1 );
end;

:: deftheorem Def3 VECTSP_2:def 3 :
canceled;

:: deftheorem Def4 VECTSP_2:def 4 :
canceled;

:: deftheorem Def5 defines domRing-like VECTSP_2:def 5 :
for b1 being non empty multLoopStr_0 holds
( b1 is domRing-like iff for b2, b3 being Element of b1 holds
( not b2 * b3 = 0. b1 or b2 = 0. b1 or b3 = 0. b1 ) );

registration
cluster strict non degenerated domRing-like doubleLoopStr ;
existence
ex b1 being comRing st
( b1 is strict & not b1 is degenerated & b1 is domRing-like )
proof end;
end;

definition
mode domRing is non degenerated domRing-like comRing;
end;

theorem Th2: :: VECTSP_2:2
canceled;

theorem Th3: :: VECTSP_2:3
canceled;

theorem Th4: :: VECTSP_2:4
canceled;

theorem Th5: :: VECTSP_2:5
canceled;

theorem Th6: :: VECTSP_2:6
canceled;

theorem Th7: :: VECTSP_2:7
canceled;

theorem Th8: :: VECTSP_2:8
canceled;

theorem Th9: :: VECTSP_2:9
canceled;

theorem Th10: :: VECTSP_2:10
canceled;

theorem Th11: :: VECTSP_2:11
canceled;

theorem Th12: :: VECTSP_2:12
canceled;

theorem Th13: :: VECTSP_2:13
for b1 being Field holds b1 is domRing
proof end;

registration
cluster Field-like non degenerated doubleLoopStr ;
existence
ex b1 being Ring st
( not b1 is degenerated & b1 is Field-like )
proof end;
end;

definition
mode Skew-Field is Field-like non degenerated Ring;
end;

registration
cluster strict doubleLoopStr ;
existence
ex b1 being Skew-Field st b1 is strict
proof end;
end;

theorem Th14: :: VECTSP_2:14
canceled;

theorem Th15: :: VECTSP_2:15
canceled;

theorem Th16: :: VECTSP_2:16
for b1 being Ring st ( for b2 being Scalar of b1 holds
( ( b2 <> 0. b1 implies ex b3 being Scalar of b1 st b2 * b3 = 1. b1 ) & 0. b1 <> 1. b1 ) ) holds
b1 is Skew-Field by VECTSP_1:def 20, VECTSP_1:def 21;

registration
cluster non empty commutative left_unital -> non empty unital multLoopStr ;
coherence
for b1 being non empty multLoopStr st b1 is commutative & b1 is left_unital holds
b1 is unital
proof end;
cluster non empty commutative right_unital -> non empty unital multLoopStr ;
coherence
for b1 being non empty multLoopStr st b1 is commutative & b1 is right_unital holds
b1 is unital
proof end;
end;

Lemma5: for b1 being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b2, b3, b4 being Scalar of b1 st b2 + b3 = b4 holds
b2 = b4 - b3
proof end;

Lemma6: for b1 being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b2, b3, b4 being Scalar of b1 st b2 = b3 - b4 holds
b2 + b4 = b3
proof end;

theorem Th17: :: VECTSP_2:17
canceled;

theorem Th18: :: VECTSP_2:18
canceled;

theorem Th19: :: VECTSP_2:19
canceled;

theorem Th20: :: VECTSP_2:20
canceled;

theorem Th21: :: VECTSP_2:21
canceled;

theorem Th22: :: VECTSP_2:22
for b1 being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b2, b3, b4 being Scalar of b1 holds
( ( b2 + b3 = b4 implies b2 = b4 - b3 ) & ( b2 = b4 - b3 implies b2 + b3 = b4 ) & ( b2 + b3 = b4 implies b3 = b4 - b2 ) & ( b3 = b4 - b2 implies b2 + b3 = b4 ) ) by Lemma5, Lemma6;

theorem Th23: :: VECTSP_2:23
canceled;

theorem Th24: :: VECTSP_2:24
canceled;

theorem Th25: :: VECTSP_2:25
canceled;

theorem Th26: :: VECTSP_2:26
canceled;

theorem Th27: :: VECTSP_2:27
canceled;

theorem Th28: :: VECTSP_2:28
canceled;

theorem Th29: :: VECTSP_2:29
canceled;

theorem Th30: :: VECTSP_2:30
canceled;

theorem Th31: :: VECTSP_2:31
canceled;

theorem Th32: :: VECTSP_2:32
canceled;

theorem Th33: :: VECTSP_2:33
canceled;

theorem Th34: :: VECTSP_2:34
for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2 being Element of b1 holds
( b2 = 0. b1 iff - b2 = 0. b1 )
proof end;

theorem Th35: :: VECTSP_2:35
canceled;

theorem Th36: :: VECTSP_2:36
canceled;

theorem Th37: :: VECTSP_2:37
canceled;

theorem Th38: :: VECTSP_2:38
for b1 being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b2, b3 being Element of b1 ex b4 being Element of b1 st
( b2 = b3 + b4 & b2 = b4 + b3 )
proof end;

theorem Th39: :: VECTSP_2:39
for b1 being non empty add-associative right_zeroed right_complementable distributive non degenerated doubleLoopStr
for b2, b3 being Element of b1 st b2 * b3 = 1. b1 holds
( b2 <> 0. b1 & b3 <> 0. b1 )
proof end;

theorem Th40: :: VECTSP_2:40
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative right_unital distributive left_unital Field-like non degenerated doubleLoopStr
for b2 being Element of b1 st b2 <> 0. b1 holds
ex b3 being Element of b1 st b3 * b2 = 1. b1
proof end;

theorem Th41: :: VECTSP_2:41
for b1 being Skew-Field
for b2, b3 being Scalar of b1 st b2 * b3 = 1. b1 holds
b3 * b2 = 1. b1
proof end;

theorem Th42: :: VECTSP_2:42
for b1 being non empty Abelian add-associative right_zeroed right_complementable unital associative distributive Field-like non degenerated doubleLoopStr
for b2, b3, b4 being Element of b1 st b2 * b3 = b2 * b4 & b2 <> 0. b1 holds
b3 = b4
proof end;

definition
let c1 be non empty Abelian add-associative right_zeroed right_complementable unital associative distributive Field-like non degenerated doubleLoopStr ;
let c2 be Element of c1;
assume E12: c2 <> 0. c1 ;
canceled;
func c2 " -> Scalar of a1 means :Def7: :: VECTSP_2:def 7
a2 * a3 = 1. a1;
existence
ex b1 being Scalar of c1 st c2 * b1 = 1. c1 by E12, VECTSP_1:def 20;
uniqueness
for b1, b2 being Scalar of c1 st c2 * b1 = 1. c1 & c2 * b2 = 1. c1 holds
b1 = b2 by E12, Th42;
end;

:: deftheorem Def6 VECTSP_2:def 6 :
canceled;

:: deftheorem Def7 defines " VECTSP_2:def 7 :
for b1 being non empty Abelian add-associative right_zeroed right_complementable unital associative distributive Field-like non degenerated doubleLoopStr
for b2 being Element of b1 st b2 <> 0. b1 holds
for b3 being Scalar of b1 holds
( b3 = b2 " iff b2 * b3 = 1. b1 );

definition
let c1 be Skew-Field;
let c2, c3 be Scalar of c1;
func c2 / c3 -> Scalar of a1 equals :: VECTSP_2:def 8
a2 * (a3 " );
correctness
coherence
c2 * (c3 " ) is Scalar of c1;
;
end;

:: deftheorem Def8 defines / VECTSP_2:def 8 :
for b1 being Skew-Field
for b2, b3 being Scalar of b1 holds b2 / b3 = b2 * (b3 " );

theorem Th43: :: VECTSP_2:43
for b1 being Skew-Field
for b2 being Scalar of b1 st b2 <> 0. b1 holds
( b2 * (b2 " ) = 1. b1 & (b2 " ) * b2 = 1. b1 )
proof end;

theorem Th44: :: VECTSP_2:44
canceled;

theorem Th45: :: VECTSP_2:45
for b1 being Skew-Field
for b2, b3 being Scalar of b1 st b2 * b3 = 1. b1 holds
( b2 = b3 " & b3 = b2 " )
proof end;

theorem Th46: :: VECTSP_2:46
for b1 being Skew-Field
for b2, b3 being Scalar of b1 st b2 <> 0. b1 & b3 <> 0. b1 holds
(b2 " ) * (b3 " ) = (b3 * b2) "
proof end;

theorem Th47: :: VECTSP_2:47
for b1 being Skew-Field
for b2, b3 being Scalar of b1 holds
( not b2 * b3 = 0. b1 or b2 = 0. b1 or b3 = 0. b1 )
proof end;

theorem Th48: :: VECTSP_2:48
for b1 being Skew-Field
for b2 being Scalar of b1 st b2 <> 0. b1 holds
b2 " <> 0. b1
proof end;

theorem Th49: :: VECTSP_2:49
for b1 being Skew-Field
for b2 being Scalar of b1 st b2 <> 0. b1 holds
(b2 " ) " = b2
proof end;

theorem Th50: :: VECTSP_2:50
for b1 being Skew-Field
for b2 being Scalar of b1 st b2 <> 0. b1 holds
( (1. b1) / b2 = b2 " & (1. b1) / (b2 " ) = b2 )
proof end;

theorem Th51: :: VECTSP_2:51
for b1 being Skew-Field
for b2 being Scalar of b1 st b2 <> 0. b1 holds
( b2 * ((1. b1) / b2) = 1. b1 & ((1. b1) / b2) * b2 = 1. b1 )
proof end;

theorem Th52: :: VECTSP_2:52
for b1 being Skew-Field
for b2 being Scalar of b1 st b2 <> 0. b1 holds
b2 / b2 = 1. b1 by Th43;

theorem Th53: :: VECTSP_2:53
for b1 being Skew-Field
for b2, b3, b4 being Scalar of b1 st b2 <> 0. b1 & b3 <> 0. b1 holds
b4 / b2 = (b4 * b3) / (b2 * b3)
proof end;

theorem Th54: :: VECTSP_2:54
for b1 being Skew-Field
for b2, b3 being Scalar of b1 st b2 <> 0. b1 holds
( - (b3 / b2) = (- b3) / b2 & b3 / (- b2) = - (b3 / b2) )
proof end;

theorem Th55: :: VECTSP_2:55
for b1 being Skew-Field
for b2, b3, b4 being Scalar of b1 st b2 <> 0. b1 holds
( (b3 / b2) + (b4 / b2) = (b3 + b4) / b2 & (b3 / b2) - (b4 / b2) = (b3 - b4) / b2 )
proof end;

theorem Th56: :: VECTSP_2:56
for b1 being Skew-Field
for b2, b3, b4 being Scalar of b1 st b2 <> 0. b1 & b3 <> 0. b1 holds
b4 / (b2 / b3) = (b4 * b3) / b2
proof end;

theorem Th57: :: VECTSP_2:57
for b1 being Skew-Field
for b2, b3 being Scalar of b1 st b2 <> 0. b1 holds
(b3 / b2) * b2 = b3
proof end;

definition
let c1 be 1-sorted ;
attr a2 is strict;
struct RightModStr of c1 -> LoopStr ;
aggr RightModStr(# carrier, add, Zero, rmult #) -> RightModStr of a1;
sel rmult c2 -> Function of [:the carrier of a2,the carrier of a1:],the carrier of a2;
end;

registration
let c1 be 1-sorted ;
cluster non empty RightModStr of a1;
existence
not for b1 being RightModStr of c1 holds b1 is empty
proof end;
end;

registration
let c1 be 1-sorted ;
let c2 be non empty set ;
let c3 be BinOp of c2;
let c4 be Element of c2;
let c5 be Function of [:c2,the carrier of c1:],c2;
cluster RightModStr(# a2,a3,a4,a5 #) -> non empty ;
coherence
not RightModStr(# c2,c3,c4,c5 #) is empty by STRUCT_0:def 1;
end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be non empty RightModStr of c1;
mode Scalar of a2 is Element of a1;
mode Vector of a2 is Element of a2;
end;

definition
let c1, c2 be 1-sorted ;
attr a3 is strict;
struct BiModStr of c1,c2 -> VectSpStr of a1, RightModStr of a2;
aggr BiModStr(# carrier, add, Zero, lmult, rmult #) -> BiModStr of a1,a2;
end;

registration
let c1, c2 be 1-sorted ;
cluster non empty BiModStr of a1,a2;
existence
not for b1 being BiModStr of c1,c2 holds b1 is empty
proof end;
end;

registration
let c1, c2 be 1-sorted ;
let c3 be non empty set ;
let c4 be BinOp of c3;
let c5 be Element of c3;
let c6 be Function of [:the carrier of c1,c3:],c3;
let c7 be Function of [:c3,the carrier of c2:],c3;
cluster BiModStr(# a3,a4,a5,a6,a7 #) -> non empty ;
coherence
not BiModStr(# c3,c4,c5,c6,c7 #) is empty by STRUCT_0:def 1;
end;

definition
let c1 be non empty Abelian add-associative right_zeroed right_complementable LoopStr ;
func AbGr c1 -> strict AbGroup equals :: VECTSP_2:def 9
 LoopStr(# the carrier of a1,the add of a1,the Zero of a1 #);
coherence
LoopStr(# the carrier of c1,the add of c1,the Zero of c1 #) is strict AbGroup
proof end;
end;

:: deftheorem Def9 defines AbGr VECTSP_2:def 9 :
for b1 being non empty Abelian add-associative right_zeroed right_complementable LoopStr holds AbGr b1 = LoopStr(# the carrier of b1,the add of b1,the Zero of b1 #);

deffunc H1( Ring) -> VectSpStr of a1 = VectSpStr(# the carrier of a1,the add of a1,the Zero of a1,the mult of a1 #);

Lemma21: for b1 being Ring holds
( H1(b1) is Abelian & H1(b1) is add-associative & H1(b1) is right_zeroed & H1(b1) is right_complementable )
proof end;

registration
let c1 be Ring;
cluster non empty Abelian add-associative right_zeroed right_complementable strict VectSpStr of a1;
existence
ex b1 being non empty VectSpStr of c1 st
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict )
proof end;
end;

definition
let c1 be Ring;
canceled;
func LeftModule c1 -> non empty Abelian add-associative right_zeroed right_complementable strict VectSpStr of a1 equals :: VECTSP_2:def 11
 VectSpStr(# the carrier of a1,the add of a1,the Zero of a1,the mult of a1 #);
coherence
VectSpStr(# the carrier of c1,the add of c1,the Zero of c1,the mult of c1 #) is non empty Abelian add-associative right_zeroed right_complementable strict VectSpStr of c1 by Lemma21;
end;

:: deftheorem Def10 VECTSP_2:def 10 :
canceled;

:: deftheorem Def11 defines LeftModule VECTSP_2:def 11 :
for b1 being Ring holds LeftModule b1 = VectSpStr(# the carrier of b1,the add of b1,the Zero of b1,the mult of b1 #);

deffunc H2( Ring) -> RightModStr of a1 = RightModStr(# the carrier of a1,the add of a1,the Zero of a1,the mult of a1 #);

Lemma22: for b1 being Ring holds
( H2(b1) is Abelian & H2(b1) is add-associative & H2(b1) is right_zeroed & H2(b1) is right_complementable )
proof end;

registration
let c1 be Ring;
cluster non empty Abelian add-associative right_zeroed right_complementable strict RightModStr of a1;
existence
ex b1 being non empty RightModStr of c1 st
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict )
proof end;
end;

definition
let c1 be Ring;
canceled;
canceled;
func RightModule c1 -> non empty Abelian add-associative right_zeroed right_complementable strict RightModStr of a1 equals :: VECTSP_2:def 14
 RightModStr(# the carrier of a1,the add of a1,the Zero of a1,the mult of a1 #);
coherence
RightModStr(# the carrier of c1,the add of c1,the Zero of c1,the mult of c1 #) is non empty Abelian add-associative right_zeroed right_complementable strict RightModStr of c1 by Lemma22;
end;

:: deftheorem Def12 VECTSP_2:def 12 :
canceled;

:: deftheorem Def13 VECTSP_2:def 13 :
canceled;

:: deftheorem Def14 defines RightModule VECTSP_2:def 14 :
for b1 being Ring holds RightModule b1 = RightModStr(# the carrier of b1,the add of b1,the Zero of b1,the mult of b1 #);

definition
let c1 be non empty 1-sorted ;
let c2 be non empty RightModStr of c1;
let c3 be Element of c1;
let c4 be Element of c2;
func c4 * c3 -> Element of a2 equals :: VECTSP_2:def 15
the rmult of a2 . a4,a3;
coherence
the rmult of c2 . c4,c3 is Element of c2 ;
end;

:: deftheorem Def15 defines * VECTSP_2:def 15 :
for b1 being non empty 1-sorted
for b2 being non empty RightModStr of b1
for b3 being Element of b1
for b4 being Element of b2 holds b4 * b3 = the rmult of b2 . b4,b3;

definition
canceled;
func op1 -> UnOp of {{} } means :: VECTSP_2:def 17
verum;
existence
ex b1 being UnOp of {{} } st verum ;
uniqueness
for b1, b2 being UnOp of {{} } holds b1 = b2 by FUNCT_2:66;
func op0 -> Element of {{} } means :: VECTSP_2:def 18
verum;
existence
ex b1 being Element of {{} } st verum ;
uniqueness
for b1, b2 being Element of {{} } holds b1 = b2
proof end;
end;

:: deftheorem Def16 VECTSP_2:def 16 :
canceled;

:: deftheorem Def17 defines op1 VECTSP_2:def 17 :
for b1 being UnOp of {{} } holds
( b1 = op1 iff verum );

:: deftheorem Def18 defines op0 VECTSP_2:def 18 :
for b1 being Element of {{} } holds
( b1 = op0 iff verum );

deffunc H3( Ring, Ring) -> BiModStr of a1,a2 = BiModStr(# {{} },op2 ,op0 ,(pr2 the carrier of a1,{{} }),(pr1 {{} },the carrier of a2) #);

Lemma23: for b1, b2 being Ring holds
( H3(b1,b2) is Abelian & H3(b1,b2) is add-associative & H3(b1,b2) is right_zeroed & H3(b1,b2) is right_complementable )
proof end;

registration
let c1, c2 be Ring;
cluster non empty Abelian add-associative right_zeroed right_complementable strict BiModStr of a1,a2;
existence
ex b1 being non empty BiModStr of c1,c2 st
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict )
proof end;
end;

definition
let c1, c2 be Ring;
canceled;
canceled;
func BiModule c1,c2 -> non empty Abelian add-associative right_zeroed right_complementable strict BiModStr of a1,a2 equals :: VECTSP_2:def 21
 BiModStr(# {{} },op2 ,op0 ,(pr2 the carrier of a1,{{} }),(pr1 {{} },the carrier of a2) #);
coherence
BiModStr(# {{} },op2 ,op0 ,(pr2 the carrier of c1,{{} }),(pr1 {{} },the carrier of c2) #) is non empty Abelian add-associative right_zeroed right_complementable strict BiModStr of c1,c2 by Lemma23;
end;

:: deftheorem Def19 VECTSP_2:def 19 :
canceled;

:: deftheorem Def20 VECTSP_2:def 20 :
canceled;

:: deftheorem Def21 defines BiModule VECTSP_2:def 21 :
for b1, b2 being Ring holds BiModule b1,b2 = BiModStr(# {{} },op2 ,op0 ,(pr2 the carrier of b1,{{} }),(pr1 {{} },the carrier of b2) #);

theorem Th58: :: VECTSP_2:58
canceled;

theorem Th59: :: VECTSP_2:59
canceled;

theorem Th60: :: VECTSP_2:60
canceled;

theorem Th61: :: VECTSP_2:61
canceled;

theorem Th62: :: VECTSP_2:62
canceled;

theorem Th63: :: VECTSP_2:63
canceled;

theorem Th64: :: VECTSP_2:64
canceled;

theorem Th65: :: VECTSP_2:65
canceled;

theorem Th66: :: VECTSP_2:66
canceled;

theorem Th67: :: VECTSP_2:67
canceled;

theorem Th68: :: VECTSP_2:68
canceled;

theorem Th69: :: VECTSP_2:69
canceled;

theorem Th70: :: VECTSP_2:70
canceled;

theorem Th71: :: VECTSP_2:71
for b1 being Ring
for b2, b3 being Scalar of b1
for b4, b5 being Vector of (LeftModule b1) holds
( b2 * (b4 + b5) = (b2 * b4) + (b2 * b5) & (b2 + b3) * b4 = (b2 * b4) + (b3 * b4) & (b2 * b3) * b4 = b2 * (b3 * b4) & (1. b1) * b4 = b4 )
proof end;

registration
let c1 be Ring;
cluster non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like VectSpStr of a1;
existence
ex b1 being non empty VectSpStr of c1 st
( b1 is VectSp-like & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict )
proof end;
end;

definition
let c1 be Ring;
mode LeftMod of a1 is non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of a1;
end;

Lemma25: for b1 being Ring holds LeftModule b1 is VectSp-like
proof end;

registration
let c1 be Ring;
cluster LeftModule a1 -> non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like ;
coherence
( LeftModule c1 is Abelian & LeftModule c1 is add-associative & LeftModule c1 is right_zeroed & LeftModule c1 is right_complementable & LeftModule c1 is strict & LeftModule c1 is VectSp-like ) by Lemma25;
end;

theorem Th72: :: VECTSP_2:72
canceled;

theorem Th73: :: VECTSP_2:73
canceled;

theorem Th74: :: VECTSP_2:74
canceled;

theorem Th75: :: VECTSP_2:75
canceled;

theorem Th76: :: VECTSP_2:76
canceled;

theorem Th77: :: VECTSP_2:77
for b1 being Ring
for b2, b3 being Scalar of b1
for b4, b5 being Vector of (RightModule b1) holds
( (b4 + b5) * b2 = (b4 * b2) + (b5 * b2) & b4 * (b2 + b3) = (b4 * b2) + (b4 * b3) & b4 * (b3 * b2) = (b4 * b3) * b2 & b4 * (1. b1) = b4 )
proof end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be non empty RightModStr of c1;
canceled;
attr a2 is RightMod-like means :Def23: :: VECTSP_2:def 23
for b1, b2 being Scalar of a1
for b3, b4 being Vector of a2 holds
( (b3 + b4) * b1 = (b3 * b1) + (b4 * b1) & b3 * (b1 + b2) = (b3 * b1) + (b3 * b2) & b3 * (b2 * b1) = (b3 * b2) * b1 & b3 * (1. a1) = b3 );
end;

:: deftheorem Def22 VECTSP_2:def 22 :
canceled;

:: deftheorem Def23 defines RightMod-like VECTSP_2:def 23 :
for b1 being non empty doubleLoopStr
for b2 being non empty RightModStr of b1 holds
( b2 is RightMod-like iff for b3, b4 being Scalar of b1
for b5, b6 being Vector of b2 holds
( (b5 + b6) * b3 = (b5 * b3) + (b6 * b3) & b5 * (b3 + b4) = (b5 * b3) + (b5 * b4) & b5 * (b4 * b3) = (b5 * b4) * b3 & b5 * (1. b1) = b5 ) );

registration
let c1 be Ring;
cluster non empty Abelian add-associative right_zeroed right_complementable strict RightMod-like RightModStr of a1;
existence
ex b1 being non empty RightModStr of c1 st
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is RightMod-like & b1 is strict )
proof end;
end;

definition
let c1 be Ring;
mode RightMod of a1 is non empty Abelian add-associative right_zeroed right_complementable RightMod-like RightModStr of a1;
end;

Lemma28: for b1 being Ring holds RightModule b1 is RightMod-like
proof end;

registration
let c1 be Ring;
cluster RightModule a1 -> non empty Abelian add-associative right_zeroed right_complementable strict RightMod-like ;
coherence
( RightModule c1 is Abelian & RightModule c1 is add-associative & RightModule c1 is right_zeroed & RightModule c1 is right_complementable & RightModule c1 is RightMod-like ) by Lemma28;
end;

Lemma29: for b1, b2 being Ring
for b3, b4 being Scalar of b1
for b5, b6 being Scalar of b2
for b7, b8 being Vector of (BiModule b1,b2) holds
( b3 * (b7 + b8) = (b3 * b7) + (b3 * b8) & (b3 + b4) * b7 = (b3 * b7) + (b4 * b7) & (b3 * b4) * b7 = b3 * (b4 * b7) & (1. b1) * b7 = b7 & (b7 + b8) * b5 = (b7 * b5) + (b8 * b5) & b7 * (b5 + b6) = (b7 * b5) + (b7 * b6) & b7 * (b6 * b5) = (b7 * b6) * b5 & b7 * (1. b2) = b7 & b3 * (b7 * b5) = (b3 * b7) * b5 )
proof end;

definition
let c1, c2 be Ring;
let c3 be non empty BiModStr of c1,c2;
attr a3 is BiMod-like means :Def24: :: VECTSP_2:def 24
for b1 being Scalar of a1
for b2 being Scalar of a2
for b3 being Vector of a3 holds b1 * (b3 * b2) = (b1 * b3) * b2;
end;

:: deftheorem Def24 defines BiMod-like VECTSP_2:def 24 :
for b1, b2 being Ring
for b3 being non empty BiModStr of b1,b2 holds
( b3 is BiMod-like iff for b4 being Scalar of b1
for b5 being Scalar of b2
for b6 being Vector of b3 holds b4 * (b6 * b5) = (b4 * b6) * b5 );

registration
let c1, c2 be Ring;
cluster non empty Abelian add-associative right_zeroed right_complementable VectSp-like strict RightMod-like BiMod-like BiModStr of a1,a2;
existence
ex b1 being non empty BiModStr of c1,c2 st
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is RightMod-like & b1 is VectSp-like & b1 is BiMod-like & b1 is strict )
proof end;
end;

definition
let c1, c2 be Ring;
mode BiMod of a1,a2 is non empty Abelian add-associative right_zeroed right_complementable VectSp-like RightMod-like BiMod-like BiModStr of a1,a2;
end;

theorem Th78: :: VECTSP_2:78
canceled;

theorem Th79: :: VECTSP_2:79
canceled;

theorem Th80: :: VECTSP_2:80
canceled;

theorem Th81: :: VECTSP_2:81
canceled;

theorem Th82: :: VECTSP_2:82
canceled;

theorem Th83: :: VECTSP_2:83
for b1, b2 being Ring
for b3 being non empty BiModStr of b1,b2 holds
( ( for b4, b5 being Scalar of b1
for b6, b7 being Scalar of b2
for b8, b9 being Vector of b3 holds
( b4 * (b8 + b9) = (b4 * b8) + (b4 * b9) & (b4 + b5) * b8 = (b4 * b8) + (b5 * b8) & (b4 * b5) * b8 = b4 * (b5 * b8) & (1. b1) * b8 = b8 & (b8 + b9) * b6 = (b8 * b6) + (b9 * b6) & b8 * (b6 + b7) = (b8 * b6) + (b8 * b7) & b8 * (b7 * b6) = (b8 * b7) * b6 & b8 * (1. b2) = b8 & b4 * (b8 * b6) = (b4 * b8) * b6 ) ) iff ( b3 is RightMod-like & b3 is VectSp-like & b3 is BiMod-like ) ) by Def23, Def24, VECTSP_1:def 26;

theorem Th84: :: VECTSP_2:84
for b1, b2 being Ring holds BiModule b1,b2 is BiMod of b1,b2
proof end;

registration
let c1, c2 be Ring;
cluster BiModule a1,a2 -> non empty Abelian add-associative right_zeroed right_complementable VectSp-like strict RightMod-like BiMod-like ;
coherence
( BiModule c1,c2 is Abelian & BiModule c1,c2 is add-associative & BiModule c1,c2 is right_zeroed & BiModule c1,c2 is right_complementable & BiModule c1,c2 is RightMod-like & BiModule c1,c2 is VectSp-like & BiModule c1,c2 is BiMod-like ) by Th84;
end;

theorem Th85: :: VECTSP_2:85
for b1 being non empty multLoopStr st b1 is well-unital holds
1_ b1 = 1. b1 by Lemma3;