begin
scheme
ElementEq{
F1()
-> set ,
P1[
set ] } :
for
X1,
X2 being
Element of
F1() st ( for
x being
set holds
(
x in X1 iff
P1[
x] ) ) & ( for
x being
set holds
(
x in X2 iff
P1[
x] ) ) holds
X1 = X2
scheme
TriOpEq{
F1()
-> non
empty set ,
F2(
Element of
F1(),
Element of
F1(),
Element of
F1())
-> set } :
for
f1,
f2 being
TriOp of
F1() st ( for
a,
b,
c being
Element of
F1() holds
f1 . a,
b,
c = F2(
a,
b,
c) ) & ( for
a,
b,
c being
Element of
F1() holds
f2 . a,
b,
c = F2(
a,
b,
c) ) holds
f1 = f2
scheme
QuaOpEq{
F1()
-> non
empty set ,
F2(
Element of
F1(),
Element of
F1(),
Element of
F1(),
Element of
F1())
-> set } :
for
f1,
f2 being
QuaOp of
F1() st ( for
a,
b,
c,
d being
Element of
F1() holds
f1 . a,
b,
c,
d = F2(
a,
b,
c,
d) ) & ( for
a,
b,
c,
d being
Element of
F1() holds
f2 . a,
b,
c,
d = F2(
a,
b,
c,
d) ) holds
f1 = f2
scheme
Fr3{
F1()
-> set ,
F2()
-> set ,
F3()
-> non
empty set ,
P1[
set ] } :
(
F1()
in F2() iff ex
a being
Element of
F3() st
(
F1()
= a &
P1[
a] ) )
provided
A1:
F2()
= { a where a is Element of F3() : P1[a] }
scheme
Fr4{
F1()
-> non
empty set ,
F2()
-> non
empty set ,
F3()
-> set ,
F4()
-> Element of
F1(),
F5(
set )
-> set ,
P1[
set ,
set ],
P2[
set ,
set ] } :
(
F4()
in F5(
F3()) iff for
b being
Element of
F2() st
b in F3() holds
P1[
F4(),
b] )
provided
A1:
F5(
F3())
= { a where a is Element of F1() : P2[a,F3()] }
and A2:
(
P2[
F4(),
F3()] iff for
b being
Element of
F2() st
b in F3() holds
P1[
F4(),
b] )
begin
Lm1:
for G being AbGroup
for a, b, c being Element of G holds
( - (a - b) = (- a) - (- b) & (a - b) + c = (a + c) - b )
theorem Th1:
theorem Th2:
theorem
theorem Th4:
theorem Th5:
theorem Th6:
begin
:: deftheorem Def1 defines SUBMODULE_DOMAIN LMOD_7:def 1 :
:: deftheorem defines LINE LMOD_7:def 2 :
:: deftheorem Def3 defines LINE_DOMAIN LMOD_7:def 3 :
:: deftheorem defines lines LMOD_7:def 4 :
:: deftheorem defines HIPERPLANE LMOD_7:def 5 :
:: deftheorem Def6 defines HIPERPLANE_DOMAIN LMOD_7:def 6 :
:: deftheorem defines hiperplanes LMOD_7:def 7 :
begin
:: deftheorem defines Sum LMOD_7:def 8 :
:: deftheorem defines /\ LMOD_7:def 9 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
begin
:: deftheorem defines + LMOD_7:def 10 :
for
K being
Ring for
V being
LeftMod of
K for
A1,
A2,
b5 being
Subset of
V holds
(
b5 = A1 + A2 iff for
x being
set holds
(
x in b5 iff ex
a1,
a2 being
Vector of
V st
(
a1 in A1 &
a2 in A2 &
x = a1 + a2 ) ) );
begin
:: deftheorem Def11 defines Vector LMOD_7:def 11 :
theorem
theorem Th17:
theorem Th18:
:: deftheorem Def12 defines .. LMOD_7:def 12 :
:: deftheorem defines .. LMOD_7:def 13 :
theorem Th19:
theorem
:: deftheorem defines - LMOD_7:def 14 :
:: deftheorem Def15 defines + LMOD_7:def 15 :
definition
let K be
Ring;
let V be
LeftMod of
K;
let W be
Subspace of
V;
deffunc H1(
Element of
V .. W)
-> Element of
V .. W =
- $1;
func COMPL W -> UnOp of
(V .. W) means
for
S1 being
Element of
V .. W holds
it . S1 = - S1;
existence
ex b1 being UnOp of (V .. W) st
for S1 being Element of V .. W holds b1 . S1 = - S1
uniqueness
for b1, b2 being UnOp of (V .. W) st ( for S1 being Element of V .. W holds b1 . S1 = - S1 ) & ( for S1 being Element of V .. W holds b2 . S1 = - S1 ) holds
b1 = b2
deffunc H2(
Element of
V .. W,
Element of
V .. W)
-> Element of
V .. W = $1
+ $2;
func ADD W -> BinOp of
(V .. W) means :
Def17:
for
S1,
S2 being
Element of
V .. W holds
it . S1,
S2 = S1 + S2;
existence
ex b1 being BinOp of (V .. W) st
for S1, S2 being Element of V .. W holds b1 . S1,S2 = S1 + S2
uniqueness
for b1, b2 being BinOp of (V .. W) st ( for S1, S2 being Element of V .. W holds b1 . S1,S2 = S1 + S2 ) & ( for S1, S2 being Element of V .. W holds b2 . S1,S2 = S1 + S2 ) holds
b1 = b2
end;
:: deftheorem defines COMPL LMOD_7:def 16 :
:: deftheorem Def17 defines ADD LMOD_7:def 17 :
:: deftheorem defines . LMOD_7:def 18 :
theorem
:: deftheorem defines . LMOD_7:def 19 :
theorem Th22:
theorem
theorem Th24:
:: deftheorem Def20 defines * LMOD_7:def 20 :
definition
let K be
Ring;
let V be
LeftMod of
K;
let W be
Subspace of
V;
func LMULT W -> Function of
[:the carrier of K,the carrier of (V . W):],the
carrier of
(V . W) means :
Def21:
for
r being
Scalar of
K for
S being
Element of
(V . W) holds
it . r,
S = r * S;
existence
ex b1 being Function of [:the carrier of K,the carrier of (V . W):],the carrier of (V . W) st
for r being Scalar of K
for S being Element of (V . W) holds b1 . r,S = r * S
uniqueness
for b1, b2 being Function of [:the carrier of K,the carrier of (V . W):],the carrier of (V . W) st ( for r being Scalar of K
for S being Element of (V . W) holds b1 . r,S = r * S ) & ( for r being Scalar of K
for S being Element of (V . W) holds b2 . r,S = r * S ) holds
b1 = b2
end;
:: deftheorem Def21 defines LMULT LMOD_7:def 21 :
begin
:: deftheorem defines / LMOD_7:def 22 :
theorem
canceled;
theorem
theorem
:: deftheorem defines / LMOD_7:def 23 :
theorem Th28:
theorem
theorem Th30:
Lm2:
for K being Ring
for V being LeftMod of K
for W being Subspace of V holds
( V / W is Abelian & V / W is add-associative & V / W is right_zeroed & V / W is right_complementable )
theorem Th31: