let n be Nat; for D being non empty set
for B being BinOp of D
for C being UnOp of D st B is having_a_unity & B is associative & C is_an_inverseOp_wrt B holds
product (C,n) is_an_inverseOp_wrt product (B,n)
let D be non empty set ; for B being BinOp of D
for C being UnOp of D st B is having_a_unity & B is associative & C is_an_inverseOp_wrt B holds
product (C,n) is_an_inverseOp_wrt product (B,n)
let B be BinOp of D; for C being UnOp of D st B is having_a_unity & B is associative & C is_an_inverseOp_wrt B holds
product (C,n) is_an_inverseOp_wrt product (B,n)
let C be UnOp of D; ( 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) )
assume that
A1:
B is having_a_unity
and
A2:
B is associative
and
A3:
C is_an_inverseOp_wrt B
; product (C,n) is_an_inverseOp_wrt product (B,n)
A4:
B is having_an_inverseOp
by A3;
then A5:
C = the_inverseOp_wrt B
by A1, A2, A3, FINSEQOP:def 3;
A6:
now for f being Element of n -tuples_on D holds
( (product (B,n)) . (f,((product (C,n)) . f)) = n |-> (the_unity_wrt B) & (product (B,n)) . (((product (C,n)) . f),f) = n |-> (the_unity_wrt B) )let f be
Element of
n -tuples_on D;
( (product (B,n)) . (f,((product (C,n)) . f)) = n |-> (the_unity_wrt B) & (product (B,n)) . (((product (C,n)) . f),f) = n |-> (the_unity_wrt B) )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
;
(product (B,n)) . (((product (C,n)) . f),f) = n |-> (the_unity_wrt B)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
;
verum end;
ex d being Element of 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
product (C,n) is_an_inverseOp_wrt product (B,n)
by A6; verum