:: by Katarzyna Zawadzka

::

:: Received December 29, 1992

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

begin

registration
end;

registration
end;

registration
end;

theorem :: FVSUM_1:9

theorem Th10: :: FVSUM_1:10

for K being non empty distributive doubleLoopStr holds the multF of K is_distributive_wrt the addF of K

proof end;

definition

let K be non empty multMagma ;

let a be Element of K;

the multF of K [;] (a,(id the carrier of K)) is UnOp of the carrier of K ;

end;
let a be Element of K;

func a multfield -> UnOp of the carrier of K equals :: FVSUM_1:def 1

the multF of K [;] (a,(id the carrier of K));

coherence the multF of K [;] (a,(id the carrier of K));

the multF of K [;] (a,(id the carrier of K)) is UnOp of the carrier of K ;

:: deftheorem defines multfield FVSUM_1:def 1 :

for K being non empty multMagma

for a being Element of K holds a multfield = the multF of K [;] (a,(id the carrier of K));

for K being non empty multMagma

for a being Element of K holds a multfield = the multF of K [;] (a,(id the carrier of K));

definition

let K be non empty addLoopStr ;

coherence

the addF of K * ((id the carrier of K),(comp K)) is BinOp of the carrier of K;

;

end;
func diffield K -> BinOp of the carrier of K equals :: FVSUM_1:def 2

the addF of K * ((id the carrier of K),(comp K));

correctness the addF of K * ((id the carrier of K),(comp K));

coherence

the addF of K * ((id the carrier of K),(comp K)) is BinOp of the carrier of K;

;

:: deftheorem defines diffield FVSUM_1:def 2 :

for K being non empty addLoopStr holds diffield K = the addF of K * ((id the carrier of K),(comp K));

for K being non empty addLoopStr holds diffield K = the addF of K * ((id the carrier of K),(comp K));

theorem Th11: :: FVSUM_1:11

for K being non empty addLoopStr

for a1, a2 being Element of K holds (diffield K) . (a1,a2) = a1 - a2

for a1, a2 being Element of K holds (diffield K) . (a1,a2) = a1 - a2

proof end;

Lm1: for K being non empty multMagma

for a, b being Element of K holds ( the multF of K [;] (b,(id the carrier of K))) . a = b * a

proof end;

theorem Th12: :: FVSUM_1:12

for K being non empty distributive doubleLoopStr

for a being Element of K holds a multfield is_distributive_wrt the addF of K by Th10, FINSEQOP:54;

for a being Element of K holds a multfield is_distributive_wrt the addF of K by Th10, FINSEQOP:54;

theorem Th13: :: FVSUM_1:13

for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr holds comp K is_an_inverseOp_wrt the addF of K

proof end;

theorem Th14: :: FVSUM_1:14

for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr holds the addF of K is having_an_inverseOp

proof end;

theorem Th15: :: FVSUM_1:15

for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr holds the_inverseOp_wrt the addF of K = comp K

proof end;

theorem :: FVSUM_1:16

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds comp K is_distributive_wrt the addF of K

proof end;

begin

definition

let K be non empty addLoopStr ;

let p1, p2 be FinSequence of the carrier of K;

correctness

coherence

the addF of K .: (p1,p2) is FinSequence of the carrier of K;

;

end;
let p1, p2 be FinSequence of the carrier of K;

correctness

coherence

the addF of K .: (p1,p2) is FinSequence of the carrier of K;

;

:: deftheorem defines + FVSUM_1:def 3 :

for K being non empty addLoopStr

for p1, p2 being FinSequence of the carrier of K holds p1 + p2 = the addF of K .: (p1,p2);

for K being non empty addLoopStr

for p1, p2 being FinSequence of the carrier of K holds p1 + p2 = the addF of K .: (p1,p2);

theorem :: FVSUM_1:17

definition

let i be Element of NAT ;

let K be non empty addLoopStr ;

let R1, R2 be Element of i -tuples_on the carrier of K;

:: original: +

redefine func R1 + R2 -> Element of i -tuples_on the carrier of K;

coherence

R1 + R2 is Element of i -tuples_on the carrier of K by FINSEQ_2:120;

end;
let K be non empty addLoopStr ;

let R1, R2 be Element of i -tuples_on the carrier of K;

:: original: +

redefine func R1 + R2 -> Element of i -tuples_on the carrier of K;

coherence

R1 + R2 is Element of i -tuples_on the carrier of K by FINSEQ_2:120;

theorem :: FVSUM_1:18

for i, j being Element of NAT

