let n be Nat; for D being non empty set
for H, G being BinOp of D
for d being Element of D
for t1, t2 being Element of n -tuples_on D st H is_distributive_wrt G holds
H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))
let D be non empty set ; for H, G being BinOp of D
for d being Element of D
for t1, t2 being Element of n -tuples_on D st H is_distributive_wrt G holds
H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))
let H, G be BinOp of D; for d being Element of D
for t1, t2 being Element of n -tuples_on D st H is_distributive_wrt G holds
H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))
let d be Element of D; for t1, t2 being Element of n -tuples_on D st H is_distributive_wrt G holds
H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))
let t1, t2 be Element of n -tuples_on D; ( H is_distributive_wrt G implies H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2))) )
( rng (H * <:((dom t1) --> d),t1:>) c= rng H & rng (H * <:((dom t2) --> d),t2:>) c= rng H )
by RELAT_1:26;
then
( rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= [:(rng (H * <:((dom t1) --> d),t1:>)),(rng (H * <:((dom t2) --> d),t2:>)):] & [:(rng (H * <:((dom t1) --> d),t1:>)),(rng (H * <:((dom t2) --> d),t2:>)):] c= [:(rng H),(rng H):] )
by FUNCT_3:51, ZFMISC_1:96;
then A1:
rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= [:(rng H),(rng H):]
by XBOOLE_1:1;
rng H c= D
by RELAT_1:def 19;
then
[:(rng H),(rng H):] c= [:D,D:]
by ZFMISC_1:96;
then
rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= [:D,D:]
by A1, XBOOLE_1:1;
then A2:
rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= dom G
by FUNCT_2:def 1;
A3: dom t2 =
Seg (len t2)
by FINSEQ_1:def 3
.=
Seg n
by CARD_1:def 7
;
( rng t1 c= D & rng t2 c= D )
by FINSEQ_1:def 4;
then A4:
[:(rng t1),(rng t2):] c= [:D,D:]
by ZFMISC_1:96;
rng <:t1,t2:> c= [:(rng t1),(rng t2):]
by FUNCT_3:51;
then
rng <:t1,t2:> c= [:D,D:]
by A4, XBOOLE_1:1;
then A5:
rng <:t1,t2:> c= dom G
by FUNCT_2:def 1;
A6: dom ((dom t2) --> d) =
dom t2
by FUNCOP_1:13
.=
Seg (len t2)
by FINSEQ_1:def 3
.=
Seg n
by CARD_1:def 7
;
dom t1 =
Seg (len t1)
by FINSEQ_1:def 3
.=
Seg n
by CARD_1:def 7
;
then
dom <:t1,t2:> = Seg n
by A3, FUNCT_3:50;
then A7:
dom (G * <:t1,t2:>) = Seg n
by A5, RELAT_1:27;
then
dom ((dom (G * <:t1,t2:>)) --> d) = Seg n
by FUNCOP_1:13;
then A8:
dom <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> = Seg n
by A7, FUNCT_3:50;
rng t2 c= D
by FINSEQ_1:def 4;
then
( rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),(rng t2):] & [:(rng ((dom t2) --> d)),(rng t2):] c= [:(rng ((dom t2) --> d)),D:] )
by FUNCT_3:51, ZFMISC_1:96;
then A9:
rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),D:]
by XBOOLE_1:1;
rng ((dom t2) --> d) c= {d}
by FUNCOP_1:13;
then
[:(rng ((dom t2) --> d)),D:] c= [:{d},D:]
by ZFMISC_1:96;
then A10:
rng <:((dom t2) --> d),t2:> c= [:{d},D:]
by A9, XBOOLE_1:1;
A11: dom t1 =
Seg (len t1)
by FINSEQ_1:def 3
.=
Seg n
by CARD_1:def 7
;
rng t1 c= D
by FINSEQ_1:def 4;
then
( rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),(rng t1):] & [:(rng ((dom t1) --> d)),(rng t1):] c= [:(rng ((dom t1) --> d)),D:] )
by FUNCT_3:51, ZFMISC_1:96;
then A12:
rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),D:]
by XBOOLE_1:1;
rng ((dom t1) --> d) c= {d}
by FUNCOP_1:13;
then
[:(rng ((dom t1) --> d)),D:] c= [:{d},D:]
by ZFMISC_1:96;
then A13:
rng <:((dom t1) --> d),t1:> c= [:{d},D:]
by A12, XBOOLE_1:1;
A14: dom ((dom t1) --> d) =
dom t1
by FUNCOP_1:13
.=
Seg (len t1)
by FINSEQ_1:def 3
.=
Seg n
by CARD_1:def 7
;
{d} c= D
by ZFMISC_1:31;
then A15:
[:{d},D:] c= [:D,D:]
by ZFMISC_1:96;
( rng ((dom (G * <:t1,t2:>)) --> d) c= {d} & {d} c= D )
by FUNCOP_1:13, ZFMISC_1:31;
then A16:
rng ((dom (G * <:t1,t2:>)) --> d) c= D
by XBOOLE_1:1;
A17: dom t2 =
Seg (len t2)
by FINSEQ_1:def 3
.=
Seg n
by CARD_1:def 7
;
dom H = [:D,D:]
by FUNCT_2:def 1;
then A18: dom (H * <:((dom t2) --> d),t2:>) =
dom <:((dom t2) --> d),t2:>
by A10, A15, RELAT_1:27, XBOOLE_1:1
.=
Seg n
by A6, A17, FUNCT_3:50
;
{d} c= D
by ZFMISC_1:31;
then A19:
[:{d},D:] c= [:D,D:]
by ZFMISC_1:96;
set A = H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>;
dom H = [:D,D:]
by FUNCT_2:def 1;
then dom (H * <:((dom t1) --> d),t1:>) =
dom <:((dom t1) --> d),t1:>
by A13, A19, RELAT_1:27, XBOOLE_1:1
.=
Seg n
by A14, A11, FUNCT_3:50
;
then
dom <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> = Seg n
by A18, FUNCT_3:50;
then A20:
dom (G * <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):>) = Seg n
by A2, RELAT_1:27;
rng (G * <:t1,t2:>) c= D
by RELAT_1:def 19;
then
( rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= [:(rng ((dom (G * <:t1,t2:>)) --> d)),(rng (G * <:t1,t2:>)):] & [:(rng ((dom (G * <:t1,t2:>)) --> d)),(rng (G * <:t1,t2:>)):] c= [:D,D:] )
by A16, FUNCT_3:51, ZFMISC_1:96;
then
rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= [:D,D:]
by XBOOLE_1:1;
then A21:
rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= dom H
by FUNCT_2:def 1;
then A22:
dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) = Seg n
by A8, RELAT_1:27;
assume A23:
H is_distributive_wrt G
; H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))
for x being object st x in dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) holds
(H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x
proof
rng t1 c= D
by FINSEQ_1:def 4;
then
(
rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),(rng t1):] &
[:(rng ((dom t1) --> d)),(rng t1):] c= [:(rng ((dom t1) --> d)),D:] )
by FUNCT_3:51, ZFMISC_1:96;
then A24:
rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),D:]
by XBOOLE_1:1;
rng ((dom t1) --> d) c= {d}
by FUNCOP_1:13;
then
[:(rng ((dom t1) --> d)),D:] c= [:{d},D:]
by ZFMISC_1:96;
then A25:
rng <:((dom t1) --> d),t1:> c= [:{d},D:]
by A24, XBOOLE_1:1;
A26:
(
rng t1 c= D &
rng t2 c= D )
by FINSEQ_1:def 4;
{d} c= D
by ZFMISC_1:31;
then A27:
[:{d},D:] c= [:D,D:]
by ZFMISC_1:96;
A28:
dom ((dom t2) --> d) =
dom t2
by FUNCOP_1:13
.=
Seg (len t2)
by FINSEQ_1:def 3
.=
Seg n
by CARD_1:def 7
;
{d} c= D
by ZFMISC_1:31;
then A29:
[:{d},D:] c= [:D,D:]
by ZFMISC_1:96;
A30:
dom t1 =
Seg (len t1)
by FINSEQ_1:def 3
.=
Seg n
by CARD_1:def 7
;
rng t2 c= D
by FINSEQ_1:def 4;
then
(
rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),(rng t2):] &
[:(rng ((dom t2) --> d)),(rng t2):] c= [:(rng ((dom t2) --> d)),D:] )
by FUNCT_3:51, ZFMISC_1:96;
then A31:
rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),D:]
by XBOOLE_1:1;
rng ((dom t2) --> d) c= {d}
by FUNCOP_1:13;
then
[:(rng ((dom t2) --> d)),D:] c= [:{d},D:]
by ZFMISC_1:96;
then A32:
rng <:((dom t2) --> d),t2:> c= [:{d},D:]
by A31, XBOOLE_1:1;
A33:
dom ((dom t1) --> d) =
dom t1
by FUNCOP_1:13
.=
Seg (len t1)
by FINSEQ_1:def 3
.=
Seg n
by CARD_1:def 7
;
let x be
object ;
( x in dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) implies (H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x )
A34:
dom <:((dom (G .: (t1,t2))) --> d),(G .: (t1,t2)):> = (dom ((dom (G .: (t1,t2))) --> d)) /\ (dom (G .: (t1,t2)))
by FUNCT_3:def 7;
assume A35:
x in dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>)
;
(H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x
then
x in dom <:((dom (G .: (t1,t2))) --> d),(G .: (t1,t2)):>
by FUNCT_1:11;
then A36:
x in dom (G .: (t1,t2))
by A34, XBOOLE_0:def 4;
dom t1 =
Seg (len t1)
by FINSEQ_1:def 3
.=
Seg n
by CARD_1:def 7
;
then A37:
t1 . x in rng t1
by A22, A35, FUNCT_1:def 3;
A38:
dom t2 =
Seg (len t2)
by FINSEQ_1:def 3
.=
Seg n
by CARD_1:def 7
;
dom H = [:D,D:]
by FUNCT_2:def 1;
then dom (H * <:((dom t1) --> d),t1:>) =
dom <:((dom t1) --> d),t1:>
by A25, A29, RELAT_1:27, XBOOLE_1:1
.=
Seg n
by A33, A30, FUNCT_3:50
;
then A39:
x in dom (H [;] (d,t1))
by A22, A35;
dom t2 =
Seg (len t2)
by FINSEQ_1:def 3
.=
Seg n
by CARD_1:def 7
;
then A40:
t2 . x in rng t2
by A22, A35, FUNCT_1:def 3;
dom H = [:D,D:]
by FUNCT_2:def 1;
then dom (H * <:((dom t2) --> d),t2:>) =
dom <:((dom t2) --> d),t2:>
by A32, A27, RELAT_1:27, XBOOLE_1:1
.=
Seg n
by A28, A38, FUNCT_3:50
;
then A41:
x in dom (H [;] (d,t2))
by A22, A35;
(H [;] (d,(G .: (t1,t2)))) . x =
H . (
d,
((G .: (t1,t2)) . x))
by A35, FUNCOP_1:32
.=
H . (
d,
(G . ((t1 . x),(t2 . x))))
by A36, FUNCOP_1:22
.=
G . (
(H . (d,(t1 . x))),
(H . (d,(t2 . x))))
by A23, A37, A26, A40, BINOP_1:11
.=
G . (
((H [;] (d,t1)) . x),
(H . (d,(t2 . x))))
by A39, FUNCOP_1:32
.=
G . (
((H [;] (d,t1)) . x),
((H [;] (d,t2)) . x))
by A41, FUNCOP_1:32
.=
(G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x
by A22, A20, A35, FUNCOP_1:22
;
hence
(H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x
;
verum
end;
hence
H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))
by A8, A21, A20, RELAT_1:27; verum