deffunc H1( object , object ) -> object = [$2,$1];
let I, J, D be non empty set ; for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
let F, G be BinOp of D; for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
let f be Function of I,D; for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
let g be Function of J,D; for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
let X be Element of Fin I; for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
let Y be Element of Fin J; ( F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative implies F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f))) )
assume A1:
( F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) )
; ( not G is commutative or F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f))) )
consider h being Function such that
A2:
( dom h = [:J,I:] & ( for x, y being object st x in J & y in I holds
h . (x,y) = H1(x,y) ) )
from FUNCT_3:sch 2();
now for z1, z2 being object st z1 in dom h & z2 in dom h & h . z1 = h . z2 holds
z1 = z2let z1,
z2 be
object ;
( z1 in dom h & z2 in dom h & h . z1 = h . z2 implies z1 = z2 )assume that A3:
z1 in dom h
and A4:
z2 in dom h
and A5:
h . z1 = h . z2
;
z1 = z2consider x2,
y2 being
object such that A6:
z2 = [x2,y2]
by A2, A4, RELAT_1:def 1;
(
x2 in J &
y2 in I )
by A2, A4, A6, ZFMISC_1:87;
then A7:
h . (
x2,
y2)
= [y2,x2]
by A2;
consider x1,
y1 being
object such that A8:
z1 = [x1,y1]
by A2, A3, RELAT_1:def 1;
(
x1 in J &
y1 in I )
by A2, A3, A8, ZFMISC_1:87;
then A9:
h . (
x1,
y1)
= [y1,x1]
by A2;
then
y1 = y2
by A5, A8, A6, A7, XTUPLE_0:1;
hence
z1 = z2
by A5, A8, A6, A9, A7, XTUPLE_0:1;
verum end;
then A10:
h is one-to-one
by FUNCT_1:def 4;
A11:
for x being object st x in [:J,I:] holds
h . x in [:I,J:]
proof
let x be
object ;
( x in [:J,I:] implies h . x in [:I,J:] )
assume A12:
x in [:J,I:]
;
h . x in [:I,J:]
then consider y,
z being
object such that A13:
x = [y,z]
by RELAT_1:def 1;
A14:
(
y in J &
z in I )
by A12, A13, ZFMISC_1:87;
then
h . (
y,
z)
= [z,y]
by A2;
hence
h . x in [:I,J:]
by A13, A14, ZFMISC_1:87;
verum
end;
assume A15:
G is commutative
; F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
A16:
G * (g,f) = (G * (f,g)) * h
proof
reconsider G =
G as
Function of
[:D,D:],
D ;
A17:
dom (G * (g,f)) = [:J,I:]
by FUNCT_2:def 1;
A18:
dom (G * (f,g)) = [:I,J:]
by FUNCT_2:def 1;
A19:
for
x being
object holds
(
x in dom (G * (g,f)) iff (
x in dom h &
h . x in dom (G * (f,g)) ) )
proof
let x be
object ;
( x in dom (G * (g,f)) iff ( x in dom h & h . x in dom (G * (f,g)) ) )
thus
(
x in dom (G * (g,f)) implies (
x in dom h &
h . x in dom (G * (f,g)) ) )
( x in dom h & h . x in dom (G * (f,g)) implies x in dom (G * (g,f)) )proof
assume A20:
x in dom (G * (g,f))
;
( x in dom h & h . x in dom (G * (f,g)) )
then consider y,
z being
object such that A21:
x = [y,z]
by RELAT_1:def 1;
A22:
(
y in J &
z in I )
by A17, A20, A21, ZFMISC_1:87;
then
h . (
y,
z)
= [z,y]
by A2;
hence
(
x in dom h &
h . x in dom (G * (f,g)) )
by A2, A18, A21, A22, ZFMISC_1:87;
verum
end;
assume that A23:
x in dom h
and
h . x in dom (G * (f,g))
;
x in dom (G * (g,f))
thus
x in dom (G * (g,f))
by A2, A23, FUNCT_2:def 1;
verum
end;
for
x being
object st
x in dom (G * (g,f)) holds
(G * (g,f)) . x = (G * (f,g)) . (h . x)
proof
let x be
object ;
( x in dom (G * (g,f)) implies (G * (g,f)) . x = (G * (f,g)) . (h . x) )
assume A24:
x in dom (G * (g,f))
;
(G * (g,f)) . x = (G * (f,g)) . (h . x)
then consider y,
z being
object such that A25:
x = [y,z]
by RELAT_1:def 1;
reconsider z =
z as
Element of
I by A17, A24, A25, ZFMISC_1:87;
reconsider y =
y as
Element of
J by A17, A24, A25, ZFMISC_1:87;
A26:
[z,y] in dom (G * (f,g))
by A18, ZFMISC_1:87;
A27:
[y,z] in dom (G * (g,f))
by A17, ZFMISC_1:87;
thus (G * (f,g)) . (h . x) =
(G * (f,g)) . (h . (y,z))
by A25
.=
(G * (f,g)) . (
z,
y)
by A2
.=
G . (
(f . z),
(g . y))
by A26, FINSEQOP:77
.=
G . (
(g . y),
(f . z))
by A15
.=
(G * (g,f)) . (
y,
z)
by A27, FINSEQOP:77
.=
(G * (g,f)) . x
by A25
;
verum
end;
hence
G * (
g,
f)
= (G * (f,g)) * h
by A19, FUNCT_1:10;
verum
end;
A28:
( X c= I & Y c= J )
by FINSUB_1:def 5;
for y being object holds
( y in [:X,Y:] iff y in h .: [:Y,X:] )
proof
let y be
object ;
( y in [:X,Y:] iff y in h .: [:Y,X:] )
thus
(
y in [:X,Y:] implies
y in h .: [:Y,X:] )
( y in h .: [:Y,X:] implies y in [:X,Y:] )proof
assume A29:
y in [:X,Y:]
;
y in h .: [:Y,X:]
then consider y1,
x1 being
object such that A30:
y = [y1,x1]
by RELAT_1:def 1;
A31:
(
y1 in X &
x1 in Y )
by A29, A30, ZFMISC_1:87;
then A32:
(
[x1,y1] in [:Y,X:] &
[x1,y1] in dom h )
by A28, A2, ZFMISC_1:87;
h . (
x1,
y1)
= y
by A28, A2, A30, A31;
hence
y in h .: [:Y,X:]
by A32, FUNCT_1:def 6;
verum
end;
assume
y in h .: [:Y,X:]
;
y in [:X,Y:]
then consider x being
object such that
x in dom h
and A33:
x in [:Y,X:]
and A34:
y = h . x
by FUNCT_1:def 6;
consider x1,
y1 being
object such that A35:
x = [x1,y1]
by A33, RELAT_1:def 1;
A36:
(
x1 in Y &
y1 in X )
by A33, A35, ZFMISC_1:87;
y = h . (
x1,
y1)
by A34, A35;
then
y = [y1,x1]
by A28, A2, A36;
hence
y in [:X,Y:]
by A36, ZFMISC_1:87;
verum
end;
then A37:
h .: [:Y,X:] = [:X,Y:]
by TARSKI:2;
reconsider h = h as Function of [:J,I:],[:I,J:] by A2, A11, FUNCT_2:3;
F $$ ([:X,Y:],(G * (f,g))) =
F $$ ([:Y,X:],((G * (f,g)) * h))
by A1, A10, A37, SETWOP_2:6
.=
F $$ ([:Y,X:],(G * (g,f)))
by A16
;
hence
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
; verum