for K being non empty addLoopStr

for a1, a2 being Element of K

for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds

(R1 + R2) . j = a1 + a2

for K being non empty addLoopStr

for a1, a2 being Element of K

for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds

(R1 + R2) . j = a1 + a2

proof end;

theorem :: FVSUM_1:19

theorem :: FVSUM_1:20

Lm2: for i being Element of NAT

for K being non empty left_zeroed right_zeroed addLoopStr

for R being Element of i -tuples_on the carrier of K holds R + (i |-> (0. K)) = R

proof end;

theorem Th21: :: FVSUM_1:21

for i being Element of NAT

for K being non empty left_zeroed Abelian right_zeroed addLoopStr

for R being Element of i -tuples_on the carrier of K holds

( R + (i |-> (0. K)) = R & R = (i |-> (0. K)) + R )

for K being non empty left_zeroed Abelian right_zeroed addLoopStr

for R being Element of i -tuples_on the carrier of K holds

( R + (i |-> (0. K)) = R & R = (i |-> (0. K)) + R )

proof end;

definition

let K be non empty addLoopStr ;

let p be FinSequence of the carrier of K;

correctness

coherence

(comp K) * p is FinSequence of the carrier of K;

;

end;
let p be FinSequence of the carrier of K;

correctness

coherence

(comp K) * p is FinSequence of the carrier of K;

;

:: deftheorem defines - FVSUM_1:def 4 :

for K being non empty addLoopStr

for p being FinSequence of the carrier of K holds - p = (comp K) * p;

for K being non empty addLoopStr

for p being FinSequence of the carrier of K holds - p = (comp K) * p;

theorem Th22: :: FVSUM_1:22

for i being Element of NAT

for K being non empty addLoopStr

for a being Element of K

for p being FinSequence of the carrier of K st i in dom (- p) & a = p . i holds

(- p) . i = - a

for K being non empty addLoopStr

for a being Element of K

for p being FinSequence of the carrier of K st i in dom (- p) & a = p . i holds

(- p) . i = - a

proof end;

definition

let i be Element of NAT ;

let K be non empty addLoopStr ;

let R be Element of i -tuples_on the carrier of K;

:: original: -

redefine func - R -> Element of i -tuples_on the carrier of K;

coherence

- R is Element of i -tuples_on the carrier of K by FINSEQ_2:113;

end;
let K be non empty addLoopStr ;

let R be Element of i -tuples_on the carrier of K;

:: original: -

redefine func - R -> Element of i -tuples_on the carrier of K;

coherence

- R is Element of i -tuples_on the carrier of K by FINSEQ_2:113;

theorem :: FVSUM_1:23

for j, i being Element of NAT

for K being non empty addLoopStr

for a being Element of K

for R being Element of i -tuples_on the carrier of K st j in Seg i & a = R . j holds

(- R) . j = - a

for K being non empty addLoopStr

for a being Element of K

for R being Element of i -tuples_on the carrier of K st j in Seg i & a = R . j holds

(- R) . j = - a

proof end;

theorem Th25: :: FVSUM_1:25

for i being Element of NAT

for K being non empty addLoopStr

for a being Element of K holds - (i |-> a) = i |-> (- a)

for K being non empty addLoopStr

for a being Element of K holds - (i |-> a) = i |-> (- a)

proof end;

Lm3: for i being Element of NAT

for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr

for R being Element of i -tuples_on the carrier of K holds R + (- R) = i |-> (0. K)

proof end;

theorem Th26: :: FVSUM_1:26

for i being Element of NAT

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R being Element of i -tuples_on the carrier of K holds

( R + (- R) = i |-> (0. K) & (- R) + R = i |-> (0. K) )

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R being Element of i -tuples_on the carrier of K holds

( R + (- R) = i |-> (0. K) & (- R) + R = i |-> (0. K) )

proof end;

theorem Th27: :: FVSUM_1:27

for i being Element of NAT

for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K st R1 + R2 = i |-> (0. K) holds

( R1 = - R2 & R2 = - R1 )

for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K st R1 + R2 = i |-> (0. K) holds

( R1 = - R2 & R2 = - R1 )

proof end;

theorem Th28: :: FVSUM_1:28

for i being Element of NAT

for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr

for R being Element of i -tuples_on the carrier of K holds - (- R) = R

for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr

for R being Element of i -tuples_on the carrier of K holds - (- R) = R

proof end;

theorem :: FVSUM_1:29

for i being Element of NAT

for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K st - R1 = - R2 holds

