:: Product of Families of Groups and Vector Spaces
:: by Anna Lango and Grzegorz Bancerek
::
:: Received December 29, 1992
:: Copyright (c) 1992-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RLVECT_1, ALGSTR_0, XBOOLE_0, STRUCT_0, VECTSP_1, SUPINF_2,
BINOP_1, SUBSET_1, FUNCT_1, ARYTM_3, FINSEQOP, ARYTM_1, RELAT_1, GROUP_1,
NAT_1, FINSEQ_2, CARD_3, FUNCOP_1, SETWISEO, ZFMISC_1, PARTFUN1, TARSKI,
FINSEQ_1, MESFUNC1, MCART_1, FUNCT_6, GROUP_2, NUMBERS, PRVECT_1,
PRALG_1, RLVECT_2, YELLOW_6, WAYBEL_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, NAT_1,
CARD_3, RELAT_1, FUNCT_1, STRUCT_0, ALGSTR_0, PARTFUN1, FUNCT_2, FUNCT_3,
BINOP_1, FUNCOP_1, RLVECT_1, GROUP_1, VECTSP_1, FINSEQOP, FINSEQ_1,
FUNCT_6, SETWISEO, FINSEQ_2, PRALG_1, YELLOW_6, WAYBEL_3;
constructors PARTFUN1, BINOP_1, FUNCT_3, SETWISEO, FUNCT_5, CARD_3, FINSEQOP,
FUNCT_6, VECTSP_1, RLVECT_1, RELSET_1, FINSEQ_2, GROUP_1, PRALG_1,
YELLOW_6, WAYBEL_3;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSEQ_1,
FINSEQ_2, CARD_3, STRUCT_0, VECTSP_1, RELSET_1, CARD_1;
requirements BOOLE, SUBSET;
definitions BINOP_1, FINSEQOP, VECTSP_1, STRUCT_0, ALGSTR_0, FUNCOP_1;
equalities BINOP_1, VECTSP_1, STRUCT_0, ALGSTR_0, FUNCOP_1;
expansions BINOP_1, FINSEQOP, RLVECT_1, FUNCT_1;
theorems BINOP_1, FUNCT_1, FUNCT_2, FUNCT_3, FINSEQ_1, FINSEQ_2, FINSEQ_3,
FINSEQOP, FUNCOP_1, VECTSP_1, ZFMISC_1, SETWISEO, TARSKI, CARD_3,
FUNCT_6, RLVECT_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, FVSUM_1,
GROUP_1, CARD_1, XTUPLE_0, PRALG_1, WAYBEL_3;
schemes FUNCT_1, BINOP_1, FUNCT_2, FINSEQ_1, CLASSES1;
begin :: Abelian Groups and Fields
reserve G for Abelian add-associative right_complementable right_zeroed
non empty addLoopStr;
deffunc car(1-sorted) = the carrier of $1;
deffunc ad(addLoopStr) = the addF of $1;
deffunc cc(non empty addLoopStr) = comp $1;
deffunc zr(addLoopStr) = 0.$1;
theorem Th1:
0.G is_a_unity_wrt the addF of G
proof
now
let x be Element of G;
thus (the addF of G).(0.G,x)=0.G + x .= x by RLVECT_1:4;
thus (the addF of G).(x,0.G)= x + 0.G .= x by RLVECT_1:4;
end;
hence thesis by BINOP_1:3;
end;
theorem Th2:
for G being AbGroup holds comp G is_an_inverseOp_wrt the addF of G
proof
let G be AbGroup;
A1: 0.G is_a_unity_wrt the addF of G by Th1;
now
let x be Element of G;
thus (the addF of G).(x,(comp G).x)= x+(-x) by VECTSP_1:def 13
.= 0.G by RLVECT_1:5
.= the_unity_wrt the addF of G by A1,BINOP_1:def 8;
thus (the addF of G).((comp G).x,x)=((comp G).x)+x
.= x+(-x) by VECTSP_1:def 13
.= 0.G by RLVECT_1:5
.= the_unity_wrt the addF of G by A1,BINOP_1:def 8;
end;
hence thesis;
end;
Lm1: comp G is_an_inverseOp_wrt the addF of G
proof
A1: 0.G is_a_unity_wrt the addF of G by Th1;
now
let x be Element of G;
thus (the addF of G).(x,(comp G).x)= x+(-x) by VECTSP_1:def 13
.= 0.G by RLVECT_1:5
.= the_unity_wrt the addF of G by A1,BINOP_1:def 8;
thus (the addF of G).((comp G).x,x)=((comp G).x)+x
.= x+(-x) by VECTSP_1:def 13
.= 0.G by RLVECT_1:5
.= the_unity_wrt the addF of G by A1,BINOP_1:def 8;
end;
hence thesis;
end;
reserve GS for non empty addLoopStr;
theorem
the addF of GS is commutative associative &
0.GS is_a_unity_wrt the addF of GS &
comp GS is_an_inverseOp_wrt the addF of GS implies GS is AbGroup
proof
assume that
A1: the addF of GS is commutative & the addF of GS is associative and
A2: 0.GS is_a_unity_wrt the addF of GS and
A3: comp GS is_an_inverseOp_wrt the addF of GS;
A4: GS is right_complementable
proof
let x be Element of GS;
reconsider b = (comp GS).x as Element of GS;
take b;
thus x+b = the_unity_wrt the addF of GS by A3
.= (0.GS) by A2,BINOP_1:def 8;
end;
for x,y,z being Element of GS holds x+y = y+x & (x+y)+z = x+(y+z) & x+(
0.GS) = x by A1,A2,BINOP_1:3;
hence thesis by A4,RLVECT_1:def 2,def 3,def 4;
end;
Lm2: the addF of GS is commutative associative implies
GS is Abelian add-associative;
Lm3: 0.GS is_a_unity_wrt the addF of GS implies GS is right_zeroed
by BINOP_1:3;
reserve F for Field;
Lm4: the multF of F is associative
proof
let x,y,z be Element of F;
thus (the multF of F).(x,(the multF of F).(y,z)) = x*(y*z)
.= (x*y)*z by GROUP_1:def 3
.= (the multF of F).((the multF of F).(x,y),z);
end;
theorem
0.F is_a_unity_wrt the addF of F
proof
now
let x be Element of F;
thus (the addF of F).(0.F,x) = x+(0.F) by RLVECT_1:2
.= x by RLVECT_1:4;
thus (the addF of F).(x,0.F) = x+(0.F) .= x by RLVECT_1:4;
end;
hence thesis by BINOP_1:3;
end;
theorem Th5:
1_F is_a_unity_wrt the multF of F
proof
now
let x be Element of F;
thus (the multF of F).(1_F,x) = (1_F)*x .= x;
thus (the multF of F).(x,1_F) = x*(1_F) .= x;
end;
hence thesis by BINOP_1:3;
end;
Lm5: the multF of F is_distributive_wrt the addF of F
proof
now
let x,y,z be Element of F;
thus (the multF of F).(x,(the addF of F).(y,z)) = x*(y + z)
.= x*y + x*z by VECTSP_1:def 7
.= (the addF of F).((the multF of F).(x,y),(the multF of F).(x,z));
thus (the multF of F).((the addF of F).(x,y),z) = (x + y)*z
.= x*z + y*z by VECTSP_1:def 7
.= (the addF of F).((the multF of F).(x,z),(the multF of F).(y,z));
end;
hence thesis by BINOP_1:11;
end;
begin :: The $n$-Product of a Binary and Unary Operation
reserve F for Field,
n for Nat,
D for non empty set,
d for Element of D,
B for BinOp of D,
C for UnOp of D;
definition
let D,n;
let F be BinOp of D;
let x,y be Element of n-tuples_on D;
redefine func F.:(x,y) -> Element of n-tuples_on D; :: redefines .: (FUNCOP_1, definition)
coherence by FINSEQ_2:120;
end;
definition
let D be non empty set;
let F be BinOp of D;
let n be Nat;
func product(F,n) -> BinOp of n-tuples_on D means
:Def1:
for x,y being Element of n-tuples_on D holds it.(x,y)=F.:(x,y);
existence
proof
defpred P[set,set,set] means ex x9,y9 be Element of n-tuples_on D st $1=x9
& $2=y9 & $3=F.:(x9,y9);
A1: for x,y being Element of (n-tuples_on D) qua non empty set ex z being
Element of (n-tuples_on D) qua non empty set st P[x,y,z]
proof
let x,y be Element of (n-tuples_on D) qua non empty set;
reconsider x9=x,y9=y as Element of n-tuples_on D;
reconsider z = F.:(x9,y9) as Element of (n-tuples_on D) qua non empty
set;
take z;
take x9,y9;
thus thesis;
end;
consider G being BinOp of n-tuples_on D such that
A2: for x,y being Element of (n-tuples_on D) qua non empty set holds P
[x,y,G.(x,y)] from BINOP_1:sch 3(A1);
take G;
let p1,p2 be Element of n-tuples_on D;
reconsider x=p1,y=p2 as Element of (n-tuples_on D) qua non empty set;
ex x9,y9 being Element of n-tuples_on D st x=x9 & y=y9 & G.(x,y)=F.:(
x9,y9) by A2;
hence thesis;
end;
uniqueness
proof
let G,H be BinOp of n-tuples_on D;
assume that
A3: for x,y being Element of n-tuples_on D holds G.(x,y)=F.:(x,y) and
A4: for x,y being Element of n-tuples_on D holds H.(x,y)=F.:(x,y);
now
let x,y be Element of n-tuples_on D;
G.(x,y)=F.:(x,y) by A3;
hence G.(x,y)=H.(x,y) by A4;
end;
hence G=H;
end;
end;
definition
let D;
let F be UnOp of D;
let n;
func product(F,n) -> UnOp of n-tuples_on D means
:Def2:
for x being Element of n-tuples_on D holds it.x=F*x;
existence
proof
defpred P[set,set] means ex x9 being Element of n-tuples_on D st x9=$1 &
$2=F*x9;
A1: for x being Element of (n-tuples_on D) qua non empty set ex y being
Element of (n-tuples_on D) qua non empty set st P[x,y]
proof
let x be Element of (n-tuples_on D) qua non empty set;
reconsider x9=x as Element of n-tuples_on D;
reconsider y=F*x9 as Element of (n-tuples_on D) qua non empty set by
FINSEQ_2:113;
take y, x9;
thus thesis;
end;
consider G being UnOp of n-tuples_on D such that
A2: for x being Element of (n-tuples_on D) qua non empty set holds P[x
,G.x] from FUNCT_2:sch 3(A1);
take G;
let p1 be Element of n-tuples_on D;
reconsider x=p1 as Element of (n-tuples_on D) qua non empty set;
ex x9 being Element of n-tuples_on D st x9=x & G.x=F*x9 by A2;
hence thesis;
end;
uniqueness
proof
let G,H be UnOp of n-tuples_on D;
assume that
A3: for x being Element of n-tuples_on D holds G.x=F*x and
A4: for x being Element of n-tuples_on D holds H.x=F*x;
now
let x be Element of n-tuples_on D;
G.x=F*x by A3;
hence G.x=H.x by A4;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th6:
B is commutative implies product(B,n) is commutative
proof
assume
A1: B is commutative;
now
let x,y be Element of n-tuples_on D;
thus product(B,n).(x,y) = B.:(x,y) by Def1
.= B.:(y,x) by A1,FINSEQOP:33
.= product(B,n).(y,x) by Def1;
end;
hence thesis;
end;
theorem Th7:
B is associative implies product(B,n) is associative
proof
assume
A1: B is associative;
now
let x,y,z be Element of n-tuples_on D;
thus product(B,n).(product(B,n).(x,y),z) = product(B,n).(B.:(x,y),z)
by Def1
.= B.:(B.:(x,y),z) by Def1
.= B.:(x,B.:(y,z)) by A1,FINSEQOP:28
.= product(B,n).(x,B.:(y,z)) by Def1
.= product(B,n).(x,product(B,n).(y,z)) by Def1;
end;
hence thesis;
end;
theorem Th8:
d is_a_unity_wrt B implies n |-> d is_a_unity_wrt product(B,n)
proof
assume d is_a_unity_wrt B;
then
A1: B is having_a_unity & d = the_unity_wrt B by BINOP_1:def 8,SETWISEO:def 2;
now
let b be Element of (n-tuples_on D) qua non empty set;
reconsider b9 = b as Element of n-tuples_on D;
thus product(B,n).(n |-> d,b) = B.:(n |-> d,b9) by Def1
.= b by A1,FINSEQOP:56;
thus product(B,n).(b,n |-> d) = B.:(b9,n |-> d) by Def1
.= b by A1,FINSEQOP:56;
end;
hence thesis by BINOP_1:3;
end;
theorem Th9:
B is having_a_unity & B is associative & C is_an_inverseOp_wrt B
implies product(C,n) is_an_inverseOp_wrt product(B,n)
proof
assume that
A1: B is having_a_unity and
A2: B is associative and
A3: C is_an_inverseOp_wrt B;
A4: B is having_an_inverseOp by A3;
then
A5: C = the_inverseOp_wrt B by A1,A2,A3,FINSEQOP:def 3;
A6: now
let f be Element of (n-tuples_on D) qua non empty set;
reconsider f9 = f as Element of n-tuples_on D;
reconsider cf = C*f9 as Element of n-tuples_on D by FINSEQ_2:113;
thus product(B,n).(f,product(C,n).f) = product(B,n).(f9,C*f9) by Def2
.= B.:(f9,cf) by Def1
.= n |->the_unity_wrt B by A1,A2,A4,A5,FINSEQOP:73;
thus product(B,n).(product(C,n).f,f) = product(B,n).(C*f9,f9) by Def2
.= B.:(cf,f9) by Def1
.= n |->the_unity_wrt B by A1,A2,A4,A5,FINSEQOP:73;
end;
ex d st d is_a_unity_wrt B by A1,SETWISEO:def 2;
then the_unity_wrt B is_a_unity_wrt B by BINOP_1:def 8;
then n |->the_unity_wrt B is_a_unity_wrt product(B,n) by Th8;
then n |->the_unity_wrt B = the_unity_wrt product(B,n) by BINOP_1:def 8;
hence thesis by A6;
end;
begin :: The $n$-Power of a Group and of a Field
definition
let F be non empty addLoopStr, n;
assume
A1: F is Abelian add-associative right_zeroed right_complementable;
func n -Group_over F -> strict AbGroup equals
:Def3:
addLoopStr(# n-tuples_on the carrier of F, product(the addF of F,n),
(n |-> 0.F) qua Element of n-tuples_on the carrier of F#);
coherence
proof
set G = addLoopStr(# n-tuples_on the carrier of F,product(the addF of F,n)
, (n |-> 0.F) qua Element of n-tuples_on the carrier of F#);
reconsider G as non empty addLoopStr;
the addF of F is commutative associative by A1,FVSUM_1:1,2; then
A2: product(the addF of F,n) is commutative associative by Th6,Th7;
A3: 0.F is_a_unity_wrt the addF of F by A1,Th1;
A4: G is right_complementable
proof
set B = the addF of F;
set C = comp F;
let x be Element of G;
reconsider y = (product (comp F,n)).x as Element of G by FUNCT_2:5;
take y;
B is associative & B is having_a_unity by A1,A3,FVSUM_1:2,SETWISEO:def 2;
then product(C,n) is_an_inverseOp_wrt product(B,n) by A1,Lm1,Th9;
then
A5: x + y = the_unity_wrt product(B,n);
0.G is_a_unity_wrt the addF of G by A1,Th1,Th8;
hence thesis by A5,BINOP_1:def 8;
end;
0.G = (n |-> 0.F) & (n |-> 0.F) qua Element of n-tuples_on the
carrier of F is_a_unity_wrt product(the addF of F,n) by A1,Th1,Th8;
hence thesis by A2,A4,Lm2,Lm3;
end;
end;
registration
let F be AbGroup, n;
cluster n-Group_over F -> non empty;
coherence;
end;
reserve x,y for set;
definition
let F,n;
func n -Mult_over F -> Function of
[:the carrier of F,n-tuples_on the carrier of F:],
n-tuples_on the carrier of F means :Def4:
for x being Element of F,
v being Element of n-tuples_on the carrier of F holds
it.(x,v) = (the multF of F)[;](x,v);
existence
proof
defpred P[object,object] means
(ex x1 being Element of F, v being Element of n
-tuples_on the carrier of F st $1=[x1,v] & $2=(the multF of F)[;](x1,v));
A1: for x being object st
x in [:the carrier of F,n-tuples_on the carrier of F:]
ex y being object
st y in n-tuples_on the carrier of F & P[x,y]
proof
let x be object;
assume x in [:the carrier of F,n-tuples_on the carrier of F:];
then consider x1,v being object such that
A2: x1 in the carrier of F and
A3: v in n-tuples_on the carrier of F and
A4: [x1,v] = x by ZFMISC_1:84;
reconsider v as Element of n-tuples_on the carrier of F by A3;
reconsider x1 as Element of F by A2;
take y = (the multF of F)[;](x1,v);
y is Element of n-tuples_on the carrier of F by FINSEQ_2:121;
hence y in n-tuples_on the carrier of F;
take x1,v;
thus thesis by A4;
end;
consider f be Function of [:the carrier of F,n-tuples_on the carrier of F
:], n-tuples_on the carrier of F such that
A5: for x being object
st x in [:the carrier of F,n-tuples_on the carrier of F:]
holds P[x,f.x] from FUNCT_2:sch 1(A1);
take f;
let x be Element of F, v be Element of n-tuples_on the carrier of F;
[x,v] in [:the carrier of F,n-tuples_on the carrier of F:] by ZFMISC_1:87;
then consider x1 being Element of F, v1 being Element of n-tuples_on the
carrier of F such that
A6: [x,v]=[x1,v1] and
A7: f.[x,v]=(the multF of F)[;](x1,v1) by A5;
x1 = x by A6,XTUPLE_0:1;
hence thesis by A6,A7,XTUPLE_0:1;
end;
uniqueness
proof
let f,g be Function of [:the carrier of F,n-tuples_on the carrier of F:],
n-tuples_on the carrier of F;
assume that
A8: for x being Element of F,v being Element of n-tuples_on the
carrier of F holds f.(x,v) = (the multF of F)[;](x,v) and
A9: for x being Element of F,v being Element of n-tuples_on the
carrier of F holds g.(x,v) = (the multF of F)[;](x,v);
now
let x be Element of F, v be Element of n-tuples_on the carrier of F;
f.(x,v) = (the multF of F)[;](x,v) by A8;
hence f.(x,v)=g.(x,v) by A9;
end;
hence thesis;
end;
end;
definition
let F,n;
func n -VectSp_over F -> strict ModuleStr over F means
:Def5:
the addLoopStr of it = n -Group_over F & the lmult of it = n -Mult_over F;
existence
proof
n-Group_over F = addLoopStr(# n-tuples_on the carrier of F,
product(the addF of F,n), (n |-> 0.F) qua
Element of n-tuples_on the carrier of F#) by Def3;
then reconsider d = n-Mult_over F as Function of [:the carrier of F, the
carrier of n-Group_over F:], the carrier of n-Group_over F;
set G = n-Group_over F;
take ModuleStr(#car(G), ad(G), zr(G), d#);
thus thesis;
end;
uniqueness;
end;
registration
let F,n;
cluster n -VectSp_over F -> non empty;
coherence
proof
the addLoopStr of n -VectSp_over F = n -Group_over F by Def5;
hence the carrier of n -VectSp_over F is non empty;
end;
end;
reserve D for non empty set,
H,G for BinOp of D,
d for Element of D,
t1,t2 for Element of n-tuples_on D;
theorem Th10:
H is_distributive_wrt G implies
H[;](d,G.:(t1,t2)) = G.: (H[;](d,t1),H[;](d,t2))
proof
rng (H*<:dom t1 -->d,t1:>) c= rng H & rng (H*<:dom t2 -->d,t2:>) c= rng
H by RELAT_1:26;
then rng <:H*<:dom t1 -->d,t1:>,H*<:dom t2 -->d,t2:>:> c= [:rng (H*<:dom t1
-->d, t1:>),rng (H*<:dom t2 -->d,t2:>):] & [:rng (H*<:dom t1 -->d,t1:>),rng (H*
<:dom t2 -->d,t2:>):] c= [:rng H, rng H:] by FUNCT_3:51,ZFMISC_1:96;
then
A1: rng <:H*<:dom t1 -->d,t1:>,H*<:dom t2 -->d,t2:>:> c= [:rng H,rng H:] by
XBOOLE_1:1;
rng H c= D by RELAT_1:def 19;
then [:rng H,rng H:] c= [:D,D:] by ZFMISC_1:96;
then rng <:H*<:dom t1 -->d,t1:>,H*<:dom t2 -->d,t2:>:> c= [:D,D:] by A1,
XBOOLE_1:1;
then
A2: rng <:H*<:dom t1 -->d,t1:>,H*<:dom t2 -->d,t2:>:> c= dom G by FUNCT_2:def 1
;
A3: dom t2 = Seg (len t2) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7;
rng t1 c= D & rng t2 c= D by FINSEQ_1:def 4;
then
A4: [:rng t1,rng t2:] c= [:D,D:] by ZFMISC_1:96;
rng <:t1,t2:> c= [:rng t1,rng t2:] by FUNCT_3:51;
then rng <:t1,t2:> c= [:D,D:] by A4,XBOOLE_1:1;
then
A5: rng <:t1,t2:> c= dom G by FUNCT_2:def 1;
A6: dom (dom t2 -->d) = dom t2 by FUNCOP_1:13
.= Seg (len t2) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7;
dom t1 = Seg (len t1) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7;
then dom <:t1,t2:> = Seg n by A3,FUNCT_3:50; then
A7: dom (G*<:t1,t2:>) = Seg n by A5,RELAT_1:27;
then dom (dom (G*<:t1,t2:>) -->d) = Seg n by FUNCOP_1:13;
then
A8: dom <: dom (G*<:t1,t2:>) -->d,G*<:t1,t2:>:> = Seg n by A7,FUNCT_3:50;
rng t2 c= D by FINSEQ_1:def 4;
then rng <:dom t2 -->d,t2:> c= [:rng (dom t2 -->d),rng t2:] & [:rng (dom t2
-->d) ,rng t2:] c= [:rng (dom t2 -->d),D:] by FUNCT_3:51,ZFMISC_1:96;
then
A9: rng <:dom t2 -->d,t2:> c= [:rng (dom t2 -->d),D:] by XBOOLE_1:1;
rng (dom t2 -->d) c= {d} by FUNCOP_1:13;
then [:rng (dom t2 -->d),D:] c= [:{d},D:] by ZFMISC_1:96;
then
A10: rng <:dom t2 -->d,t2:> c= [:{d},D:] by A9,XBOOLE_1:1;
A11: dom t1 = Seg (len t1) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7;
rng t1 c= D by FINSEQ_1:def 4;
then rng <:dom t1 -->d,t1:> c= [:rng (dom t1 -->d),rng t1:] & [:rng (dom t1
-->d) ,rng t1:] c= [:rng (dom t1 -->d),D:] by FUNCT_3:51,ZFMISC_1:96;
then
A12: rng <:dom t1 -->d,t1:> c= [:rng (dom t1 -->d),D:] by XBOOLE_1:1;
rng (dom t1 -->d) c= {d} by FUNCOP_1:13;
then [:rng (dom t1 -->d),D:] c= [:{d},D:] by ZFMISC_1:96;
then
A13: rng <:dom t1 -->d,t1:> c= [:{d},D:] by A12,XBOOLE_1:1;
A14: dom (dom t1 -->d) = dom t1 by FUNCOP_1:13
.= Seg (len t1) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7;
{d} c= D by ZFMISC_1:31;
then
A15: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;
rng (dom (G*<:t1,t2:>) -->d) c= {d} & {d} c= D by FUNCOP_1:13,ZFMISC_1:31;
then
A16: rng (dom (G*<:t1,t2:>) -->d) c= D by XBOOLE_1:1;
A17: dom t2 = Seg (len t2) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7;
dom H = [:D,D:] by FUNCT_2:def 1;
then
A18: dom (H*<:dom t2-->d,t2:>) = dom <:dom t2 -->d,t2:> by A10,A15,RELAT_1:27
,XBOOLE_1:1
.= Seg n by A6,A17,FUNCT_3:50;
{d} c= D by ZFMISC_1:31;
then
A19: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;
set A = H*<:dom (G*<:t1,t2:>) --> d,G*<:t1,t2:>:>;
dom H = [:D,D:] by FUNCT_2:def 1;
then dom (H*<:dom t1 -->d,t1:>) = dom <:dom t1 -->d,t1:> by A13,A19,
RELAT_1:27,XBOOLE_1:1
.= Seg n by A14,A11,FUNCT_3:50;
then dom <:H*<:dom t1 -->d,t1:>,H*<:dom t2 -->d,t2:>:> = Seg n by A18,
FUNCT_3:50;
then
A20: dom (G*<:H*<:dom t1 -->d,t1:>,H*<:dom t2 -->d,t2:>:>) = Seg n by A2,
RELAT_1:27;
rng (G*<:t1,t2:>) c= D by RELAT_1:def 19;
then
rng <: dom (G*<:t1,t2:>) -->d,G*<:t1,t2:>:> c= [:rng (dom (G*<:t1,t2:>)
-->d) ,rng (G*<:t1,t2:>):] & [:rng (dom (G*<:t1,t2:>) -->d),rng (G*<:t1,t2:>):]
c= [:D,D:] by A16,FUNCT_3:51,ZFMISC_1:96;
then rng <: dom (G*<:t1,t2:>) -->d,G*<:t1,t2:>:> c= [:D,D:] by XBOOLE_1:1;
then
A21: rng <: dom (G*<:t1,t2:>) -->d,G*<:t1,t2:>:> c= dom H by FUNCT_2:def 1;
then
A22: dom A = Seg n by A8,RELAT_1:27;
assume
A23: H is_distributive_wrt G;
for x being object st x in dom A
holds H[;](d,G.:(t1,t2)).x = G.:(H[;](d,t1),H[;](d,t2 ) ) . x
proof
rng t1 c= D by FINSEQ_1:def 4;
then rng <:dom t1 -->d,t1:> c= [:rng (dom t1 -->d),rng t1:] & [:rng (dom
t1 -->d) ,rng t1:] c= [:rng (dom t1 -->d),D:] by FUNCT_3:51,ZFMISC_1:96;
then
A24: rng <:dom t1 -->d,t1:> c= [:rng (dom t1 -->d),D:] by XBOOLE_1:1;
rng (dom t1 -->d) c= {d} by FUNCOP_1:13;
then [:rng (dom t1 -->d),D:] c= [:{d},D:] by ZFMISC_1:96;
then
A25: rng <:dom t1 -->d,t1:> c= [:{d},D:] by A24,XBOOLE_1:1;
A26: rng t1 c= D & rng t2 c= D by FINSEQ_1:def 4;
{d} c= D by ZFMISC_1:31; then
A27: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;
A28: dom (dom t2 -->d) = dom t2 by FUNCOP_1:13
.= Seg (len t2) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7;
{d} c= D by ZFMISC_1:31; then
A29: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;
A30: dom t1 = Seg (len t1) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7;
rng t2 c= D by FINSEQ_1:def 4;
then rng <:dom t2 -->d,t2:> c= [:rng (dom t2 -->d),rng t2:] & [:rng (dom
t2 -->d) ,rng t2:] c= [:rng (dom t2 -->d),D:] by FUNCT_3:51,ZFMISC_1:96;
then
A31: rng <:dom t2 -->d,t2:> c= [:rng (dom t2 -->d),D:] by XBOOLE_1:1;
rng (dom t2 -->d) c= {d} by FUNCOP_1:13;
then [:rng (dom t2 -->d),D:] c= [:{d},D:] by ZFMISC_1:96;
then
A32: rng <:dom t2 -->d,t2:> c= [:{d},D:] by A31,XBOOLE_1:1;
A33: dom (dom t1 -->d) = dom t1 by FUNCOP_1:13
.= Seg (len t1) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7;
let x be object;
A34: dom <:dom (G.:(t1,t2)) -->d,G.:(t1,t2):> = dom (dom (G.:(t1,t2)) -->d
) /\ dom (G.:(t1,t2)) by FUNCT_3:def 7;
assume
A35: x in dom A;
then x in dom <:dom (G.:(t1,t2)) -->d,G.:(t1,t2):> by FUNCT_1:11;
then
A36: x in dom (G.:(t1,t2)) by A34,XBOOLE_0:def 4;
dom t1 = Seg (len t1) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7;
then
A37: t1.x in rng t1 by A22,A35,FUNCT_1:def 3;
A38: dom t2 = Seg (len t2) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7;
dom H = [:D,D:] by FUNCT_2:def 1;
then dom (H*<:dom t1 -->d,t1:>) = dom <:dom t1 -->d,t1:> by A25,A29,
RELAT_1:27,XBOOLE_1:1
.= Seg n by A33,A30,FUNCT_3:50; then
A39: x in dom (H[;](d,t1)) by A22,A35;
dom t2 = Seg (len t2) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7; then
A40: t2.x in rng t2 by A22,A35,FUNCT_1:def 3;
dom H = [:D,D:] by FUNCT_2:def 1;
then dom (H*<:dom t2-->d,t2:>) = dom <:dom t2 -->d,t2:> by A32,A27,
RELAT_1:27,XBOOLE_1:1
.= Seg n by A28,A38,FUNCT_3:50; then
A41: x in dom (H[;](d,t2)) by A22,A35;
H[;](d,G.:(t1,t2)).x = H.(d,G.:(t1,t2).x) by A35,FUNCOP_1:32
.= H.(d,G.(t1.x,t2.x)) by A36,FUNCOP_1:22
.= G.(H.(d,t1.x),H.(d,t2.x)) by A23,A37,A26,A40,BINOP_1:11
.= G.((H[;](d,t1)).x,H.(d,t2.x)) by A39,FUNCOP_1:32
.= G.((H[;](d,t1)).x,(H[;](d,t2)).x) by A41,FUNCOP_1:32
.= (G.: (H[;](d,t1),H[;](d,t2))).x by A22,A20,A35,FUNCOP_1:22;
hence thesis;
end;
hence thesis by A8,A21,A20,RELAT_1:27;
end;
definition
let D be non empty set, n be Nat, F be BinOp of D, x be Element of D,
v be Element of n-tuples_on D;
redefine func F[;](x,v) -> Element of n-tuples_on D; :: redefines [;] (FUNCOP_1, definition)
coherence by FINSEQ_2:121;
end;
registration
let F,n;
cluster n -VectSp_over F -> vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence
proof
A1: the addLoopStr of n -VectSp_over F=n-Group_over F & n-Group_over F=
addLoopStr(# n-tuples_on the carrier of F, product(the addF of F,n), (n |-> 0.
F) qua Element of n-tuples_on the carrier of F#) by Def3,Def5;
1_F is_a_unity_wrt the multF of F by Th5;
then
A2: the multF of F is having_a_unity & the_unity_wrt the multF of F = 1_F
by BINOP_1:def 8,SETWISEO:def 2;
A3: n-VectSp_over F is vector-distributive
proof
let x be Element of F;
let v,w be Element of n -VectSp_over F;
reconsider v9=v,w9=w as Element of n-tuples_on the carrier of F by A1;
thus x*(v+w) = (n-Mult_over F).(x,product(the addF of F,n).(v,w)) by A1
,Def5
.= (n-Mult_over F).(x,(the addF of F).:(v9,w9)) by Def1
.= (the multF of F)[;](x,(the addF of F).:(v9,w9)) by Def4
.= (the addF of F).: ((the multF of F)[;](x,v9),(the multF of F)[;](
x,w9)) by Lm5,Th10
.= product(the addF of F,n).((the multF of F)[;](x,v9), (the multF
of F)[;](x,w9)) by Def1
.= product(the addF of F,n).((n-Mult_over F).(x,v9), (the multF of F
)[;](x,w9)) by Def4
.= product(the addF of F,n).((n-Mult_over F).(x,v9), (n-Mult_over F)
.(x,w9)) by Def4
.= product(the addF of F,n).((the lmult of n-VectSp_over F).(x,v), (
n-Mult_over F).(x,w9)) by Def5
.= x*v + x*w by A1,Def5;
end;
A4: n-VectSp_over F is scalar-distributive
proof
let x,y be Element of F;
let v be Element of n -VectSp_over F;
reconsider v9=v as Element of n-tuples_on the carrier of F by A1;
thus (x+y)*v = (n-Mult_over F).(x+y,v9) by Def5
.= (the multF of F)[;]((the addF of F).(x,y),v9) by Def4
.= (the addF of F).: ((the multF of F)[;](x,v9),(the multF of F)[;](
y,v9)) by Lm5,FINSEQOP:46
.= product(the addF of F,n).((the multF of F)[;](x,v9), (the multF
of F)[;](y,v9)) by Def1
.= product(the addF of F,n).((n-Mult_over F).(x,v9), (the multF of F
)[;](y,v9)) by Def4
.= product(the addF of F,n).((n-Mult_over F).(x,v9), (n-Mult_over F)
.(y,v9)) by Def4
.= product(the addF of F,n).((the lmult of n-VectSp_over F).(x,v), (
n-Mult_over F).(y,v9)) by Def5
.= x*v + y*v by A1,Def5;
end;
A5: n-VectSp_over F is scalar-associative
proof
let x,y be Element of F;
let v be Element of n -VectSp_over F;
reconsider v9=v as Element of n-tuples_on the carrier of F by A1;
thus (x*y)*v = (n-Mult_over F).(x*y,v9) by Def5
.= (the multF of F)[;](x*y,v9) by Def4
.= (the multF of F)[;](x,(the multF of F)[;](y,v9)) by Lm4,FINSEQOP:31
.= (n-Mult_over F).(x,(the multF of F)[;](y,v9)) by Def4
.= (n-Mult_over F).(x,(n-Mult_over F).(y,v9)) by Def4
.= (n-Mult_over F).(x,(the lmult of n-VectSp_over F).(y,v)) by Def5
.= x*(y*v) by Def5;
end;
n-VectSp_over F is scalar-unital
proof
let v be Element of n -VectSp_over F;
reconsider v9=v as Element of n-tuples_on the carrier of F by A1;
thus (1.F)*v = (n-Mult_over F).(1.F,v9) by Def5
.= (the multF of F)[;](1.F,v9) by Def4
.= v by A2,FINSEQOP:57;
end;
hence thesis by A3,A4,A5;
end;
end;
begin :: Sequences of domains
reserve x,y,z for set,
A for AbGroup;
definition
mode Domain-Sequence is non empty non-empty FinSequence;
end;
scheme
NEFinSeqLambda {w() -> non empty FinSequence, F(set)->set}:
ex p being non empty FinSequence st
len p = len w() & for i being Element of dom w() holds p.i = F(i)
proof
consider p being FinSequence such that
A1: len p = len w() & for i being Nat st i in dom p holds p.i = F(i)
from FINSEQ_1:sch 2;
reconsider p9=p as non empty FinSequence by A1;
take p9;
thus len p9 = len w() by A1;
let i be Element of dom w();
A2: dom w() = Seg len w() by FINSEQ_1:def 3;
dom p = Seg len w() by A1,FINSEQ_1:def 3;
hence thesis by A1,A2;
end;
definition
let a be non-empty non empty Function;
let f be Element of product a;
let i be Element of dom a;
redefine func f.i -> Element of a.i; :: redefines . (FUNCT_1, definition)
coherence by CARD_3:9;
end;
begin :: The Product of Families of Operations
reserve a for Domain-Sequence,
i for Element of dom a,
p for FinSequence;
definition
let a be non-empty non empty Function;
mode BinOps of a -> Function means :Def6:
dom it = dom a & for i being Element of dom a holds it.i is BinOp of a.i;
existence
proof
deffunc F(object) = pr1(a.$1,a.$1);
consider f being Function such that
A1: dom f = dom a &
for x being object st x in dom a holds f.x = F(x) from FUNCT_1:sch 3;
take f;
thus dom f = dom a by A1;
let i be Element of dom a;
f.i = pr1(a.i,a.i) by A1;
hence thesis;
end;
mode UnOps of a -> Function means :Def7:
dom it = dom a & for i being Element of dom a holds it.i is UnOp of a.i;
existence
proof
deffunc F(object) = id (a.$1);
consider f being Function such that
A2: dom f = dom a &
for x being object st x in dom a holds f.x = F(x) from FUNCT_1:sch 3;
take f;
thus dom f = dom a by A2;
let i be Element of dom a;
f.i = id (a.i) by A2;
hence thesis;
end;
end;
registration
let a;
cluster -> FinSequence-like for BinOps of a;
coherence
proof
let f be BinOps of a;
dom a = dom f & dom a = Seg len a by Def6,FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 2;
end;
cluster -> FinSequence-like for UnOps of a;
coherence
proof
let f be UnOps of a;
dom a = dom f & dom a = Seg len a by Def7,FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 2;
end;
end;
registration
let a;
cluster -> Function-yielding for BinOps of a;
coherence
proof let b be BinOps of a;
let x be object;
assume x in dom b;
then reconsider xx=x as Element of dom a by Def6;
b.xx is BinOp of a.xx by Def6;
hence b.x is Function;
end;
cluster -> Function-yielding for UnOps of a;
coherence
proof let b be UnOps of a;
let x be object;
assume x in dom b;
then reconsider xx=x as Element of dom a by Def7;
b.xx is UnOp of a.xx by Def7;
hence b.x is Function;
end;
end;
theorem Th11:
p is BinOps of a iff len p = len a & for i holds p.i is BinOp of a.i
proof
dom p = dom a iff len p = len a by FINSEQ_3:29;
hence thesis by Def6;
end;
theorem Th12:
p is UnOps of a iff len p = len a & for i holds p.i is UnOp of a .i
proof
dom p = dom a iff len p = len a by FINSEQ_3:29;
hence thesis by Def7;
end;
definition
let a;
let b be BinOps of a;
let i;
redefine func b.i -> BinOp of a.i; :: redefines . (FUNCT_1, definition)
coherence by Th11;
end;
definition
let a;
let u be UnOps of a;
let i;
redefine func u.i -> UnOp of a.i; :: redefines . (FUNCT_1, definition)
coherence by Th12;
end;
theorem
for d,d9 being UnOp of product a st
for f being Element of product a, i being Element of dom a holds
(d.f).i = (d9.f).i holds d = d9
proof
let d,d9 be UnOp of product a such that
A1: for f being Element of product a, i being Element of dom a holds
(d.f).i = (d9.f).i;
now
let f be Element of product a;
dom (d.f) = dom a & dom (d9.f) = dom a by CARD_3:9;
hence d.f = d9.f by A1;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th14:
for u being UnOps of a holds doms u = a & product rngs u c= product a
proof
let u be UnOps of a;
A2: dom a = Seg len a & dom u = Seg len u by FINSEQ_1:def 3;
A3: len u = len a by Th12;
A4: dom doms u = dom u by FUNCT_6:def 2;
A5: now
let x be object;
assume x in dom u;
then reconsider i = x as Element of dom a by A2,Th12;
(rngs u).i = rng (u.i) by A2,A3,FUNCT_6:22;
hence (rngs u).x c= a.x by RELAT_1:def 19;
end;
now
let x be object;
assume x in dom u;
then reconsider i = x as Element of dom a by A2,Th12;
(doms u).i = dom (u.i) by A2,A3,FUNCT_6:22
.= a.i by FUNCT_2:def 1;
hence (doms u).x = a.x;
end;
hence doms u = a by A2,Th12,A4;
dom rngs u = dom u by FUNCT_6:def 3;
hence thesis by A2,A3,A5,CARD_3:27;
end;
definition
let a;
let u be UnOps of a;
redefine func Frege u -> UnOp of product a; :: redefines Frege (FUNCT_6, definition)
coherence
proof
A1: product rngs u c= product a & rng Frege u = product rngs u by Th14,
FUNCT_6:38;
dom Frege u = product doms u & doms u = a by Th14,FUNCT_6:def 7;
hence thesis by A1,FUNCT_2:def 1,RELSET_1:4;
end;
end;
theorem Th15:
for u being UnOps of a for f being Element of product a, i being
Element of dom a holds (Frege u).f.i = (u.i).(f.i)
proof
let u be UnOps of a, f be Element of product a;
let i be Element of dom a;
A1: dom u = Seg len u & doms u = a by Th14,FINSEQ_1:def 3;
dom a = Seg len a & len a = len u by Th12,FINSEQ_1:def 3;
hence thesis by A1,FUNCT_6:37;
end;
theorem Th16:
for d,d9 being BinOp of product a st
for f,g being Element of product a, i being Element of dom a holds
(d.(f,g)).i = (d9.(f,g)).i holds d = d9
proof
let d,d9 be BinOp of product a such that
A1: for f,g be Element of product a, i be Element of dom a holds
(d.(f,g)).i = (d9.(f,g)).i;
now
let f,g be Element of product a;
dom (d.(f,g)) = dom a & dom (d9.(f,g)) = dom a by CARD_3:9;
hence d.(f,g) = d9.(f,g) by A1;
end;
hence thesis;
end;
reserve i for Element of dom a;
definition
let a;
let b be BinOps of a;
func [:b:] -> BinOp of product a means
:Def8:
for f,g being Element of product a, i being Element of dom a holds
(it.(f,g)).i = (b.i).(f.i,g.i);
existence
proof
defpred Q[Element of product a,Element of product a,Element of product a]
means for i being Element of dom a holds $3.i = (b.i).($1.i,$2.i);
A1: for f,g being Element of product a ex z being Element of product a st
Q[f,g,z]
proof
let f,g be Element of product a;
defpred P[object,object] means ex i st $1 =i & $2 = (b.i).(f.i,g.i);
A2: for x being object st x in dom a ex z being object st P[x,z]
proof
let x be object;
assume x in dom a;
then reconsider i = x as Element of dom a;
take (b.i).(f.i,g.i);
thus thesis;
end;
consider z being Function such that
A3: dom z = dom a &
for x being object st x in dom a holds P[x,z.x]
from CLASSES1:sch 1(A2);
now
let x be object;
assume x in dom a;
then ex i st x = i & z.x = (b.i).(f.i,g.i) by A3;
hence z.x in a.x;
end;
then reconsider z9 = z as Element of product a by A3,CARD_3:9;
take z9;
let i;
ex j being Element of dom a st j = i & z.i = (b.j).(f.j,g.j) by A3;
hence thesis;
end;
consider d being BinOp of product a such that
A4: for f,g being Element of product a holds Q[f,g,d.(f,g)] from
BINOP_1:sch 3 (A1);
take d;
thus thesis by A4;
end;
uniqueness
proof
let d,d9 be BinOp of product a such that
A5: for f,g being Element of product a,i being Element of dom a holds
(d.(f,g)).i = (b.i).(f.i,g.i) and
A6: for f,g being Element of product a,i being Element of dom a holds
(d9.(f,g)).i = (b.i).(f.i,g.i);
now
let f,g be Element of product a;
let i be Element of dom a;
thus (d.(f,g)).i = (b.i).(f.i,g.i) by A5
.= (d9.(f,g)).i by A6;
end;
hence thesis by Th16;
end;
end;
theorem Th17:
for b being BinOps of a st for i holds b.i is commutative holds
[:b:] is commutative
proof
let b be BinOps of a such that
A1: for i holds b.i is commutative;
let x,y be Element of product a;
A2: now
let z be object;
assume z in dom a;
then reconsider i = z as Element of dom a;
A3: [:b:].(y,x).i = (b.i).(y.i,x.i) by Def8;
b.i is commutative & [:b:].(x,y).i = (b.i).(x.i,y.i) by A1,Def8;
hence [:b:].(x,y).z = [:b:].(y,x).z by A3;
end;
dom ([:b:].(x,y)) = dom a & dom ([:b:].(y,x)) = dom a by CARD_3:9;
hence thesis by A2,FUNCT_1:2;
end;
theorem Th18:
for b being BinOps of a st for i holds b.i is associative holds
[:b:] is associative
proof
let b be BinOps of a such that
A1: for i holds b.i is associative;
let x,y,z be Element of product a;
A2: now
set xy = [:b:].(x,y), yz = [:b:].(y,z);
let v be object;
assume v in dom a;
then reconsider i = v as Element of dom a;
A3: [:b:].(y,z).i = (b.i).(y.i,z.i) & [:b:].(x,yz).i = (b.i).(x.i,yz.i) by Def8
;
A4: [:b:].(xy,z).i = (b.i).(xy.i,z.i) by Def8;
b.i is associative & [:b:].(x,y).i = (b.i).(x.i,y.i) by A1,Def8;
hence [:b:].(x,[:b:].(y,z)).v = [:b:].([:b:].(x,y),z).v by A3,A4;
end;
dom ([:b:].(x,[:b:].(y,z))) = dom a &
dom ([:b:].([:b:].(x,y),z)) = dom a by CARD_3:9;
hence thesis by A2,FUNCT_1:2;
end;
theorem Th19:
for b being BinOps of a, f being Element of product a st for i
holds f.i is_a_unity_wrt b.i holds f is_a_unity_wrt [:b:]
proof
let b be BinOps of a, f be Element of product a such that
A1: for i holds f.i is_a_unity_wrt b.i;
now
let x be Element of product a;
A3: now
let y be object;
assume y in dom a;
then reconsider i = y as Element of dom a;
[:b:].(f,x).i = (b.i).(f.i,x.i) & f.i is_a_unity_wrt b.i by A1,Def8;
hence [:b:].(f,x).y = x.y by BINOP_1:3;
end;
dom ([:b:].(f,x)) = dom a by CARD_3:9;
hence [:b:].(f,x) = x by A3,CARD_3:9;
A4: now
let y be object;
assume y in dom a;
then reconsider i = y as Element of dom a;
[:b:].(x,f).i = (b.i).(x.i,f.i) & f.i is_a_unity_wrt b.i by A1,Def8;
hence [:b:].(x,f).y = x.y by BINOP_1:3;
end;
dom ([:b:].(x,f)) = dom a by CARD_3:9;
hence [:b:].(x,f) = x by A4,CARD_3:9;
end;
hence thesis by BINOP_1:3;
end;
theorem Th20:
for b being BinOps of a, u being UnOps of a st for i holds
u.i is_an_inverseOp_wrt b.i & b.i is having_a_unity holds
Frege u is_an_inverseOp_wrt [:b:]
proof
let b be BinOps of a, u be UnOps of a such that
A1: for i holds u.i is_an_inverseOp_wrt b.i & b.i is having_a_unity;
defpred P[object,object] means
ex i st $1 = i & $2 = the_unity_wrt (b.i);
A2: for x being object st x in dom a ex y being object st P[x,y]
proof
let x be object;
assume x in dom a;
then reconsider i = x as Element of dom a;
take the_unity_wrt (b.i);
thus thesis;
end;
consider f being Function such that
A3: dom f = dom a &
for x being object st x in dom a holds P[x,f.x] from CLASSES1:sch 1(A2);
now
let x be object;
assume x in dom a;
then ex i st x = i & f.x = the_unity_wrt (b.i) by A3;
hence f.x in a.x;
end;
then reconsider f as Element of product a by A3,CARD_3:9;
let x be Element of product a;
A5: now
let y be object;
assume y in dom a;
then reconsider i = y as Element of dom a;
A6: (Frege u).x.i = (u.i).(x.i) & u.i is_an_inverseOp_wrt b.i by A1,Th15;
( ex j being Element of dom a st i = j & f.i = the_unity_wrt (b.j))&
[:b:].(x, (Frege u).x).i = (b.i).(x.i,(Frege u).x.i) by A3,Def8;
hence [:b:].(x,(Frege u).x).y = f.y by A6;
end;
now
let i;
( ex j being Element of dom a st i = j & f.i = the_unity_wrt (b.j))& b
.i is having_a_unity by A1,A3;
hence f.i is_a_unity_wrt b.i by SETWISEO:14;
end;
then f is_a_unity_wrt [:b:] by Th19;
then
A7: f = the_unity_wrt [:b:] by BINOP_1:def 8;
A8: now
let y be object;
assume y in dom a;
then reconsider i = y as Element of dom a;
A9: (Frege u).x.i = (u.i).(x.i) & u.i is_an_inverseOp_wrt b.i by A1,Th15;
( ex j being Element of dom a st i = j & f.i = the_unity_wrt (b.j))&
[:b:].(( Frege u).x,x).i = (b.i).((Frege u).x.i,x.i) by A3,Def8;
hence [:b:].((Frege u).x,x).y = f.y by A9;
end;
dom ([:b:].(x,(Frege u).x)) = dom a by CARD_3:9;
hence [:b:].(x,(Frege u).x) = the_unity_wrt [:b:] by A7,A5,CARD_3:9;
dom ([:b:].((Frege u).x,x)) = dom a by CARD_3:9;
hence [:b:].((Frege u).x,x) = the_unity_wrt [:b:] by A7,A8,CARD_3:9;
end;
begin :: The Product of Groups
definition ::: non-empty-addLoopStr-yielding should be replaced
::: by non-Empty addLoopStr-yielding
let F be Relation;
attr F is non-empty-addLoopStr-yielding means :DefAA:
x in rng F implies x is non empty addLoopStr;
attr F is AbGroup-yielding means :Def9:
x in rng F implies x is AbGroup;
end;
registration
cluster AbGroup-yielding -> non-empty-addLoopStr-yielding for Relation;
coherence;
end;
registration
cluster non-empty-addLoopStr-yielding ->
non-Empty 1-sorted-yielding for Relation;
coherence
proof
let R be Relation;
assume
A1: R is non-empty-addLoopStr-yielding; then
a2: for x being object st x in rng R holds x is 1-sorted;
for S being 1-sorted st S in rng R holds S is non empty by A1;
hence thesis by a2,WAYBEL_3:def 7,PRALG_1:def 11;
end;
end;
registration
cluster non empty AbGroup-yielding for FinSequence;
existence
proof
set A = the AbGroup;
take <*A*>;
thus <*A*> is non empty;
let x;
assume that
A1: x in rng <*A*> and
A2: not x is AbGroup;
x in {A} by A1,FINSEQ_1:38;
hence contradiction by A2,TARSKI:def 1;
end;
end;
definition
mode Group-Sequence is non empty AbGroup-yielding FinSequence;
end;
definition
let g be non empty non-empty-addLoopStr-yielding FinSequence;
let i be Element of dom g;
redefine func g.i -> non empty addLoopStr; :: redefines . (FUNCT_1, definition)
coherence
proof
g.i in rng g by FUNCT_1:def 3;
hence thesis by DefAA;
end;
end;
definition
let g be Group-Sequence;
let i be Element of dom g;
redefine func g.i -> AbGroup; :: redefines . (FUNCT_1, definition)
coherence
proof
g.i in rng g by FUNCT_1:def 3;
hence thesis by Def9;
end;
end;
notation let g be non empty non-Empty 1-sorted-yielding FinSequence;
synonym carr g for Carrier g;
end;
registration let f be 1-sorted-yielding FinSequence;
cluster Carrier f -> FinSequence-like;
coherence
proof
consider n being Nat such that
A1: dom f = Seg n by FINSEQ_1:def 2;
ex n being Nat st dom Carrier f = Seg n by A1,PRALG_1:def 14;
hence thesis by FINSEQ_1:def 2;
end;
end;
registration let f be non empty 1-sorted-yielding Function;
cluster Carrier f -> non empty;
coherence
proof
dom f = dom Carrier f by PRALG_1:def 14;
hence thesis;
end;
end;
registration let f be non-Empty 1-sorted-yielding Function;
cluster Carrier f -> non-empty;
coherence
proof
A0: dom f = dom Carrier f by PRALG_1:def 14;
for x being object st x in dom Carrier f holds
(Carrier f).x is non empty
proof
let x be object;
assume
A1: x in dom Carrier f; then
A5: f.x in rng f by A0,FUNCT_1:3; then
reconsider S = f.x as 1-sorted by PRALG_1:def 11;
A6: S is non empty by A5,WAYBEL_3:def 7;
consider R being 1-sorted such that
A2: R = f.x and
A3: (Carrier f).x = the carrier of R by PRALG_1:def 14,A0,A1;
thus thesis by A3,A2,A6;
end;
hence thesis;
end;
end;
definition
let g be non empty non-Empty 1-sorted-yielding FinSequence;
redefine func carr g -> Domain-Sequence means :Def10: :: redefines carr (PRVECT_1, synonym) → Carrier (PRALG_1, definition)
len it = len g &
for j be Element of dom g holds it.j = the carrier of g.j;
coherence;
compatibility
proof
let f be Domain-Sequence;
thus f = carr g implies
len f = len g &
for j be Element of dom g holds f.j = the carrier of g.j
proof
assume
a0: f = carr g;
for j be Element of dom g holds f.j = the carrier of g.j
proof
let j be Element of dom g;
consider R being 1-sorted such that
A2: R = g.j & f.j = the carrier of R by a0,PRALG_1:def 14;
thus thesis by A2;
end;
hence thesis by a0,FINSEQ_3:29,PRALG_1:def 14;
end;
assume
B1: len f = len g &
for j be Element of dom g holds f.j = the carrier of g.j;
for j be set st j in dom g
ex R being 1-sorted st R = g.j & f.j = the carrier of R
proof
let j be set;
assume
B3: j in dom g; then
reconsider R = g.j as 1-sorted by PRALG_1:def 12;
take R;
thus thesis by B1,B3;
end;
hence thesis by B1,PRALG_1:def 14,FINSEQ_3:29;
end;
end;
reserve g for Group-Sequence,
i for Element of dom carr g;
definition
let g be non empty non-empty-addLoopStr-yielding FinSequence;
let i be Element of dom carr g;
redefine func g.i -> non empty addLoopStr; :: redefines . (FUNCT_1, definition)
coherence
proof
dom g = Seg len g & Seg len(carr g) = dom carr g by FINSEQ_1:def 3;
then reconsider i9 = i as Element of dom g by Def10;
g.i9 is non empty addLoopStr;
hence thesis;
end;
end;
definition
let g,i;
redefine func g.i -> AbGroup; :: redefines . (FUNCT_1, definition)
coherence
proof
dom g = Seg len g & Seg len(carr g) = dom carr g by FINSEQ_1:def 3;
then reconsider i9 = i as Element of dom g by Def10;
g.i9 is AbGroup;
hence thesis;
end;
end;
definition
let g be non-empty-addLoopStr-yielding non empty FinSequence;
func addop g -> BinOps of carr g means :Def11:
len it = len carr g & for i being Element of dom carr g holds
it.i = the addF of g.i;
existence
proof
deffunc F(Element of dom carr g) = the addF of g.$1;
consider p being non empty FinSequence such that
A1: len p = len carr g & for i being Element of dom carr g
holds p.i = F(i) from NEFinSeqLambda;
now
let i be Element of dom carr g;
len g = len carr g by Def10;
then reconsider j = i as Element of dom g by FINSEQ_3:29;
p.i = the addF of g.i & the carrier of g.j = (carr g).j by A1,Def10;
hence p.i is BinOp of (carr g).i;
end;
then reconsider p9 = p as BinOps of carr g by A1,Th11;
take p9;
thus thesis by A1;
end;
uniqueness
proof
let f,h be BinOps of carr g;
assume that
A2: len f = len carr g and
A3: for i be Element of dom carr g holds f.i = the addF of g.i and
A4: len h = len carr g and
A5: for i be Element of dom carr g holds h.i = the addF of g.i;
reconsider f9 = f,h9 = h as FinSequence;
A6: now
let i be Nat;
assume i in dom f9;
then reconsider i9 = i as Element of dom carr g by A2,FINSEQ_3:29;
f9.i = the addF of g.i9 by A3;
hence f9.i = h9.i by A5;
end;
dom f9 = Seg len f9 & dom h9 = Seg len h9 by FINSEQ_1:def 3;
hence thesis by A2,A4,A6;
end;
end;
definition
let g be non-empty-addLoopStr-yielding non empty FinSequence;
func complop g -> UnOps of carr g means :Def12:
len it = len carr g &
for i being Element of dom carr g holds it.i = comp g.i;
existence
proof
deffunc F(Element of dom carr g) = comp g.$1;
consider p being non empty FinSequence such that
A7: len p = len carr g & for i being Element of dom carr g
holds p.i = F(i) from NEFinSeqLambda;
now
let i be Element of dom carr g;
len g = len (carr g) by Def10;
then reconsider j = i as Element of dom g by FINSEQ_3:29;
p.i = comp g.i & the carrier of g.j = (carr g).j by A7,Def10;
hence p.i is UnOp of (carr g).i;
end;
then reconsider p9 = p as UnOps of carr g by A7,Th12;
take p9;
thus thesis by A7;
end;
uniqueness
proof
let f,h be UnOps of carr g;
assume that
A8: len f = len carr g and
A9: for i being Element of dom carr g holds f.i = comp g.i and
A10: len h = len carr g and
A11: for i being Element of dom carr g holds h.i = comp g.i;
reconsider f9 = f,h9 = h as FinSequence;
A12: now
let i be Nat;
assume i in dom f9;
then reconsider i9 = i as Element of dom carr g by A8,FINSEQ_3:29;
f.i = comp g.i9 by A9;
hence f.i = h.i by A11;
end;
dom f9 = Seg len f9 & dom h9 = Seg len h9 by FINSEQ_1:def 3;
hence thesis by A8,A10,A12;
end;
func zeros g -> Element of product carr g means :Def13:
for i being Element of dom carr g holds it.i = 0.(g.i);
existence
proof
deffunc F(Element of dom carr g) = 0.(g.$1);
A13: dom (carr g) = Seg len (carr g) by FINSEQ_1:def 3;
consider p being non empty FinSequence such that
A14: len p = len carr g &
for i being Element of dom carr g holds p.i = F(i) from NEFinSeqLambda;
A15: dom g = Seg len g by FINSEQ_1:def 3;
A16: now
let i be object;
assume i in dom (carr g);
then reconsider x = i as Element of dom carr g;
reconsider x9 = x as Element of dom g by A15,A13,Def10;
p.x = 0.(g.x) & (carr g).x9 = the carrier of g.x9 by A14,Def10;
hence p.i in (carr g).i;
end;
dom p = Seg len p by FINSEQ_1:def 3;
then reconsider t = p as Element of product carr g
by A14,FINSEQ_1:def 3,A16,CARD_3:9;
take t;
thus thesis by A14;
end;
uniqueness
proof
let f,h be Element of product carr g;
assume that
A17: for i be Element of dom carr g holds f.i = 0.(g.i) and
A18: for i be Element of dom carr g holds h.i = 0.(g.i);
reconsider f9 = f, h9 = h as Function;
A19: now
let x be object;
assume x in dom carr g;
then reconsider i = x as Element of dom carr g;
thus f9.x = 0.(g.i) by A17
.= h9.x by A18;
end;
dom f9 = dom carr g & dom h9 = dom carr g by CARD_3:9;
hence thesis by A19;
end;
end;
definition
let G be non-empty-addLoopStr-yielding non empty FinSequence;
func product G -> strict non empty addLoopStr equals
addLoopStr (# product carr G, [:addop G:], zeros G #);
coherence;
end;
registration
let G be Group-Sequence;
cluster product G ->
add-associative right_zeroed right_complementable non empty Abelian;
coherence
proof
reconsider GS = addLoopStr (# product carr G, [:addop G:], zeros G #) as
non empty addLoopStr;
A1: now
let i be Element of dom carr G;
dom G = Seg len G by FINSEQ_1:def 3
.= Seg len carr G by Def10
.= dom carr G by FINSEQ_1:def 3;
hence (carr G).i = car(G.i) by Def10;
end;
now
let i be Element of dom carr G;
(addop G).i = ad(G.i) & (carr G).i = car(G.i) by A1,Def11;
hence (addop G).i is associative by FVSUM_1:2;
end; then
A2: [:addop G:] is associative by Th18;
now
let i be Element of dom carr G;
A3: (carr G).i = car(G. i ) by A1;
(addop G).i = ad(G.i) & (zeros G).i = zr(G.i) by Def11,Def13;
hence (zeros G).i is_a_unity_wrt (addop G).i by A3,Th1;
end; then
A4: zeros G is_a_unity_wrt [:addop G:] by Th19;
A5: GS is right_complementable
proof
let x be Element of GS;
reconsider y = (Frege complop G).x as Element of GS by FUNCT_2:5;
take y;
now
let i be Element of dom carr G;
A6: (addop G).i = ad(G.i) & (complop G).i = cc(G.i) by Def11,Def12;
zr(G.i) is_a_unity_wrt ad(G.i) & (carr G).i = car(G.i) by A1,Th1;
hence (complop G).i is_an_inverseOp_wrt (addop G).i & (addop G).i is
having_a_unity by A6,Th2,SETWISEO:def 2;
end;
then Frege complop G is_an_inverseOp_wrt [:addop G:] by Th20;
then x + y = the_unity_wrt [:addop G:];
hence thesis by A4,BINOP_1:def 8;
end;
now
let i be Element of dom carr G;
(addop G).i = ad(G.i) & (carr G).i = car(G.i) by A1,Def11;
hence (addop G).i is commutative by FVSUM_1:1;
end;
then 0.GS = zeros G & [:addop G:] is commutative by Th17;
hence thesis by A2,A4,A5,BINOP_1:3;
end;
end;