:: VECTSP_2 semantic presentation

definition

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

end;

:: deftheorem VECTSP_2:def 1 :

:: deftheorem Def2 defines well-unital VECTSP_2:def 2 :

Lm1: for L being non empty multLoopStr st L is well-unital holds
L is unital

proof end;

registration

cluster non empty well-unital -> non empty unital multLoopStr ;
coherence by Lm1;

end;

Lm2: for L being non empty multLoopStr st L is well-unital holds
1_ L = 1. L

proof end;

registration

cluster non empty Abelian add-associative right_zeroed right_complementable unital strict distributive doubleLoopStr ;
existence

proof end;

end;

theorem :: VECTSP_2:1

for FS being non empty doubleLoopStr holds
( ( for x, y, z being Scalar of FS holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. FS) = x & x + (- x) = 0. FS & x * (1. FS) = x & (1. FS) * x = x & (x * y) * z = x * (y * z) & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) ) iff FS is Ring )

proof end;

registration

cluster strict doubleLoopStr ;
existence

proof end;

end;

registration

cluster commutative doubleLoopStr ;
existence

proof end;

end;

definition

mode comRing is commutative Ring;

end;

registration

cluster strict doubleLoopStr ;
existence

proof end;

end;

definition

let IT be non empty multLoopStr_0 ;
canceled;
canceled;
attr IT is domRing-like means :Def5: :: VECTSP_2:def 5
for x, y being Element of IT holds
( not x * y = 0. IT or x = 0. IT or y = 0. IT );

end;

:: deftheorem VECTSP_2:def 3 :

:: deftheorem VECTSP_2:def 4 :

:: deftheorem Def5 defines domRing-like VECTSP_2:def 5 :

registration

cluster strict non degenerated domRing-like doubleLoopStr ;
existence

proof end;

end;

definition

mode domRing is non degenerated domRing-like comRing;

end;

theorem :: VECTSP_2:2

canceled;

theorem :: VECTSP_2:3

canceled;

theorem :: VECTSP_2:4

canceled;

theorem :: VECTSP_2:5

canceled;

theorem :: VECTSP_2:6

canceled;

theorem :: VECTSP_2:7

canceled;

theorem :: VECTSP_2:8

canceled;

theorem :: VECTSP_2:9

canceled;

theorem :: VECTSP_2:10

canceled;

theorem :: VECTSP_2:11

canceled;

theorem :: VECTSP_2:12

canceled;

theorem :: VECTSP_2:13

for F being Field holds F is domRing

proof end;

registration

cluster Field-like non degenerated doubleLoopStr ;
existence

proof end;

end;

definition

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

end;

registration

cluster strict doubleLoopStr ;
existence

proof end;

end;

theorem :: VECTSP_2:14

canceled;

theorem :: VECTSP_2:15

canceled;

theorem :: VECTSP_2:16

for R being Ring st ( for x being Scalar of R holds
( ( x <> 0. R implies ex y being Scalar of R st x * y = 1. R ) & 0. R <> 1. R ) ) holds
R is Skew-Field by VECTSP_1:def 20, VECTSP_1:def 21;

registration

cluster non empty commutative left_unital -> non empty unital multLoopStr ;
coherence

proof end;

cluster non empty commutative right_unital -> non empty unital multLoopStr ;
coherence

proof end;

end;

Lm3: for R being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for x, y, z being Scalar of R st x + y = z holds
x = z - y

proof end;

Lm4: for R being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for x, z, y being Scalar of R st x = z - y holds
x + y = z

proof end;

theorem :: VECTSP_2:17

canceled;

theorem :: VECTSP_2:18

canceled;

theorem :: VECTSP_2:19

canceled;

theorem :: VECTSP_2:20

canceled;

theorem :: VECTSP_2:21

canceled;

theorem :: VECTSP_2:22

for R being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for x, y, z being Scalar of R holds
( ( x + y = z implies x = z - y ) & ( x = z - y implies x + y = z ) & ( x + y = z implies y = z - x ) & ( y = z - x implies x + y = z ) ) by Lm3, Lm4;

theorem :: VECTSP_2:23

canceled;

theorem :: VECTSP_2:24

canceled;

theorem :: VECTSP_2:25

canceled;

theorem :: VECTSP_2:26

canceled;

theorem :: VECTSP_2:27

canceled;

theorem :: VECTSP_2:28

canceled;

theorem :: VECTSP_2:29

canceled;

theorem :: VECTSP_2:30

canceled;

theorem :: VECTSP_2:31

canceled;

theorem :: VECTSP_2:32

canceled;

theorem :: VECTSP_2:33

canceled;

theorem Th34: :: VECTSP_2:34