R1 = R2

for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K st - R1 = - R2 holds

R1 = R2

proof end;

Lm4: for i being Element of NAT

for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr

for R1, R, R2 being Element of i -tuples_on the carrier of K st R1 + R = R2 + R holds

R1 = R2

proof end;

theorem :: FVSUM_1:30

for i being Element of NAT

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R, R1, R2 being Element of i -tuples_on the carrier of K st ( R1 + R = R2 + R or R1 + R = R + R2 ) holds

R1 = R2

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R, R1, R2 being Element of i -tuples_on the carrier of K st ( R1 + R = R2 + R or R1 + R = R + R2 ) holds

R1 = R2

proof end;

theorem Th31: :: FVSUM_1:31

for i being Element of NAT

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 + R2) = (- R1) + (- R2)

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 + R2) = (- R1) + (- R2)

proof end;

definition

let K be non empty addLoopStr ;

let p1, p2 be FinSequence of the carrier of K;

correctness

coherence

(diffield K) .: (p1,p2) is FinSequence of the carrier of K;

;

end;
let p1, p2 be FinSequence of the carrier of K;

correctness

coherence

(diffield K) .: (p1,p2) is FinSequence of the carrier of K;

;

:: deftheorem defines - FVSUM_1:def 5 :

for K being non empty addLoopStr

for p1, p2 being FinSequence of the carrier of K holds p1 - p2 = (diffield K) .: (p1,p2);

for K being non empty addLoopStr

for p1, p2 being FinSequence of the carrier of K holds p1 - p2 = (diffield K) .: (p1,p2);

theorem Th32: :: FVSUM_1:32

for i being Element of NAT

for K being non empty addLoopStr

for a1, a2 being Element of K

for p1, p2 being FinSequence of the carrier of K st i in dom (p1 - p2) & a1 = p1 . i & a2 = p2 . i holds

(p1 - p2) . i = a1 - a2

for K being non empty addLoopStr

for a1, a2 being Element of K

for p1, p2 being FinSequence of the carrier of K st i in dom (p1 - p2) & a1 = p1 . i & a2 = p2 . i holds

(p1 - p2) . i = a1 - a2

proof end;

definition

let i be Element of NAT ;

let K be non empty addLoopStr ;

let R1, R2 be Element of i -tuples_on the carrier of K;

:: original: -

redefine func R1 - R2 -> Element of i -tuples_on the carrier of K;

coherence

R1 - R2 is Element of i -tuples_on the carrier of K by FINSEQ_2:120;

end;
let K be non empty addLoopStr ;

let R1, R2 be Element of i -tuples_on the carrier of K;

:: original: -

redefine func R1 - R2 -> Element of i -tuples_on the carrier of K;

coherence

R1 - R2 is Element of i -tuples_on the carrier of K by FINSEQ_2:120;

theorem :: FVSUM_1:33

for j, i being Element of NAT

for K being non empty addLoopStr

for a1, a2 being Element of K

for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds

(R1 - R2) . j = a1 - a2

for K being non empty addLoopStr

for a1, a2 being Element of K

for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds

(R1 - R2) . j = a1 - a2

proof end;

theorem :: FVSUM_1:34

for K being non empty addLoopStr

for a1, a2 being Element of K holds <*a1*> - <*a2*> = <*(a1 - a2)*>

for a1, a2 being Element of K holds <*a1*> - <*a2*> = <*(a1 - a2)*>

proof end;

theorem :: FVSUM_1:35

for i being Element of NAT

for K being non empty addLoopStr

for a1, a2 being Element of K holds (i |-> a1) - (i |-> a2) = i |-> (a1 - a2)

for K being non empty addLoopStr

for a1, a2 being Element of K holds (i |-> a1) - (i |-> a2) = i |-> (a1 - a2)

proof end;

theorem :: FVSUM_1:36

for i being Element of NAT

for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr

for R being Element of i -tuples_on the carrier of K holds R - (i |-> (0. K)) = R

for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr

for R being Element of i -tuples_on the carrier of K holds R - (i |-> (0. K)) = R

proof end;

theorem :: FVSUM_1:37

for i being Element of NAT

for K being non empty left_zeroed Abelian right_zeroed addLoopStr

for R being Element of i -tuples_on the carrier of K holds (i |-> (0. K)) - R = - R

for K being non empty left_zeroed Abelian right_zeroed addLoopStr

for R being Element of i -tuples_on the carrier of K holds (i |-> (0. K)) - R = - R

proof end;

