let D1, D2 be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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:| )
:: thesis: ( |: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
;
:: according to LATTICE2:def 1 :: thesis: ( 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
;
:: according to LATTICE2:def 1 :: thesis: |:f1,f2:| absorbs |:g1,g2:|
A3:
for
d1,
d1' being
Element of
D1 for
d2,
d2' being
Element of
D2 holds
S1[
[d1,d2],
[d1',d2']]
proof
let a1,
b1 be
Element of
D1;
:: thesis: for d2, d2' being Element of D2 holds S1[[a1,d2],[b1,d2']]let a2,
b2 be
Element of
D2;
:: thesis: 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 Th22
.=
[(f1 . a1,(g1 . a1,b1)),(f2 . a2,(g2 . a2,b2))]
by Th22
.=
[a1,(f2 . a2,(g2 . a2,b2))]
by A1
.=
[a1,a2]
by A2
;
:: thesis: verum
end;
thus
for
a,
b being
Element of
[:D1,D2:] holds
S1[
a,
b]
from FILTER_1:sch 5(A3); :: according to LATTICE2:def 1 :: thesis: verum
end;
assume A4:
for a, b being Element of [:D1,D2:] holds |:f1,f2:| . a,(|:g1,g2:| . a,b) = a
; :: according to LATTICE2:def 1 :: thesis: ( f1 absorbs g1 & f2 absorbs g2 )
thus
for a1, b1 being Element of D1 holds f1 . a1,(g1 . a1,b1) = a1
:: according to LATTICE2:def 1 :: thesis: f2 absorbs g2proof
let a1,
b1 be
Element of
D1;
:: thesis: f1 . a1,(g1 . a1,b1) = a1
consider a2,
b2 being
Element of
D2;
[a1,a2] =
|:f1,f2:| . [a1,a2],
(|:g1,g2:| . [a1,a2],[b1,b2])
by A4
.=
|:f1,f2:| . [a1,a2],
[(g1 . a1,b1),(g2 . a2,b2)]
by Th22
.=
[(f1 . a1,(g1 . a1,b1)),(f2 . a2,(g2 . a2,b2))]
by Th22
;
hence
f1 . a1,
(g1 . a1,b1) = a1
by ZFMISC_1:33;
:: thesis: verum
end;
let a2 be Element of D2; :: according to LATTICE2:def 1 :: thesis: for b1 being Element of D2 holds f2 . a2,(g2 . a2,b1) = a2
let b2 be Element of D2; :: thesis: f2 . a2,(g2 . a2,b2) = a2
consider a1, b1 being Element of D1;
[a1,a2] =
|:f1,f2:| . [a1,a2],(|:g1,g2:| . [a1,a2],[b1,b2])
by A4
.=
|:f1,f2:| . [a1,a2],[(g1 . a1,b1),(g2 . a2,b2)]
by Th22
.=
[(f1 . a1,(g1 . a1,b1)),(f2 . a2,(g2 . a2,b2))]
by Th22
;
hence
f2 . a2,(g2 . a2,b2) = a2
by ZFMISC_1:33; :: thesis: verum