:: Sum and Product of Finite Sequences of Elements of a Field
:: by Katarzyna Zawadzka
::
:: Received December 29, 1992
:: Copyright (c) 1992 Association of Mizar Users
theorem :: FVSUM_1:1
canceled;
theorem Th2: :: FVSUM_1:2
theorem Th3: :: FVSUM_1:3
theorem Th4: :: FVSUM_1:4
theorem :: FVSUM_1:5
canceled;
theorem Th6: :: FVSUM_1:6
theorem Th7: :: FVSUM_1:7
theorem Th8: :: FVSUM_1:8
theorem Th9: :: FVSUM_1:9
theorem Th10: :: FVSUM_1:10
theorem Th11: :: FVSUM_1:11
theorem Th12: :: FVSUM_1:12
:: deftheorem defines multfield FVSUM_1:def 1 :
:: deftheorem defines diffield FVSUM_1:def 2 :
theorem :: FVSUM_1:13
canceled;
theorem Th14: :: FVSUM_1:14
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
theorem Th15: :: FVSUM_1:15
theorem Th16: :: FVSUM_1:16
theorem Th17: :: FVSUM_1:17
theorem Th18: :: FVSUM_1:18
theorem :: FVSUM_1:19
:: deftheorem defines + FVSUM_1:def 3 :
theorem :: FVSUM_1:20
canceled;
theorem :: FVSUM_1:21
theorem :: FVSUM_1:22
theorem :: FVSUM_1:23
canceled;
theorem :: FVSUM_1:24
theorem :: FVSUM_1:25
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
theorem :: FVSUM_1:26
canceled;
theorem :: FVSUM_1:27
canceled;
theorem Th28: :: FVSUM_1:28
:: deftheorem defines - FVSUM_1:def 4 :
theorem :: FVSUM_1:29
canceled;
theorem Th30: :: FVSUM_1:30
theorem :: FVSUM_1:31
theorem :: FVSUM_1:32
canceled;
theorem :: FVSUM_1:33
theorem Th34: :: FVSUM_1:34
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)
theorem Th35: :: FVSUM_1:35
theorem Th36: :: FVSUM_1:36
theorem Th37: :: FVSUM_1:37
theorem :: FVSUM_1:38
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
theorem :: FVSUM_1:39
theorem Th40: :: FVSUM_1:40
:: deftheorem defines - FVSUM_1:def 5 :
theorem :: FVSUM_1:41
canceled;
theorem Th42: :: FVSUM_1:42
theorem :: FVSUM_1:43
theorem :: FVSUM_1:44
canceled;
theorem :: FVSUM_1:45
theorem :: FVSUM_1:46
theorem :: FVSUM_1:47
canceled;
theorem :: FVSUM_1:48
theorem :: FVSUM_1:49
theorem :: FVSUM_1:50
theorem :: FVSUM_1:51
theorem Th52: :: FVSUM_1:52
theorem Th53: :: FVSUM_1:53
theorem :: FVSUM_1:54
theorem :: FVSUM_1:55
theorem Th56: :: FVSUM_1:56
theorem :: FVSUM_1:57
theorem :: FVSUM_1:58
theorem :: FVSUM_1:59
theorem Th60: :: FVSUM_1:60
theorem :: FVSUM_1:61
:: deftheorem defines * FVSUM_1:def 6 :
theorem Th62: :: FVSUM_1:62
theorem :: FVSUM_1:63
theorem :: FVSUM_1:64
canceled;
theorem :: FVSUM_1:65
theorem Th66: :: FVSUM_1:66
theorem :: FVSUM_1:67
theorem :: FVSUM_1:68
theorem :: FVSUM_1:69
theorem :: FVSUM_1:70
theorem :: FVSUM_1:71
theorem :: FVSUM_1:72
:: deftheorem defines mlt FVSUM_1:def 7 :
theorem :: FVSUM_1:73
theorem :: FVSUM_1:74
theorem :: FVSUM_1:75
canceled;
theorem :: FVSUM_1:76
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)*>
theorem :: FVSUM_1:77
theorem Th78: :: FVSUM_1:78
theorem :: FVSUM_1:79
theorem Th80: :: FVSUM_1:80
theorem :: FVSUM_1:81
theorem :: FVSUM_1:82
theorem :: FVSUM_1:83
theorem :: FVSUM_1:84
:: deftheorem defines Sum FVSUM_1:def 8 :
theorem :: FVSUM_1:85
canceled;
theorem :: FVSUM_1:86
canceled;
theorem :: FVSUM_1:87
theorem :: FVSUM_1:88
canceled;
theorem :: FVSUM_1:89
theorem :: FVSUM_1:90
canceled;
theorem :: FVSUM_1:91
canceled;
theorem :: FVSUM_1:92
theorem :: FVSUM_1:93
theorem :: FVSUM_1:94
theorem :: FVSUM_1:95
theorem :: FVSUM_1:96
Lm6:
for K being non empty commutative well-unital multLoopStr holds Product (<*> the carrier of K) = 1. K
theorem :: FVSUM_1:97
canceled;
theorem :: FVSUM_1:98
canceled;
theorem :: FVSUM_1:99
canceled;
theorem :: FVSUM_1:100
canceled;
theorem :: FVSUM_1:101
canceled;
theorem :: FVSUM_1:102
theorem :: FVSUM_1:103
canceled;
theorem :: FVSUM_1:104
theorem :: FVSUM_1:105
theorem :: FVSUM_1:106
theorem :: FVSUM_1:107
theorem :: FVSUM_1:108
theorem :: FVSUM_1:109
theorem :: FVSUM_1:110
theorem Th111: :: FVSUM_1:111
theorem :: FVSUM_1:112
:: deftheorem FVSUM_1:def 9 :
canceled;
:: deftheorem defines "*" FVSUM_1:def 10 :
theorem :: FVSUM_1:113
theorem :: FVSUM_1:114
theorem :: FVSUM_1:115