theorem :: FVSUM_1:38

for i being Element of NAT

for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K holds R1 - (- R2) = R1 + R2

for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K holds R1 - (- R2) = R1 + R2

proof end;

theorem :: FVSUM_1:39

for i being Element of NAT

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = R2 - R1

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = R2 - R1

proof end;

theorem Th40: :: FVSUM_1:40

for i being Element of NAT

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = (- R1) + R2

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = (- R1) + R2

proof end;

theorem Th41: :: FVSUM_1:41

for i being Element of NAT

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R being Element of i -tuples_on the carrier of K holds R - R = i |-> (0. K)

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R being Element of i -tuples_on the carrier of K holds R - R = i |-> (0. K)

proof end;

theorem :: FVSUM_1:42

for i being Element of NAT

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K st R1 - R2 = i |-> (0. K) holds

R1 = R2

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K st R1 - R2 = i |-> (0. K) holds

R1 = R2

proof end;

theorem :: FVSUM_1:43

for i being Element of NAT

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R2, R3 being Element of i -tuples_on the carrier of K holds (R1 - R2) - R3 = R1 - (R2 + R3)

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R2, R3 being Element of i -tuples_on the carrier of K holds (R1 - R2) - R3 = R1 - (R2 + R3)

proof end;

theorem Th44: :: FVSUM_1:44

for i being Element of NAT

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R2, R3 being Element of i -tuples_on the carrier of K holds R1 + (R2 - R3) = (R1 + R2) - R3

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R2, R3 being Element of i -tuples_on the carrier of K holds R1 + (R2 - R3) = (R1 + R2) - R3

proof end;

theorem :: FVSUM_1:45

for i being Element of NAT

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R2, R3 being Element of i -tuples_on the carrier of K holds R1 - (R2 - R3) = (R1 - R2) + R3

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R2, R3 being Element of i -tuples_on the carrier of K holds R1 - (R2 - R3) = (R1 - R2) + R3

proof end;

theorem :: FVSUM_1:46

for i being Element of NAT

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R being Element of i -tuples_on the carrier of K holds R1 = (R1 + R) - R

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R being Element of i -tuples_on the carrier of K holds R1 = (R1 + R) - R

proof end;

theorem :: FVSUM_1:47

for i being Element of NAT

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R being Element of i -tuples_on the carrier of K holds R1 = (R1 - R) + R

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R being Element of i -tuples_on the carrier of K holds R1 = (R1 - R) + R

proof end;

theorem Th48: :: FVSUM_1:48

for K being non empty multMagma

for a, b being Element of K holds ( the multF of K [;] (a,(id the carrier of K))) . b = a * b

for a, b being Element of K holds ( the multF of K [;] (a,(id the carrier of K))) . b = a * b

proof end;

theorem :: FVSUM_1:49

definition

let K be non empty multMagma ;

let p be FinSequence of the carrier of K;

let a be Element of K;

correctness

coherence

(a multfield) * p is FinSequence of the carrier of K;

;

end;
let p be FinSequence of the carrier of K;

let a be Element of K;

correctness

coherence

(a multfield) * p is FinSequence of the carrier of K;

;

:: deftheorem defines * FVSUM_1:def 6 :

for K being non empty multMagma

for p being FinSequence of the carrier of K

for a being Element of K holds a * p = (a multfield) * p;

for K being non empty multMagma

for p being FinSequence of the carrier of K

for a being Element of K holds a * p = (a multfield) * p;

theorem Th50: :: FVSUM_1:50

for i being Element of NAT

for K being non empty multMagma

for a, a9 being Element of K

for p being FinSequence of the carrier of K st i in dom (a * p) & a9 = p . i holds

(a * p) . i = a * a9

for K being non empty multMagma

for a, a9 being Element of K

for p being FinSequence of the carrier of K st i in dom (a * p) & a9 = p . i holds

(a * p) . i = a * a9

proof end;

definition

let i be Element of NAT ;

let K be non empty multMagma ;

let R be Element of i -tuples_on the carrier of K;

let a be Element of K;

:: original: *

redefine func a * R -> Element of i -tuples_on the carrier of K;

coherence

a * R is Element of i -tuples_on the carrier of K by FINSEQ_2:113;

end;
let K be non empty multMagma ;

let R be Element of i -tuples_on the carrier of K;

let a be Element of K;

:: original: *

redefine func a * R -> Element of i -tuples_on the carrier of K;

coherence

a * R is Element of i -tuples_on the carrier of K by FINSEQ_2:113;

theorem :: FVSUM_1:51

