let D1, D2 be non empty set ; :: thesis: for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( f1 is commutative & f2 is commutative ) iff |:f1,f2:| is commutative )
let f1 be BinOp of D1; :: thesis: for f2 being BinOp of D2 holds
( ( f1 is commutative & f2 is commutative ) iff |:f1,f2:| is commutative )
let f2 be BinOp of D2; :: thesis: ( ( f1 is commutative & f2 is commutative ) iff |:f1,f2:| is commutative )
defpred S1[ set , set ] means |:f1,f2:| . $1,$2 = |:f1,f2:| . $2,$1;
thus
( f1 is commutative & f2 is commutative implies |:f1,f2:| is commutative )
:: thesis: ( |:f1,f2:| is commutative implies ( f1 is commutative & f2 is commutative ) )proof
assume A1:
for
a,
b being
Element of
D1 holds
f1 . a,
b = f1 . b,
a
;
:: according to BINOP_1:def 13 :: thesis: ( not f2 is commutative or |:f1,f2:| is commutative )
assume A2:
for
a,
b being
Element of
D2 holds
f2 . a,
b = f2 . b,
a
;
:: according to BINOP_1:def 13 :: thesis: |:f1,f2:| is commutative
A3:
for
d1,
d1' being
Element of
D1 for
d2,
d2' being
Element of
D2 holds
S1[
[d1,d2],
[d1',d2']]
proof
let a1,
b1 be
Element of
D1;
:: thesis: for d2, d2' being Element of D2 holds S1[[a1,d2],[b1,d2']]let a2,
b2 be
Element of
D2;
:: thesis: S1[[a1,a2],[b1,b2]]
thus |:f1,f2:| . [a1,a2],
[b1,b2] =
[(f1 . a1,b1),(f2 . a2,b2)]
by Th22
.=
[(f1 . b1,a1),(f2 . a2,b2)]
by A1
.=
[(f1 . b1,a1),(f2 . b2,a2)]
by A2
.=
|:f1,f2:| . [b1,b2],
[a1,a2]
by Th22
;
:: thesis: verum
end;
thus
for
a,
b being
Element of
[:D1,D2:] holds
S1[
a,
b]
from FILTER_1:sch 5(A3); :: according to BINOP_1:def 13 :: thesis: verum
end;
assume A4:
for a, b being Element of [:D1,D2:] holds |:f1,f2:| . a,b = |:f1,f2:| . b,a
; :: according to BINOP_1:def 13 :: thesis: ( f1 is commutative & f2 is commutative )
thus
for a, b being Element of D1 holds f1 . a,b = f1 . b,a
:: according to BINOP_1:def 13 :: thesis: f2 is commutative proof
let a1,
b1 be
Element of
D1;
:: thesis: f1 . a1,b1 = f1 . b1,a1
consider a2,
b2 being
Element of
D2;
[(f1 . a1,b1),(f2 . a2,b2)] =
|:f1,f2:| . [a1,a2],
[b1,b2]
by Th22
.=
|:f1,f2:| . [b1,b2],
[a1,a2]
by A4
.=
[(f1 . b1,a1),(f2 . b2,a2)]
by Th22
;
hence
f1 . a1,
b1 = f1 . b1,
a1
by ZFMISC_1:33;
:: thesis: verum
end;
let a2 be Element of D2; :: according to BINOP_1:def 13 :: thesis: for b1 being Element of D2 holds f2 . a2,b1 = f2 . b1,a2
let b2 be Element of D2; :: thesis: f2 . a2,b2 = f2 . b2,a2
consider a1, b1 being Element of D1;
[(f1 . a1,b1),(f2 . a2,b2)] =
|:f1,f2:| . [a1,a2],[b1,b2]
by Th22
.=
|:f1,f2:| . [b1,b2],[a1,a2]
by A4
.=
[(f1 . b1,a1),(f2 . b2,a2)]
by Th22
;
hence
f2 . a2,b2 = f2 . b2,a2
by ZFMISC_1:33; :: thesis: verum