let D1, D2 be non empty set ; for f1, g1 being BinOp of D1
for f2, g2 being BinOp of D2 holds
( ( f1 absorbs g1 & f2 absorbs g2 ) iff |:f1,f2:| absorbs |:g1,g2:| )
let f1, g1 be BinOp of D1; for f2, g2 being BinOp of D2 holds
( ( f1 absorbs g1 & f2 absorbs g2 ) iff |:f1,f2:| absorbs |:g1,g2:| )
let f2, g2 be BinOp of D2; ( ( f1 absorbs g1 & f2 absorbs g2 ) iff |:f1,f2:| absorbs |:g1,g2:| )
defpred S1[ set , set ] means |:f1,f2:| . ($1,(|:g1,g2:| . ($1,$2))) = $1;
thus
( f1 absorbs g1 & f2 absorbs g2 implies |:f1,f2:| absorbs |:g1,g2:| )
( |:f1,f2:| absorbs |:g1,g2:| implies ( f1 absorbs g1 & f2 absorbs g2 ) )proof
assume A1:
for
a1,
b1 being
Element of
D1 holds
f1 . (
a1,
(g1 . (a1,b1)))
= a1
;
LATTICE2:def 1 ( not f2 absorbs g2 or |:f1,f2:| absorbs |:g1,g2:| )
assume A2:
for
a2,
b2 being
Element of
D2 holds
f2 . (
a2,
(g2 . (a2,b2)))
= a2
;
LATTICE2:def 1 |:f1,f2:| absorbs |:g1,g2:|
A3:
for
d1,
d19 being
Element of
D1 for
d2,
d29 being
Element of
D2 holds
S1[
[d1,d2],
[d19,d29]]
proof
let a1,
b1 be
Element of
D1;
for d2, d29 being Element of D2 holds S1[[a1,d2],[b1,d29]]let a2,
b2 be
Element of
D2;
S1[[a1,a2],[b1,b2]]
thus |:f1,f2:| . (
[a1,a2],
(|:g1,g2:| . ([a1,a2],[b1,b2]))) =
|:f1,f2:| . (
[a1,a2],
[(g1 . (a1,b1)),(g2 . (a2,b2))])
by Th21
.=
[(f1 . (a1,(g1 . (a1,b1)))),(f2 . (a2,(g2 . (a2,b2))))]
by Th21
.=
[a1,(f2 . (a2,(g2 . (a2,b2))))]
by A1
.=
[a1,a2]
by A2
;
verum
end;
thus
for
a,
b being
Element of
[:D1,D2:] holds
S1[
a,
b]
from FILTER_1:sch 5(A3); LATTICE2:def 1 verum
end;
assume A4:
for a, b being Element of [:D1,D2:] holds |:f1,f2:| . (a,(|:g1,g2:| . (a,b))) = a
; LATTICE2:def 1 ( f1 absorbs g1 & f2 absorbs g2 )
thus
for a1, b1 being Element of D1 holds f1 . (a1,(g1 . (a1,b1))) = a1
LATTICE2:def 1 f2 absorbs g2proof
set a2 = the
Element of
D2;
let a1,
b1 be
Element of
D1;
f1 . (a1,(g1 . (a1,b1))) = a1
[a1, the Element of D2] =
|:f1,f2:| . (
[a1, the Element of D2],
(|:g1,g2:| . ([a1, the Element of D2],[b1, the Element of D2])))
by A4
.=
|:f1,f2:| . (
[a1, the Element of D2],
[(g1 . (a1,b1)),(g2 . ( the Element of D2, the Element of D2))])
by Th21
.=
[(f1 . (a1,(g1 . (a1,b1)))),(f2 . ( the Element of D2,(g2 . ( the Element of D2, the Element of D2))))]
by Th21
;
hence
f1 . (
a1,
(g1 . (a1,b1)))
= a1
by XTUPLE_0:1;
verum
end;
set a1 = the Element of D1;
let a2 be Element of D2; LATTICE2:def 1 for b1 being Element of D2 holds f2 . (a2,(g2 . (a2,b1))) = a2
let b2 be Element of D2; f2 . (a2,(g2 . (a2,b2))) = a2
[ the Element of D1,a2] =
|:f1,f2:| . ([ the Element of D1,a2],(|:g1,g2:| . ([ the Element of D1,a2],[ the Element of D1,b2])))
by A4
.=
|:f1,f2:| . ([ the Element of D1,a2],[(g1 . ( the Element of D1, the Element of D1)),(g2 . (a2,b2))])
by Th21
.=
[(f1 . ( the Element of D1,(g1 . ( the Element of D1, the Element of D1)))),(f2 . (a2,(g2 . (a2,b2))))]
by Th21
;
hence
f2 . (a2,(g2 . (a2,b2))) = a2
by XTUPLE_0:1; verum