for j, i being Element of NAT

for K being non empty multMagma

for a9, a being Element of K

for R being Element of i -tuples_on the carrier of K st j in Seg i & a9 = R . j holds

(a * R) . j = a * a9

for K being non empty multMagma

for a9, a being Element of K

for R being Element of i -tuples_on the carrier of K st j in Seg i & a9 = R . j holds

(a * R) . j = a * a9

proof end;

theorem Th53: :: FVSUM_1:53

for i being Element of NAT

for K being non empty multMagma

for a1, a2 being Element of K holds a1 * (i |-> a2) = i |-> (a1 * a2)

for K being non empty multMagma

for a1, a2 being Element of K holds a1 * (i |-> a2) = i |-> (a1 * a2)

proof end;

theorem :: FVSUM_1:54

for i being Element of NAT

for K being non empty associative multMagma

for a1, a2 being Element of K

for R being Element of i -tuples_on the carrier of K holds (a1 * a2) * R = a1 * (a2 * R)

for K being non empty associative multMagma

for a1, a2 being Element of K

for R being Element of i -tuples_on the carrier of K holds (a1 * a2) * R = a1 * (a2 * R)

proof end;

theorem :: FVSUM_1:55

for i being Element of NAT

for K being non empty distributive doubleLoopStr

for a1, a2 being Element of K

for R being Element of i -tuples_on the carrier of K holds (a1 + a2) * R = (a1 * R) + (a2 * R)

for K being non empty distributive doubleLoopStr

for a1, a2 being Element of K

for R being Element of i -tuples_on the carrier of K holds (a1 + a2) * R = (a1 * R) + (a2 * R)

proof end;

theorem :: FVSUM_1:56

for i being Element of NAT

for K being non empty distributive doubleLoopStr

for a being Element of K

for R1, R2 being Element of i -tuples_on the carrier of K holds a * (R1 + R2) = (a * R1) + (a * R2) by Th12, FINSEQOP:51;

for K being non empty distributive doubleLoopStr

for a being Element of K

for R1, R2 being Element of i -tuples_on the carrier of K holds a * (R1 + R2) = (a * R1) + (a * R2) by Th12, FINSEQOP:51;

theorem :: FVSUM_1:57

for i being Element of NAT

for K being non empty commutative distributive left_unital doubleLoopStr

for R being Element of i -tuples_on the carrier of K holds (1. K) * R = R

for K being non empty commutative distributive left_unital doubleLoopStr

for R being Element of i -tuples_on the carrier of K holds (1. K) * R = R

proof end;

theorem :: FVSUM_1:58

for i being Element of NAT

for K being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr

for R being Element of i -tuples_on the carrier of K holds (0. K) * R = i |-> (0. K)

for K being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr

for R being Element of i -tuples_on the carrier of K holds (0. K) * R = i |-> (0. K)

proof end;

theorem :: FVSUM_1:59

for i being Element of NAT

for K being non empty right_complementable commutative add-associative right_zeroed distributive left_unital doubleLoopStr

for R being Element of i -tuples_on the carrier of K holds (- (1. K)) * R = - R

for K being non empty right_complementable commutative add-associative right_zeroed distributive left_unital doubleLoopStr

for R being Element of i -tuples_on the carrier of K holds (- (1. K)) * R = - R

proof end;

definition

let M be non empty multMagma ;

let p1, p2 be FinSequence of the carrier of M;

coherence

the multF of M .: (p1,p2) is FinSequence of the carrier of M;

;

end;
let p1, p2 be FinSequence of the carrier of M;

func mlt (p1,p2) -> FinSequence of the carrier of M equals :: FVSUM_1:def 7

the multF of M .: (p1,p2);

correctness the multF of M .: (p1,p2);

coherence

the multF of M .: (p1,p2) is FinSequence of the carrier of M;

;

:: deftheorem defines mlt FVSUM_1:def 7 :

for M being non empty multMagma

for p1, p2 being FinSequence of the carrier of M holds mlt (p1,p2) = the multF of M .: (p1,p2);

for M being non empty multMagma

for p1, p2 being FinSequence of the carrier of M holds mlt (p1,p2) = the multF of M .: (p1,p2);

theorem :: FVSUM_1:60

definition

let i be Element of NAT ;

let K be non empty multMagma ;

let R1, R2 be Element of i -tuples_on the carrier of K;

:: original: mlt

redefine func mlt (R1,R2) -> Element of i -tuples_on the carrier of K;

coherence

