let I, J, D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) )
; :: thesis: ( not G is commutative or F $$ [:X,Y:],(G * f,g) = F $$ [:Y,X:],(G * g,f) )
assume A2:
G is commutative
; :: thesis: F $$ [:X,Y:],(G * f,g) = F $$ [:Y,X:],(G * g,f)
A3:
( X c= I & Y c= J )
by FINSUB_1:def 5;
deffunc H1( set , set ) -> set = [$2,$1];
consider h being Function such that
A4:
( dom h = [:J,I:] & ( for x, y being set st x in J & y in I holds
h . x,y = H1(x,y) ) )
from FUNCT_3:sch 2();
A5:
h is one-to-one
proof
now let z1,
z2 be
set ;
:: thesis: ( z1 in dom h & z2 in dom h & h . z1 = h . z2 implies z1 = z2 )assume A6:
(
z1 in dom h &
z2 in dom h &
h . z1 = h . z2 )
;
:: thesis: z1 = z2then consider x1,
y1 being
set such that A7:
z1 = [x1,y1]
by A4, RELAT_1:def 1;
consider x2,
y2 being
set such that A8:
z2 = [x2,y2]
by A4, A6, RELAT_1:def 1;
A9:
(
x1 in J &
y1 in I &
x2 in J &
y2 in I )
by A4, A6, A7, A8, ZFMISC_1:106;
then A10:
h . x1,
y1 = [y1,x1]
by A4;
h . x2,
y2 = [y2,x2]
by A4, A9;
then
(
y1 = y2 &
x1 = x2 )
by A6, A7, A8, A10, ZFMISC_1:33;
hence
z1 = z2
by A7, A8;
:: thesis: verum end;
hence
h is
one-to-one
by FUNCT_1:def 8;
:: thesis: verum
end;
A11:
h .: [:Y,X:] = [:X,Y:]
proof
for
y being
set holds
(
y in [:X,Y:] iff
y in h .: [:Y,X:] )
proof
let y be
set ;
:: thesis: ( y in [:X,Y:] iff y in h .: [:Y,X:] )
thus
(
y in [:X,Y:] implies
y in h .: [:Y,X:] )
:: thesis: ( y in h .: [:Y,X:] implies y in [:X,Y:] )proof
assume A12:
y in [:X,Y:]
;
:: thesis: y in h .: [:Y,X:]
then consider y1,
x1 being
set such that A13:
y = [y1,x1]
by RELAT_1:def 1;
A14:
(
y1 in X &
x1 in Y )
by A12, A13, ZFMISC_1:106;
then A15:
[x1,y1] in [:Y,X:]
by ZFMISC_1:106;
A16:
[x1,y1] in dom h
by A3, A4, A14, ZFMISC_1:106;
h . x1,
y1 = y
by A3, A4, A13, A14;
hence
y in h .: [:Y,X:]
by A15, A16, FUNCT_1:def 12;
:: thesis: verum
end;
assume
y in h .: [:Y,X:]
;
:: thesis: y in [:X,Y:]
then consider x being
set such that A17:
(
x in dom h &
x in [:Y,X:] &
y = h . x )
by FUNCT_1:def 12;
consider x1,
y1 being
set such that A18:
x = [x1,y1]
by A17, RELAT_1:def 1;
A19:
y = h . x1,
y1
by A17, A18;
A20:
(
x1 in Y &
y1 in X )
by A17, A18, ZFMISC_1:106;
then
y = [y1,x1]
by A3, A4, A19;
hence
y in [:X,Y:]
by A20, ZFMISC_1:106;
:: thesis: verum
end;
hence
h .: [:Y,X:] = [:X,Y:]
by TARSKI:2;
:: thesis: verum
end;
A21:
for x being set st x in [:J,I:] holds
h . x in [:I,J:]
proof
let x be
set ;
:: thesis: ( x in [:J,I:] implies h . x in [:I,J:] )
assume A22:
x in [:J,I:]
;
:: thesis: h . x in [:I,J:]
then consider y,
z being
set such that A23:
x = [y,z]
by RELAT_1:def 1;
A24:
(
y in J &
z in I )
by A22, A23, ZFMISC_1:106;
then
h . y,
z = [z,y]
by A4;
hence
h . x in [:I,J:]
by A23, A24, ZFMISC_1:106;
:: thesis: verum
end;
A25:
G * g,f = (G * f,g) * h
proof
reconsider G =
G as
Function of
[:D,D:],
D ;
A26:
dom (G * f,g) = [:I,J:]
by FUNCT_2:def 1;
A27:
dom (G * g,f) = [:J,I:]
by FUNCT_2:def 1;
( ( for
x being
set holds
(
x in dom (G * g,f) iff (
x in dom h &
h . x in dom (G * f,g) ) ) ) & ( for
x being
set st
x in dom (G * g,f) holds
(G * g,f) . x = (G * f,g) . (h . x) ) )
proof
thus
for
x being
set holds
(
x in dom (G * g,f) iff (
x in dom h &
h . x in dom (G * f,g) ) )
:: thesis: for x being set st x in dom (G * g,f) holds
(G * g,f) . x = (G * f,g) . (h . x)proof
let x be
set ;
:: thesis: ( 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) ) )
:: thesis: ( x in dom h & h . x in dom (G * f,g) implies x in dom (G * g,f) )proof
assume A28:
x in dom (G * g,f)
;
:: thesis: ( x in dom h & h . x in dom (G * f,g) )
then consider y,
z being
set such that A29:
x = [y,z]
by RELAT_1:def 1;
A30:
(
y in J &
z in I )
by A27, A28, A29, ZFMISC_1:106;
then
h . y,
z = [z,y]
by A4;
hence
(
x in dom h &
h . x in dom (G * f,g) )
by A4, A26, A29, A30, ZFMISC_1:106;
:: thesis: verum
end;
assume
(
x in dom h &
h . x in dom (G * f,g) )
;
:: thesis: x in dom (G * g,f)
hence
x in dom (G * g,f)
by A4, FUNCT_2:def 1;
:: thesis: verum
end;
thus
for
x being
set st
x in dom (G * g,f) holds
(G * g,f) . x = (G * f,g) . (h . x)
:: thesis: verumproof
let x be
set ;
:: thesis: ( x in dom (G * g,f) implies (G * g,f) . x = (G * f,g) . (h . x) )
assume A31:
x in dom (G * g,f)
;
:: thesis: (G * g,f) . x = (G * f,g) . (h . x)
then consider y,
z being
set such that A32:
x = [y,z]
by RELAT_1:def 1;
reconsider y =
y as
Element of
J by A27, A31, A32, ZFMISC_1:106;
reconsider z =
z as
Element of
I by A27, A31, A32, ZFMISC_1:106;
A33:
(
[z,y] in dom (G * f,g) &
[y,z] in dom (G * g,f) )
by A26, A27, ZFMISC_1:106;
thus (G * f,g) . (h . x) =
(G * f,g) . (h . y,z)
by A32
.=
(G * f,g) . z,
y
by A4
.=
G . (f . z),
(g . y)
by A33, FINSEQOP:82
.=
G . (g . y),
(f . z)
by A2, BINOP_1:def 2
.=
(G * g,f) . y,
z
by A33, FINSEQOP:82
.=
(G * g,f) . x
by A32
;
:: thesis: verum
end;
thus
verum
;
:: thesis: verum
end;
hence
G * g,
f = (G * f,g) * h
by FUNCT_1:20;
:: thesis: verum
end;
reconsider h = h as Function of [:J,I:],[:I,J:] by A4, A21, FUNCT_2:5;
F $$ [:X,Y:],(G * f,g) =
F $$ [:Y,X:],((G * f,g) * h)
by A1, A5, A11, SETWOP_2:8
.=
F $$ [:Y,X:],(G * g,f)
by A25
;
hence
F $$ [:X,Y:],(G * f,g) = F $$ [:Y,X:],(G * g,f)
; :: thesis: verum