for R being non empty add-associative right_zeroed right_complementable LoopStr
for x being Element of R holds
( x = 0. R iff - x = 0. R )

proof end;

theorem :: VECTSP_2:35

canceled;

theorem :: VECTSP_2:36

canceled;

theorem :: VECTSP_2:37

canceled;

theorem :: VECTSP_2:38

for R being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for x, y being Element of R ex z being Element of R st
( x = y + z & x = z + y )

proof end;

theorem Th39: :: VECTSP_2:39

for F being non empty add-associative right_zeroed right_complementable distributive non degenerated doubleLoopStr
for x, y being Element of F st x * y = 1. F holds
( x <> 0. F & y <> 0. F )

proof end;

theorem Th40: :: VECTSP_2:40

for SF being non empty Abelian add-associative right_zeroed right_complementable associative right_unital distributive left_unital Field-like non degenerated doubleLoopStr
for x being Element of SF st x <> 0. SF holds
ex y being Element of SF st y * x = 1. SF

proof end;

theorem Th41: :: VECTSP_2:41

for SF being Skew-Field
for x, y being Scalar of SF st x * y = 1. SF holds
y * x = 1. SF

proof end;

theorem Th42: :: VECTSP_2:42

for SF being non empty Abelian add-associative right_zeroed right_complementable unital associative distributive Field-like non degenerated doubleLoopStr
for x, y, z being Element of SF st x * y = x * z & x <> 0. SF holds
y = z

proof end;

definition

let SF be non empty Abelian add-associative right_zeroed right_complementable unital associative distributive Field-like non degenerated doubleLoopStr ;
let x be Element of SF;
assume A1: x <> 0. SF ;
canceled;
func x " -> Scalar of SF means :Def7: :: VECTSP_2:def 7
x * it = 1. SF;
existence by A1, VECTSP_1:def 20;
uniqueness by A1, Th42;

end;

:: deftheorem VECTSP_2:def 6 :

:: deftheorem Def7 defines " VECTSP_2:def 7 :

definition