mlt (R1,R2) is Element of i -tuples_on the carrier of K by FINSEQ_2:120;

end;
let K be non empty multMagma ;

let R1, R2 be Element of i -tuples_on the carrier of K;

:: original: mlt

redefine func mlt (R1,R2) -> Element of i -tuples_on the carrier of K;

coherence

mlt (R1,R2) is Element of i -tuples_on the carrier of K by FINSEQ_2:120;

theorem :: FVSUM_1:61

for j, i being Element of NAT

for K being non empty multMagma

for a1, a2 being Element of K

for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds

(mlt (R1,R2)) . j = a1 * a2

for K being non empty multMagma

for a1, a2 being Element of K

for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds

(mlt (R1,R2)) . j = a1 * a2

proof end;

theorem :: FVSUM_1:62

Lm5: for K being non empty multMagma

for a1, a2, b1, b2 being Element of K holds mlt (<*a1,a2*>,<*b1,b2*>) = <*(a1 * b1),(a2 * b2)*>

proof end;

theorem :: FVSUM_1:63

for i being Element of NAT

for K being non empty commutative multMagma

for R1, R2 being Element of i -tuples_on the carrier of K holds mlt (R1,R2) = mlt (R2,R1) by FINSEQOP:33;

for K being non empty commutative multMagma

for R1, R2 being Element of i -tuples_on the carrier of K holds mlt (R1,R2) = mlt (R2,R1) by FINSEQOP:33;

theorem Th64: :: FVSUM_1:64

for K being non empty commutative multMagma

for p, q being FinSequence of the carrier of K holds mlt (p,q) = mlt (q,p)

for p, q being FinSequence of the carrier of K holds mlt (p,q) = mlt (q,p)

proof end;

theorem :: FVSUM_1:65

for i being Element of NAT

for K being non empty associative multMagma

for R1, R2, R3 being Element of i -tuples_on the carrier of K holds mlt (R1,(mlt (R2,R3))) = mlt ((mlt (R1,R2)),R3) by FINSEQOP:28;

for K being non empty associative multMagma

for R1, R2, R3 being Element of i -tuples_on the carrier of K holds mlt (R1,(mlt (R2,R3))) = mlt ((mlt (R1,R2)),R3) by FINSEQOP:28;

theorem Th66: :: FVSUM_1:66

for i being Element of NAT

for K being non empty associative commutative multMagma

for a being Element of K

for R being Element of i -tuples_on the carrier of K holds

( mlt ((i |-> a),R) = a * R & mlt (R,(i |-> a)) = a * R )

for K being non empty associative commutative multMagma

for a being Element of K

for R being Element of i -tuples_on the carrier of K holds

( mlt ((i |-> a),R) = a * R & mlt (R,(i |-> a)) = a * R )

proof end;

theorem :: FVSUM_1:67

for i being Element of NAT

for K being non empty associative commutative multMagma

for a1, a2 being Element of K holds mlt ((i |-> a1),(i |-> a2)) = i |-> (a1 * a2)

for K being non empty associative commutative multMagma

for a1, a2 being Element of K holds mlt ((i |-> a1),(i |-> a2)) = i |-> (a1 * a2)

proof end;

theorem :: FVSUM_1:68

for i being Element of NAT

for K being non empty associative multMagma

for a being Element of K

for R1, R2 being Element of i -tuples_on the carrier of K holds a * (mlt (R1,R2)) = mlt ((a * R1),R2) by FINSEQOP:26;

for K being non empty associative multMagma

for a being Element of K

for R1, R2 being Element of i -tuples_on the carrier of K holds a * (mlt (R1,R2)) = mlt ((a * R1),R2) by FINSEQOP:26;

theorem :: FVSUM_1:69

for i being Element of NAT

for K being non empty associative commutative multMagma

for a being Element of K

for R1, R2 being Element of i -tuples_on the carrier of K holds

( a * (mlt (R1,R2)) = mlt ((a * R1),R2) & a * (mlt (R1,R2)) = mlt (R1,(a * R2)) )

for K being non empty associative commutative multMagma

for a being Element of K

for R1, R2 being Element of i -tuples_on the carrier of K holds

( a * (mlt (R1,R2)) = mlt ((a * R1),R2) & a * (mlt (R1,R2)) = mlt (R1,(a * R2)) )

proof end;

theorem :: FVSUM_1:70

for i being Element of NAT

for K being non empty associative commutative multMagma

for a being Element of K

for R being Element of i -tuples_on the carrier of K holds a * R = mlt ((i |-> a),R) by Th66;

