environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, FINSUB_1, BINOP_1, FUNCT_1, NAT_1, FINSEQ_1, FINSEQ_2, ARYTM_3, XXREAL_0, SETWISEO, TARSKI, RELAT_1, FINSEQOP, FUNCOP_1, FUNCT_4, ORDINAL4, FINSOP_1, CARD_1, SETWOP_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, RELAT_1, RELSET_1, FUNCT_1, FINSEQ_1, FINSUB_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, SETWISEO, FINSEQ_2, FINSEQOP, FINSOP_1, XXREAL_0;
definitions BINOP_1, XBOOLE_0;
theorems TARSKI, ENUMSET1, ZFMISC_1, NAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSEQ_1, FINSUB_1, BINOP_1, SETWISEO, FINSEQ_2, WELLORD2, CARD_1, FINSEQOP, RELAT_1, FUNCT_4, FINSOP_1, XBOOLE_0, XBOOLE_1, XREAL_1, ORDINAL1;
schemes NAT_1, SETWISEO, FINSEQ_2;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FINSUB_1, XREAL_0, FINSEQ_1, FINSEQ_2, NAT_1, CARD_1, RELAT_1;
constructors HIDDEN, PARTFUN1, WELLORD2, BINOP_1, SETWISEO, XXREAL_0, XREAL_0, NAT_1, FINSEQOP, FINSOP_1, RELSET_1, FINSEQ_2, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities RELAT_1;
expansions BINOP_1, XBOOLE_0;
Lm1:
for i being Nat holds Seg i is Element of Fin NAT
by FINSUB_1:def 5;
Lm2:
for i being Nat holds not i + 1 in Seg i
by FINSEQ_1:1, XREAL_1:29;
theorem Th9:
for
C,
D being non
empty set for
B being
Element of
Fin C for
e being
Element of
D for
F,
G being
BinOp of
D for
f,
f9 being
Function of
C,
D st
F is
commutative &
F is
associative &
F is
having_a_unity &
e = the_unity_wrt F &
G . (
e,
e)
= e & ( for
d1,
d2,
d3,
d4 being
Element of
D holds
F . (
(G . (d1,d2)),
(G . (d3,d4)))
= G . (
(F . (d1,d3)),
(F . (d2,d4))) ) holds
G . (
(F $$ (B,f)),
(F $$ (B,f9)))
= F $$ (
B,
(G .: (f,f9)))
Lm3:
for D being non empty set
for F being BinOp of D st F is commutative & F is associative holds
for d1, d2, d3, d4 being Element of D holds F . ((F . (d1,d2)),(F . (d3,d4))) = F . ((F . (d1,d3)),(F . (d2,d4)))
theorem
for
C,
D being non
empty set for
B being
Element of
Fin C for
F,
G being
BinOp of
D for
f,
f9 being
Function of
C,
D st
F is
commutative &
F is
associative &
F is
having_a_unity &
F is
having_an_inverseOp &
G = F * (
(id D),
(the_inverseOp_wrt F)) holds
G . (
(F $$ (B,f)),
(F $$ (B,f9)))
= F $$ (
B,
(G .: (f,f9)))
Lm4:
for D being non empty set
for e being Element of D
for F being BinOp of D
for p, q being FinSequence of D st len p = len q & F . (e,e) = e holds
F .: (([#] (p,e)),([#] (q,e))) = [#] ((F .: (p,q)),e)
Lm5:
for D being non empty set
for d, e being Element of D
for F being BinOp of D
for p being FinSequence of D st F . (e,d) = e holds
F [:] (([#] (p,e)),d) = [#] ((F [:] (p,d)),e)
Lm6:
for D being non empty set
for d, e being Element of D
for F being BinOp of D
for p being FinSequence of D st F . (d,e) = e holds
F [;] (d,([#] (p,e))) = [#] ((F [;] (d,p)),e)
theorem Th32:
for
D being non
empty set for
e being
Element of
D for
F,
G being
BinOp of
D for
p,
q being
FinSequence of
D st
F is
commutative &
F is
associative &
F is
having_a_unity &
e = the_unity_wrt F &
G . (
e,
e)
= e & ( for
d1,
d2,
d3,
d4 being
Element of
D holds
F . (
(G . (d1,d2)),
(G . (d3,d4)))
= G . (
(F . (d1,d3)),
(F . (d2,d4))) ) &
len p = len q holds
G . (
(F "**" p),
(F "**" q))
= F "**" (G .: (p,q))
theorem Th33:
for
D being non
empty set for
e being
Element of
D for
F,
G being
BinOp of
D for
i being
Nat for
T1,
T2 being
Element of
i -tuples_on D st
F is
commutative &
F is
associative &
F is
having_a_unity &
e = the_unity_wrt F &
G . (
e,
e)
= e & ( for
d1,
d2,
d3,
d4 being
Element of
D holds
F . (
(G . (d1,d2)),
(G . (d3,d4)))
= G . (
(F . (d1,d3)),
(F . (d2,d4))) ) holds
G . (
(F "**" T1),
(F "**" T2))
= F "**" (G .: (T1,T2))