:: by Micha{\l} Muzalewski

::

:: Received June 19, 1992

:: Copyright (c) 1992-2021 Association of Mizar Users

theorem :: LMOD_6:1

theorem :: LMOD_6:2

for K being Ring

for r being Scalar of K

for V being LeftMod of K

for a being Vector of V

for v being Vector of ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) st a = v holds

r * a = r * v

for r being Scalar of K

for V being LeftMod of K

for a being Vector of V

for v being Vector of ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) st a = v holds

r * a = r * v

proof end;

theorem Th3: :: LMOD_6:3

for K being Ring

for V being LeftMod of K holds ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is strict Subspace of V

for V being LeftMod of K holds ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is strict Subspace of V

proof end;

:: deftheorem defines trivial LMOD_6:def 1 :

for K being Ring holds

( K is trivial iff 0. K = 1_ K );

for K being Ring holds

( K is trivial iff 0. K = 1_ K );

theorem Th5: :: LMOD_6:5

for K being Ring

for V being LeftMod of K st K is trivial holds

( ( for r being Scalar of K holds r = 0. K ) & ( for a being Vector of V holds a = 0. V ) )

for V being LeftMod of K st K is trivial holds

( ( for r being Scalar of K holds r = 0. K ) & ( for a being Vector of V holds a = 0. V ) )

proof end;

theorem :: LMOD_6:6

theorem :: LMOD_6:7

for K being Ring

for V being LeftMod of K holds

( V is trivial iff ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (0). V )

for V being LeftMod of K holds

( V is trivial iff ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (0). V )

proof end;

definition

let K be Ring;

let V be LeftMod of K;

let W be strict Subspace of V;

coherence

W is Element of Submodules V by VECTSP_5:def 3;

end;
let V be LeftMod of K;

let W be strict Subspace of V;

coherence

W is Element of Submodules V by VECTSP_5:def 3;

:: deftheorem defines @ LMOD_6:def 2 :

for K being Ring

for V being LeftMod of K

for W being strict Subspace of V holds @ W = W;

for K being Ring

for V being LeftMod of K

for W being strict Subspace of V holds @ W = W;

theorem Th8: :: LMOD_6:8

for K being Ring

for V being LeftMod of K

for W being Subspace of V

for A being Subset of W holds A is Subset of V

for V being LeftMod of K

for W being Subspace of V

for A being Subset of W holds A is Subset of V

proof end;

definition

let K be Ring;

let V be LeftMod of K;

let W be Subspace of V;

let A be Subset of W;

coherence

A is Subset of V by Th8;

end;
let V be LeftMod of K;

let W be Subspace of V;

let A be Subset of W;

coherence

A is Subset of V by Th8;

:: deftheorem defines @ LMOD_6:def 3 :

for K being Ring

for V being LeftMod of K

for W being Subspace of V

for A being Subset of W holds @ A = A;

for K being Ring

for V being LeftMod of K

for W being Subspace of V

for A being Subset of W holds @ A = A;

registration

let K be Ring;

let V be LeftMod of K;

let W be Subspace of V;

let A be non empty Subset of W;

coherence

not @ A is empty ;

end;
let V be LeftMod of K;

let W be Subspace of V;

let A be non empty Subset of W;

coherence

not @ A is empty ;

theorem :: LMOD_6:9

theorem :: LMOD_6:10

theorem Th12: :: LMOD_6:12

for K being Ring

for V being LeftMod of K

for A being Subset of V

for l being Linear_Combination of A st A <> {} & A is linearly-closed holds

Sum l in A

for V being LeftMod of K

for A being Subset of V

for l being Linear_Combination of A st A <> {} & A is linearly-closed holds

Sum l in A

proof end;

theorem :: LMOD_6:13

for K being Ring

for V being LeftMod of K

for A being Subset of V st 0. V in A & A is linearly-closed holds