for K being non empty associative commutative multMagma

for a being Element of K

for R being Element of i -tuples_on the carrier of K holds a * R = mlt ((i |-> a),R) by Th66;

begin

::

::The Sum of Finite Number of Elements

::

::The Sum of Finite Number of Elements

::

registration

coherence

for b_{1} being non empty addLoopStr st b_{1} is Abelian & b_{1} is right_zeroed holds

b_{1} is left_zeroed

end;
for b

b

proof end;

definition

let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;

let p be FinSequence of the carrier of K;

compatibility

for b_{1} being Element of the carrier of K holds

( b_{1} = Sum p iff b_{1} = the addF of K $$ p )

end;
let p be FinSequence of the carrier of K;

compatibility

for b

( b

proof end;

:: deftheorem defines Sum FVSUM_1:def 8 :

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for p being FinSequence of the carrier of K holds Sum p = the addF of K $$ p;

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for p being FinSequence of the carrier of K holds Sum p = the addF of K $$ p;

theorem :: FVSUM_1:71

for K being non empty right_complementable add-associative right_zeroed addLoopStr

for a being Element of K

for p being FinSequence of the carrier of K holds Sum (p ^ <*a*>) = (Sum p) + a

for a being Element of K

for p being FinSequence of the carrier of K holds Sum (p ^ <*a*>) = (Sum p) + a

proof end;

theorem :: FVSUM_1:72

for K being non empty right_complementable add-associative right_zeroed addLoopStr

for a being Element of K

for p being FinSequence of the carrier of K holds Sum (<*a*> ^ p) = a + (Sum p)

for a being Element of K

for p being FinSequence of the carrier of K holds Sum (<*a*> ^ p) = a + (Sum p)

proof end;

theorem :: FVSUM_1:73

for K being non empty right_complementable Abelian add-associative right_zeroed distributive doubleLoopStr

for a being Element of K

for p being FinSequence of the carrier of K holds Sum (a * p) = a * (Sum p)

for a being Element of K

for p being FinSequence of the carrier of K holds Sum (a * p) = a * (Sum p)

proof end;

theorem :: FVSUM_1:74

for K being non empty addLoopStr

for R being Element of 0 -tuples_on the carrier of K holds Sum R = 0. K

for R being Element of 0 -tuples_on the carrier of K holds Sum R = 0. K

proof end;

theorem :: FVSUM_1:75

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for p being FinSequence of the carrier of K holds Sum (- p) = - (Sum p)

for p being FinSequence of the carrier of K holds Sum (- p) = - (Sum p)

proof end;

theorem :: FVSUM_1:76

for i being Element of NAT

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K holds Sum (R1 + R2) = (Sum R1) + (Sum R2) by Th8, SETWOP_2:35;

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K holds Sum (R1 + R2) = (Sum R1) + (Sum R2) by Th8, SETWOP_2:35;

theorem :: FVSUM_1:77

for i being Element of NAT

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K holds Sum (R1 - R2) = (Sum R1) - (Sum R2)

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K holds Sum (R1 - R2) = (Sum R1) - (Sum R2)

proof end;

begin

Lm6: for K being non empty commutative well-unital multLoopStr holds Product (<*> the carrier of K) = 1. K

proof end;

theorem :: FVSUM_1:78

for K being non empty associative commutative well-unital doubleLoopStr

for a being Element of K

for p1 being FinSequence of the carrier of K holds Product (<*a*> ^ p1) = a * (Product p1)

for a being Element of K

for p1 being FinSequence of the carrier of K holds Product (<*a*> ^ p1) = a * (Product p1)

proof end;

theorem :: FVSUM_1:79

for K being non empty associative commutative well-unital doubleLoopStr

for a1, a2, a3 being Element of K holds Product <*a1,a2,a3*> = (a1 * a2) * a3

for a1, a2, a3 being Element of K holds Product <*a1,a2,a3*> = (a1 * a2) * a3

proof end;

theorem :: FVSUM_1:80

for K being non empty associative commutative well-unital doubleLoopStr

for R being Element of 0 -tuples_on the carrier of K holds Product R = 1. K

for R being Element of 0 -tuples_on the carrier of K holds Product R = 1. K

proof end;

theorem :: FVSUM_1:81

for i being Element of NAT

for K being non empty associative commutative well-unital doubleLoopStr holds Product (i |-> (1_ K)) = 1_ K

for K being non empty associative commutative well-unital doubleLoopStr holds Product (i |-> (1_ K)) = 1_ K

proof end;

theorem :: FVSUM_1:82

for K being non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for p being FinSequence of the carrier of K holds

( ex k being Element of NAT st

( k in dom p & p . k = 0. K ) iff Product p = 0. K )

for p being FinSequence of the carrier of K holds

( ex k being Element of NAT st

( k in dom p & p . k = 0. K ) iff Product p = 0. K )

proof end;

theorem :: FVSUM_1:83

for i, j being Element of NAT

for K being non empty associative commutative well-unital doubleLoopStr

for a being Element of K holds Product ((i + j) |-> a) = (Product (i |-> a)) * (Product (j |-> a)) by SETWOP_2:26;

for K being non empty associative commutative well-unital doubleLoopStr

for a being Element of K holds Product ((i + j) |-> a) = (Product (i |-> a)) * (Product (j |-> a)) by SETWOP_2:26;

theorem :: FVSUM_1:84

for i, j being Element of NAT

for K being non empty associative commutative well-unital doubleLoopStr

for a being Element of K holds Product ((i * j) |-> a) = Product (j |-> (Product (i |-> a))) by SETWOP_2:27;

for K being non empty associative commutative well-unital doubleLoopStr

for a being Element of K holds Product ((i * j) |-> a) = Product (j |-> (Product (i |-> a))) by SETWOP_2:27;

theorem :: FVSUM_1:85

for i being Element of NAT

for K being non empty associative commutative well-unital doubleLoopStr

for a1, a2 being Element of K holds Product (i |-> (a1 * a2)) = (Product (i |-> a1)) * (Product (i |-> a2)) by SETWOP_2:36;

for K being non empty associative commutative well-unital doubleLoopStr

for a1, a2 being Element of K holds Product (i |-> (a1 * a2)) = (Product (i |-> a1)) * (Product (i |-> a2)) by SETWOP_2:36;

theorem Th86: :: FVSUM_1:86

for i being Element of NAT

for K being non empty associative commutative well-unital doubleLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K holds Product (mlt (R1,R2)) = (Product R1) * (Product R2) by SETWOP_2:35;

for K being non empty associative commutative well-unital doubleLoopStr

for R1, R2 being Element of i -tuples_on the carrier of K holds Product (mlt (R1,R2)) = (Product R1) * (Product R2) by SETWOP_2:35;

theorem :: FVSUM_1:87

for i being Element of NAT

for K being non empty associative commutative well-unital doubleLoopStr

for a being Element of K

for R1 being Element of i -tuples_on the carrier of K holds Product (a * R1) = (Product (i |-> a)) * (Product R1)

for K being non empty associative commutative well-unital doubleLoopStr

for a being Element of K

for R1 being Element of i -tuples_on the carrier of K holds Product (a * R1) = (Product (i |-> a)) * (Product R1)

proof end;

begin

definition

let K be non empty doubleLoopStr ;

let p, q be FinSequence of the carrier of K;

coherence

Sum (mlt (p,q)) is Element of K ;

end;
let p, q be FinSequence of the carrier of K;

coherence

Sum (mlt (p,q)) is Element of K ;

:: deftheorem defines "*" FVSUM_1:def 9 :

for K being non empty doubleLoopStr

for p, q being FinSequence of the carrier of K holds p "*" q = Sum (mlt (p,q));

for K being non empty doubleLoopStr

for p, q being FinSequence of the carrier of K holds p "*" q = Sum (mlt (p,q));

theorem :: FVSUM_1:88

for K being non empty right_complementable associative commutative Abelian add-associative right_zeroed left_unital doubleLoopStr

for a, b being Element of K holds <*a*> "*" <*b*> = a * b

for a, b being Element of K holds <*a*> "*" <*b*> = a * b

proof end;

theorem :: FVSUM_1:89

for K being non empty right_complementable associative commutative Abelian add-associative right_zeroed left_unital doubleLoopStr

for a1, a2, b1, b2 being Element of K holds <*a1,a2*> "*" <*b1,b2*> = (a1 * b1) + (a2 * b2)

for a1, a2, b1, b2 being Element of K holds <*a1,a2*> "*" <*b1,b2*> = (a1 * b1) + (a2 * b2)

proof end;

theorem :: FVSUM_1:90

for K being non empty associative commutative well-unital doubleLoopStr

for p, q being FinSequence of the carrier of K holds p "*" q = q "*" p by Th64;

for p, q being FinSequence of the carrier of K holds p "*" q = q "*" p by Th64;

:: Some Operations on the i-tuples on Element of K

::