let X, Y be non empty set ; for F being BinOp of Y st F is commutative & F is associative & F is idempotent holds
for f, g being Function of X,Y
for A, B being Element of Fin X st A <> {} & f .: A = g .: B holds
F $$ (A,f) = F $$ (B,g)
let F be BinOp of Y; ( F is commutative & F is associative & F is idempotent implies for f, g being Function of X,Y
for A, B being Element of Fin X st A <> {} & f .: A = g .: B holds
F $$ (A,f) = F $$ (B,g) )
assume that
A1:
F is commutative
and
A2:
F is associative
and
A3:
F is idempotent
; for f, g being Function of X,Y
for A, B being Element of Fin X st A <> {} & f .: A = g .: B holds
F $$ (A,f) = F $$ (B,g)
let f, g be Function of X,Y; for A, B being Element of Fin X st A <> {} & f .: A = g .: B holds
F $$ (A,f) = F $$ (B,g)
defpred S1[ Element of Fin X] means ( $1 <> {} implies for B being Element of Fin X st f .: $1 = g .: B holds
F $$ ($1,f) = F $$ (B,g) );
A4:
for B9 being Element of Fin X
for b being Element of X st S1[B9] holds
S1[B9 \/ {.b.}]
proof
let A be
Element of
Fin X;
for b being Element of X st S1[A] holds
S1[A \/ {.b.}]let x be
Element of
X;
( S1[A] implies S1[A \/ {.x.}] )
assume A5:
(
A <> {} implies for
B being
Element of
Fin X st
f .: A = g .: B holds
F $$ (
A,
f)
= F $$ (
B,
g) )
;
S1[A \/ {.x.}]
assume
A \/ {x} <> {}
;
for B being Element of Fin X st f .: (A \/ {.x.}) = g .: B holds
F $$ ((A \/ {.x.}),f) = F $$ (B,g)
let B be
Element of
Fin X;
( f .: (A \/ {.x.}) = g .: B implies F $$ ((A \/ {.x.}),f) = F $$ (B,g) )
assume A6:
f .: (A \/ {x}) = g .: B
;
F $$ ((A \/ {.x.}),f) = F $$ (B,g)
per cases
( f . x in f .: A or not f . x in f .: A )
;
suppose
f . x in f .: A
;
F $$ ((A \/ {.x.}),f) = F $$ (B,g)then consider x9 being
Element of
X such that A7:
x9 in A
and A8:
f . x9 = f . x
by FUNCT_2:65;
A9:
g .: B =
(f .: A) \/ (Im (f,x))
by A6, RELAT_1:120
.=
(f .: A) \/ {(f . x)}
by Th5
.=
f .: A
by A7, A8, FUNCT_2:35, ZFMISC_1:40
;
thus F $$ (
(A \/ {.x.}),
f) =
F . (
(F $$ (A,f)),
(f . x))
by A1, A2, A3, A7, Th17
.=
F . (
(F $$ ((A \/ {.x9.}),f)),
(f . x))
by A7, ZFMISC_1:40
.=
F . (
(F . ((F $$ (A,f)),(f . x9))),
(f . x))
by A1, A2, A3, A7, Th17
.=
F . (
(F $$ (A,f)),
(F . ((f . x9),(f . x9))))
by A2, A8
.=
F $$ (
(A \/ {.x9.}),
f)
by A1, A2, A3, A7, Th17
.=
F $$ (
A,
f)
by A7, ZFMISC_1:40
.=
F $$ (
B,
g)
by A5, A7, A9
;
verum end; suppose A10:
not
f . x in f .: A
;
F $$ ((A \/ {.x.}),f) = F $$ (B,g)per cases
( A = {} or A <> {} )
;
suppose A11:
A = {}
;
F $$ ((A \/ {.x.}),f) = F $$ (B,g)then A12:
g .: B =
Im (
f,
x)
by A6
.=
{(f . x)}
by Th5
;
thus F $$ (
(A \/ {.x.}),
f) =
f . x
by A1, A2, A11, Th14
.=
F $$ (
B,
g)
by A1, A2, A3, A12, Th22
;
verum end; suppose A13:
A <> {}
;
F $$ ((A \/ {.x.}),f) = F $$ (B,g)reconsider B1 =
B \ (g " {(f . x)}) as
Element of
Fin X by Th8;
reconsider B2 =
B /\ (g " {(f . x)}) as
Element of
Fin X by Th8, XBOOLE_1:17;
A16:
B = B1 \/ B2
by XBOOLE_1:51;
A17:
for
b being
Element of
X st
b in B2 holds
g . b = f . x
A18:
f .: A =
(f .: A) \ {(f . x)}
by A10, ZFMISC_1:57
.=
(f .: A) \ (Im (f,x))
by Th5
.=
((f .: A) \/ (f .: {x})) \ (f .: {x})
by XBOOLE_1:40
.=
(f .: (A \/ {x})) \ (Im (f,x))
by RELAT_1:120
.=
(g .: B) \ {(f . x)}
by A6, Th5
.=
g .: B1
by Th3
;
x in A \/ {x}
by ZFMISC_1:136;
then consider x9 being
Element of
X such that A19:
x9 in B
and A20:
g . x9 = f . x
by A6, FUNCT_2:35, FUNCT_2:65;
x9 in g " {(f . x)}
by A20, Th4;
then A21:
B2 <> {}
by A19, XBOOLE_0:def 4;
thus F $$ (
(A \/ {.x.}),
f) =
F . (
(F $$ (A,f)),
(f . x))
by A1, A2, A3, A13, Th17
.=
F . (
(F $$ (B1,g)),
(f . x))
by A5, A13, A18
.=
F . (
(F $$ (B1,g)),
(F $$ (B2,g)))
by A1, A2, A3, A21, A17, Th21
.=
F $$ (
B,
g)
by A1, A2, A3, A16, A14, A21, Th18
;
verum end;
end;
A22:
S1[ {}. X]
;
A23:
for A being Element of Fin X holds S1[A]
from SETWISEO:sch 4(A22, A4);
let A, B be Element of Fin X; ( A <> {} & f .: A = g .: B implies F $$ (A,f) = F $$ (B,g) )
assume
( A <> {} & f .: A = g .: B )
; F $$ (A,f) = F $$ (B,g)
hence
F $$ (A,f) = F $$ (B,g)
by A23; verum