A = [#] (Lin A)

for V being LeftMod of K

for A being Subset of V st 0. V in A & A is linearly-closed holds

A = [#] (Lin A)

proof end;

definition

let K be Ring;

let V be LeftMod of K;

let a be Vector of V;

correctness

coherence

Lin {a} is strict Subspace of V;

;

end;
let V be LeftMod of K;

let a be Vector of V;

correctness

coherence

Lin {a} is strict Subspace of V;

;

:: deftheorem defines <: LMOD_6:def 4 :

for K being Ring

for V being LeftMod of K

for a being Vector of V holds <:a:> = Lin {a};

for K being Ring

for V being LeftMod of K

for a being Vector of V holds <:a:> = Lin {a};

definition

let K be Ring;

let M, N be LeftMod of K;

reflexivity

for M being LeftMod of K holds M is Subspace of M by VECTSP_4:24;

end;
let M, N be LeftMod of K;

reflexivity

for M being LeftMod of K holds M is Subspace of M by VECTSP_4:24;

:: deftheorem defines c= LMOD_6:def 5 :

for K being Ring

for M, N being LeftMod of K holds

( M c= N iff M is Subspace of N );

for K being Ring

for M, N being LeftMod of K holds

( M c= N iff M is Subspace of N );

theorem Th14: :: LMOD_6:14

for K being Ring

for M, N being LeftMod of K

for x being object st M c= N holds

( ( x in M implies x in N ) & ( x is Vector of M implies x is Vector of N ) ) by VECTSP_4:9, VECTSP_4:10;

for M, N being LeftMod of K

for x being object st M c= N holds

( ( x in M implies x in N ) & ( x is Vector of M implies x is Vector of N ) ) by VECTSP_4:9, VECTSP_4:10;

theorem :: LMOD_6:15

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;

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;

theorem :: LMOD_6:16

for K being Ring

for M1, M2, N being LeftMod of K st M1 c= N & M2 c= N holds

( 0. M1 = 0. M2 & 0. M1 in M2 & ( the carrier of M1 c= the carrier of M2 implies M1 c= M2 ) & ( ( for n being Vector of N st n in M1 holds

n in M2 ) implies M1 c= M2 ) & ( the carrier of M1 = the carrier of M2 & M1 is strict & M2 is strict implies M1 = M2 ) & (0). M1 c= M2 ) by VECTSP_4:12, VECTSP_4:18, VECTSP_4:27, VECTSP_4:28, VECTSP_4:29, VECTSP_4:40;

for M1, M2, N being LeftMod of K st M1 c= N & M2 c= N holds

( 0. M1 = 0. M2 & 0. M1 in M2 & ( the carrier of M1 c= the carrier of M2 implies M1 c= M2 ) & ( ( for n being Vector of N st n in M1 holds

n in M2 ) implies M1 c= M2 ) & ( the carrier of M1 = the carrier of M2 & M1 is strict & M2 is strict implies M1 = M2 ) & (0). M1 c= M2 ) by VECTSP_4:12, VECTSP_4:18, VECTSP_4:27, VECTSP_4:28, VECTSP_4:29, VECTSP_4:40;

theorem :: LMOD_6:17

theorem :: LMOD_6:18

theorem :: LMOD_6:19

theorem :: LMOD_6:20

theorem :: LMOD_6:22

theorem :: LMOD_6:23

theorem :: LMOD_6:24

theorem :: LMOD_6:25

theorem :: LMOD_6:26

theorem :: LMOD_6:27

theorem :: LMOD_6:28

theorem :: LMOD_6:29

theorem :: LMOD_6:30

theorem :: LMOD_6:31

theorem :: LMOD_6:32

theorem :: LMOD_6:33

theorem :: LMOD_6:34

theorem :: LMOD_6:35

theorem Th37: :: LMOD_6:37

for K being Ring

for V being LeftMod of K

for W1, W2 being Subspace of V holds

( W1 c= W2 iff for a being Vector of V st a in W1 holds

a in W2 ) by VECTSP_4:8, VECTSP_4:28;

for V being LeftMod of K

for W1, W2 being Subspace of V holds

( W1 c= W2 iff for a being Vector of V st a in W1 holds

a in W2 ) by VECTSP_4:8, VECTSP_4:28;

theorem Th38: :: LMOD_6:38

for K being Ring

for V being LeftMod of K

for W1, W2 being Subspace of V holds

( W1 c= W2 iff [#] W1 c= [#] W2 )

for V being LeftMod of K

for W1, W2 being Subspace of V holds

( W1 c= W2 iff [#] W1 c= [#] W2 )

proof end;

theorem :: LMOD_6:39

theorem :: LMOD_6:40

for K being Ring

for V being LeftMod of K

for W, W1, W2 being Subspace of V holds

( (0). W c= V & (0). V c= W & (0). W1 c= W2 ) by VECTSP_4:38, VECTSP_4:39, VECTSP_4:40;

for V being LeftMod of K

for W, W1, W2 being Subspace of V holds

( (0). W c= V & (0). V c= W & (0). W1 c= W2 ) by VECTSP_4:38, VECTSP_4:39, VECTSP_4:40;