let SF be Skew-Field;
let x, y be Scalar of SF;
func x / y -> Scalar of SF equals :: VECTSP_2:def 8
x * (y " );
correctness ;

end;

:: deftheorem defines / VECTSP_2:def 8 :

theorem Th43: :: VECTSP_2:43

for SF being Skew-Field
for x being Scalar of SF st x <> 0. SF holds
( x * (x " ) = 1. SF & (x " ) * x = 1. SF )

proof end;

theorem :: VECTSP_2:44

canceled;

theorem Th45: :: VECTSP_2:45

for SF being Skew-Field
for x, y being Scalar of SF st x * y = 1. SF holds
( x = y " & y = x " )

proof end;

theorem Th46: :: VECTSP_2:46

for SF being Skew-Field
for x, y being Scalar of SF st x <> 0. SF & y <> 0. SF holds
(x " ) * (y " ) = (y * x) "

proof end;

theorem :: VECTSP_2:47

for SF being Skew-Field
for x, y being Scalar of SF holds
( not x * y = 0. SF or x = 0. SF or y = 0. SF )

proof end;

theorem Th48: :: VECTSP_2:48

for SF being Skew-Field
for x being Scalar of SF st x <> 0. SF holds
x " <> 0. SF

proof end;

theorem Th49: :: VECTSP_2:49

for SF being Skew-Field
for x being Scalar of SF st x <> 0. SF holds
(x " ) " = x

proof end;

theorem Th50: :: VECTSP_2:50

for SF being Skew-Field
for x being Scalar of SF st x <> 0. SF holds
( (1. SF) / x = x " & (1. SF) / (x " ) = x )

proof end;

theorem :: VECTSP_2:51

for SF being Skew-Field
for x being Scalar of SF st x <> 0. SF holds
( x * ((1. SF) / x) = 1. SF & ((1. SF) / x) * x = 1. SF )

proof end;

theorem :: VECTSP_2:52

for SF being Skew-Field
for x being Scalar of SF st x <> 0. SF holds
x / x = 1. SF by Th43;

theorem Th53: :: VECTSP_2:53

for SF being Skew-Field
for y, z, x being Scalar of SF st y <> 0. SF & z <> 0. SF holds
x / y = (x * z) / (y * z)

proof end;

theorem Th54: :: VECTSP_2:54

for SF being Skew-Field
for y, x being Scalar of SF st y <> 0. SF holds
( - (x / y) = (- x) / y & x / (- y) = - (x / y) )

proof end;

theorem :: VECTSP_2:55

for SF being Skew-Field
for z, x, y being Scalar of SF st z <> 0. SF holds
( (x / z) + (y / z) = (x + y) / z & (x / z) - (y / z) = (x - y) / z )

proof end;

theorem :: VECTSP_2:56

for SF being Skew-Field
for y, z, x being Scalar of SF st y <> 0. SF & z <> 0. SF holds
x / (y / z) = (x * z) / y

proof end;

theorem :: VECTSP_2:57

for SF being Skew-Field
for y, x being Scalar of SF st y <> 0. SF holds
(x / y) * y = x

proof end;

definition

let FS be 1-sorted ;
attr c₂ is strict;
struct RightModStr of FS -> LoopStr ;
aggr RightModStr(# carrier, add, Zero, rmult #) -> RightModStr of FS;
sel rmult c₂ -> Function of [:the carrier of c₂,the carrier of FS:],the carrier of c₂;

end;

registration

let FS be 1-sorted ;
cluster non empty RightModStr of FS;
existence

proof end;

end;

registration

let FS be 1-sorted ;
let A be non empty set ;
let a be BinOp of A;
let Z be Element of A;
let r be Function of [:A,the carrier of FS:],A;
cluster RightModStr(# A,a,Z,r #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

definition

let FS be non empty doubleLoopStr ;
let RMS be non empty RightModStr of FS;
mode Scalar of RMS is Element of FS;
mode Vector of RMS is Element of RMS;

end;

definition

let FS1, FS2 be 1-sorted ;
attr c₃ is strict;
struct BiModStr of FS1,FS2 -> VectSpStr of FS1, RightModStr of FS2;
aggr BiModStr(# carrier, add, Zero, lmult, rmult #) -> BiModStr of FS1,FS2;

end;

registration

let FS1, FS2 be 1-sorted ;
cluster non empty BiModStr of FS1,FS2;
existence

proof end;

end;

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 by STRUCT_0:def 1;

end;

definition

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

proof end;

end;

:: deftheorem defines AbGr VECTSP_2:def 9 :

deffunc H₁( Ring) -> VectSpStr of $1 = VectSpStr(# the carrier of $1,the add of $1,the Zero of $1,the mult of $1 #);

Lm5: for R being Ring holds
( H₁(R) is Abelian & H₁(R) is add-associative & H₁(R) is right_zeroed & H₁(R) is right_complementable )

proof end;

registration

let R be Ring;
cluster non empty Abelian add-associative right_zeroed right_complementable strict VectSpStr of R;
existence

proof end;

end;

definition

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

end;

:: deftheorem VECTSP_2:def 10 :

:: deftheorem defines LeftModule VECTSP_2:def 11 :

deffunc H₂( Ring) -> RightModStr of $1 = RightModStr(# the carrier of $1,the add of $1,the Zero of $1,the mult of $1 #);

Lm6: for R being Ring holds
( H₂(R) is Abelian & H₂(R) is add-associative & H₂(R) is right_zeroed & H₂(R) is right_complementable )

proof end;

registration

let R be Ring;
cluster non empty Abelian add-associative right_zeroed right_complementable strict RightModStr of R;
existence

proof end;

end;

definition

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

end;

:: deftheorem VECTSP_2:def 12 :

:: deftheorem VECTSP_2:def 13 :

:: deftheorem defines RightModule VECTSP_2:def 14 :

definition

let R be non empty 1-sorted ;
let V be non empty RightModStr of R;
let x be Element of R;
let v be Element of V;
func v * x -> Element of V equals :: VECTSP_2:def 15
the rmult of V . v,x;
coherence ;

end;

:: deftheorem defines * VECTSP_2:def 15 :

definition

canceled;
func op1 -> UnOp of {{} } means :: VECTSP_2:def 17
verum;
existence ;
uniqueness by FUNCT_2:66;
func op0 -> Element of {{} } means :: VECTSP_2:def 18
verum;
existence ;
uniqueness

proof end;

end;

:: deftheorem VECTSP_2:def 16 :

:: deftheorem defines op1 VECTSP_2:def 17 :

:: deftheorem defines op0 VECTSP_2:def 18 :

deffunc H₃( Ring, Ring) -> BiModStr of $1,$2 = BiModStr(# {{} },op2 ,op0 ,(pr2 the carrier of $1,{{} }),(pr1 {{} },the carrier of $2) #);

Lm7: for R1, R2 being Ring holds
( H₃(R1,R2) is Abelian & H₃(R1,R2) is add-associative & H₃(R1,R2) is right_zeroed & H₃(R1,R2) is right_complementable )

proof end;

registration

let R1, R2 be Ring;
cluster non empty Abelian add-associative right_zeroed right_complementable strict BiModStr of R1,R2;
existence

proof end;

end;

definition

let R1, R2 be Ring;
canceled;
canceled;
func BiModule R1,R2 -> non empty Abelian add-associative right_zeroed right_complementable strict BiModStr of R1,R2 equals :: VECTSP_2:def 21
BiModStr(# {{} },op2 ,op0 ,(pr2 the carrier of R1,{{} }),(pr1 {{} },the carrier of R2) #);
coherence by Lm7;

end;

:: deftheorem VECTSP_2:def 19 :

:: deftheorem VECTSP_2:def 20 :

:: deftheorem defines BiModule VECTSP_2:def 21 :

theorem :: VECTSP_2:58

canceled;

theorem :: VECTSP_2:59

canceled;

theorem :: VECTSP_2:60

canceled;

theorem :: VECTSP_2:61

canceled;

theorem :: VECTSP_2:62

canceled;

theorem :: VECTSP_2:63

canceled;

theorem :: VECTSP_2:64

canceled;

theorem :: VECTSP_2:65

canceled;

theorem :: VECTSP_2:66

canceled;

theorem :: VECTSP_2:67

canceled;

theorem :: VECTSP_2:68

canceled;

theorem :: VECTSP_2:69

canceled;

theorem :: VECTSP_2:70

canceled;

theorem Th71: :: VECTSP_2:71

for R being Ring
for x, y being Scalar of R
for v, w being Vector of (LeftModule R) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. R) * v = v )

proof end;

registration

let R be Ring;
cluster non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like VectSpStr of R;
existence

proof end;

end;

definition

let R be Ring;
mode LeftMod of R is non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of R;

end;

Lm8: for R being Ring holds LeftModule R is VectSp-like

proof end;

registration

let R be Ring;
cluster LeftModule R -> non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like ;
coherence by Lm8;

end;

theorem :: VECTSP_2:72

canceled;

theorem :: VECTSP_2:73

canceled;

theorem :: VECTSP_2:74

canceled;

theorem :: VECTSP_2:75

canceled;

theorem :: VECTSP_2:76

canceled;

theorem Th77: :: VECTSP_2:77

for R being Ring
for x, y being Scalar of R
for v, w being Vector of (RightModule R) 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 )

proof end;

definition

let R be non empty doubleLoopStr ;
let IT be non empty RightModStr of R;
canceled;
attr IT is RightMod-like means :Def23: :: VECTSP_2:def 23
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 );

end;

:: deftheorem VECTSP_2:def 22 :

:: deftheorem Def23 defines RightMod-like VECTSP_2:def 23 :

registration

let R be Ring;
cluster non empty Abelian add-associative right_zeroed right_complementable strict RightMod-like RightModStr of R;
existence

proof end;

end;

definition

let R be Ring;
mode RightMod of R is non empty Abelian add-associative right_zeroed right_complementable RightMod-like RightModStr of R;

end;

Lm9: for R being Ring holds RightModule R is RightMod-like

proof end;

registration

let R be Ring;
cluster RightModule R -> non empty Abelian add-associative right_zeroed right_complementable strict RightMod-like ;
coherence by Lm9;

end;

Lm10: 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 )

proof end;

definition

let R1, R2 be Ring;
let IT be non empty BiModStr of R1,R2;
attr IT is BiMod-like means :Def24: :: VECTSP_2:def 24
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;

end;

:: deftheorem Def24 defines BiMod-like VECTSP_2:def 24 :

registration

let R1, R2 be Ring;
cluster non empty Abelian add-associative right_zeroed right_complementable VectSp-like strict RightMod-like BiMod-like BiModStr of R1,R2;
existence

proof end;

end;

definition

let R1, R2 be Ring;
mode BiMod of R1,R2 is non empty Abelian add-associative right_zeroed right_complementable VectSp-like RightMod-like BiMod-like BiModStr of R1,R2;

end;

theorem :: VECTSP_2:78

canceled;

theorem :: VECTSP_2:79

canceled;

theorem :: VECTSP_2:80

canceled;

theorem :: VECTSP_2:81

canceled;

theorem :: VECTSP_2:82

canceled;

theorem :: VECTSP_2:83

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 VectSp-like & V is BiMod-like ) ) by Def23, Def24, VECTSP_1:def 26;

theorem Th84: :: VECTSP_2:84

for R1, R2 being Ring holds BiModule R1,R2 is BiMod of R1,R2

proof end;

registration

let R1, R2 be Ring;
cluster BiModule R1,R2 -> non empty Abelian add-associative right_zeroed right_complementable VectSp-like strict RightMod-like BiMod-like ;
coherence by Th84;

end;

theorem :: VECTSP_2:85

for L being non empty multLoopStr st L is well-unital holds
1_ L = 1. L by Lm2;