let B be B_Lattice; :: thesis: for a being Element of B holds B,[:(B /\/ <.a.)),():] are_isomorphic
let a be Element of B; :: thesis: B,[:(B /\/ <.a.)),():] are_isomorphic
set F = <.a.);
set E = equivalence_wrt <.a.);
deffunc H3( object ) -> Element of bool the carrier of B = Class (,\$1);
consider g being Function such that
A1: ( dom g = the carrier of B & ( for x being object st x in the carrier of B holds
g . x = H3(x) ) ) from A2: for b being Element of B holds (b "\/" (b <=> a)) <=> b = b "\/" a
proof
let b be Element of B; :: thesis: (b "\/" (b <=> a)) <=> b = b "\/" a
A3: (b "\/" (b <=> a)) ` = (b `) "/\" ((b <=> a) `) by LATTICES:24;
A4: (b `) "/\" ((b "/\" (a `)) "\/" ((b `) "/\" a)) = ((b `) "/\" (b "/\" (a `))) "\/" ((b `) "/\" ((b `) "/\" a)) by LATTICES:def 11;
A5: b "\/" ((b "/\" a) "\/" ((b `) "/\" (a `))) = (b "\/" (b "/\" a)) "\/" ((b `) "/\" (a `)) by LATTICES:def 5;
A6: b <=> a = (b "/\" a) "\/" ((b `) "/\" (a `)) by Th50;
A7: (b `) "/\" b = Bottom B by LATTICES:20;
A8: (b `) "/\" ((a `) "/\" b) = ((b `) "/\" (a `)) "/\" b by LATTICES:def 7;
A9: (b `) "/\" ((b `) "/\" a) = ((b `) "/\" (b `)) "/\" a by LATTICES:def 7;
A10: (b <=> a) ` = (b "/\" (a `)) "\/" ((b `) "/\" a) by Th51;
A11: (b `) "/\" (b "/\" (a `)) = ((b `) "/\" b) "/\" (a `) by LATTICES:def 7;
A12: (b "\/" ((b `) "/\" (a `))) "/\" b = (b "/\" b) "\/" (((b `) "/\" (a `)) "/\" b) by LATTICES:def 11;
A13: (b "/\" a) "\/" b = b by LATTICES:def 8;
(b "\/" (b <=> a)) <=> b = ((b "\/" (b <=> a)) "/\" b) "\/" (((b "\/" (b <=> a)) `) "/\" (b `)) by Th50;
hence (b "\/" (b <=> a)) <=> b = b "\/" ((b "/\" a) "\/" ((b `) "/\" a)) by A3, A10, A4, A11, A7, A9, A6, A5, A13, A12, A8, LATTICES:def 5
.= b "\/" ((b "\/" (b `)) "/\" a) by LATTICES:def 11
.= b "\/" ((Top B) "/\" a) by LATTICES:21
.= b "\/" a ;
:: thesis: verum
end;
set S = LattRel [:(B /\/ <.a.)),():];
A14: field (LattRel [:(B /\/ <.a.)),():]) = the carrier of [:(B /\/ <.a.)),():] by Th32;
reconsider o1 = H1(B), o2 = H2(B) as BinOp of equivalence_wrt <.a.) by ;
A15: LattStr(# (),(o1 /\/ ),(o2 /\/ ) #) = B /\/ <.a.) by Def5;
set R = LattRel B;
deffunc H4( Element of B) -> Element of the carrier of B = (\$1 "\/" (\$1 <=> a)) <=> \$1;
consider h being UnOp of the carrier of B such that
A16: for b being Element of B holds h . b = H4(b) from take f = <:g,h:>; :: according to WELLORD1:def 8,FILTER_1:def 9 :: thesis: f is_isomorphism_of LattRel B, LattRel [:(B /\/ <.a.)),():]
A17: field () = the carrier of B by Th32;
A18: dom h = dom g by ;
hence A19: dom f = field () by ; :: according to WELLORD1:def 7 :: thesis: ( rng f = field (LattRel [:(B /\/ <.a.)),():]) & f is one-to-one & ( for b1, b2 being object holds
( ( not [b1,b2] in LattRel B or ( b1 in field () & b2 in field () & [(f . b1),(f . b2)] in LattRel [:(B /\/ <.a.)),():] ) ) & ( not b1 in field () or not b2 in field () or not [(f . b1),(f . b2)] in LattRel [:(B /\/ <.a.)),():] or [b1,b2] in LattRel B ) ) ) )

A20: for b being Element of B holds h . b is Element of ()
proof
let b be Element of B; :: thesis: h . b is Element of ()
b "\/" (b <=> a) in Class (,b) by Th60;
then [(b "\/" (b <=> a)),b] in equivalence_wrt <.a.) by EQREL_1:19;
then A21: (b "\/" (b <=> a)) <=> b in <.a.) by FILTER_0:def 11;
h . b = (b "\/" (b <=> a)) <=> b by A16;
hence h . b is Element of () by ; :: thesis: verum
end;
thus rng f c= field (LattRel [:(B /\/ <.a.)),():]) :: according to XBOOLE_0:def 10 :: thesis: ( field (LattRel [:(B /\/ <.a.)),():]) c= rng f & f is one-to-one & ( for b1, b2 being object holds
( ( not [b1,b2] in LattRel B or ( b1 in field () & b2 in field () & [(f . b1),(f . b2)] in LattRel [:(B /\/ <.a.)),():] ) ) & ( not b1 in field () or not b2 in field () or not [(f . b1),(f . b2)] in LattRel [:(B /\/ <.a.)),():] or [b1,b2] in LattRel B ) ) ) )
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in field (LattRel [:(B /\/ <.a.)),():]) )
assume x in rng f ; :: thesis: x in field (LattRel [:(B /\/ <.a.)),():])
then consider y being object such that
A22: y in dom f and
A23: x = f . y by FUNCT_1:def 3;
reconsider y = y as Element of B by ;
reconsider z2 = h . y as Element of () by A20;
g . y = EqClass (,y) by A1;
then reconsider z1 = g . y as Element of (B /\/ <.a.)) by A15;
x = [z1,z2] by ;
hence x in field (LattRel [:(B /\/ <.a.)),():]) by A14; :: thesis: verum
end;
A24: the carrier of () = <.a.) by FILTER_0:49;
thus field (LattRel [:(B /\/ <.a.)),():]) c= rng f :: thesis: ( f is one-to-one & ( for b1, b2 being object holds
( ( not [b1,b2] in LattRel B or ( b1 in field () & b2 in field () & [(f . b1),(f . b2)] in LattRel [:(B /\/ <.a.)),():] ) ) & ( not b1 in field () or not b2 in field () or not [(f . b1),(f . b2)] in LattRel [:(B /\/ <.a.)),():] or [b1,b2] in LattRel B ) ) ) )
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in field (LattRel [:(B /\/ <.a.)),():]) or x in rng f )
assume x in field (LattRel [:(B /\/ <.a.)),():]) ; :: thesis: x in rng f
then consider y being Element of Class , z being Element of <.a.) such that
A25: x = [y,z] by ;
consider b being Element of B such that
A26: y = Class (,b) by EQREL_1:36;
set ty = b "\/" (b <=> a);
(b "\/" (b <=> a)) <=> ((b "\/" (b <=> a)) <=> z) = z by Th53;
then ((b "\/" (b <=> a)) <=> z) <=> (b "\/" (b <=> a)) = z ;
then A27: [((b "\/" (b <=> a)) <=> z),(b "\/" (b <=> a))] in equivalence_wrt <.a.) by FILTER_0:def 11;
b "\/" (b <=> a) in y by ;
then y = Class (,(b "\/" (b <=> a))) by ;
then A28: (b "\/" (b <=> a)) <=> z in y by ;
then A29: y = Class (,((b "\/" (b <=> a)) <=> z)) by ;
then A30: b "\/" (b <=> a) [= ((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) by ;
y = Class (,((b "\/" (b <=> a)) <=> z)) by ;
then A31: g . ((b "\/" (b <=> a)) <=> z) = y by A1;
((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) [= b "\/" (b <=> a) by ;
then A32: ((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) = b "\/" (b <=> a) by ;
h . ((b "\/" (b <=> a)) <=> z) = (((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a)) <=> ((b "\/" (b <=> a)) <=> z) by A16;
then h . ((b "\/" (b <=> a)) <=> z) = z by ;
then x = f . ((b "\/" (b <=> a)) <=> z) by ;
hence x in rng f by ; :: thesis: verum
end;
thus f is one-to-one :: thesis: for b1, b2 being object holds
( ( not [b1,b2] in LattRel B or ( b1 in field () & b2 in field () & [(f . b1),(f . b2)] in LattRel [:(B /\/ <.a.)),():] ) ) & ( not b1 in field () or not b2 in field () or not [(f . b1),(f . b2)] in LattRel [:(B /\/ <.a.)),():] or [b1,b2] in LattRel B ) )
proof
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A33: x in dom f and
A34: y in dom f ; :: thesis: ( not f . x = f . y or x = y )
reconsider x9 = x, y9 = y as Element of B by ;
assume A35: f . x = f . y ; :: thesis: x = y
A36: g . y9 = Class (,y9) by A1;
A37: h . y9 = (y9 "\/" (y9 <=> a)) <=> y9 by A16;
A38: h . x9 = (x9 "\/" (x9 <=> a)) <=> x9 by A16;
A39: g . x9 = Class (,x9) by A1;
A40: f . y = [(g . y9),(h . y9)] by ;
A41: f . x = [(g . x9),(h . x9)] by ;
then A42: g . x = g . y by ;
then A43: y9 "\/" (y9 <=> a) [= x9 "\/" (x9 <=> a) by ;
x9 "\/" (x9 <=> a) [= y9 "\/" (y9 <=> a) by ;
then A44: y9 "\/" (y9 <=> a) = x9 "\/" (x9 <=> a) by ;
h . x = h . y by ;
hence x = y by ; :: thesis: verum
end;
let x, y be object ; :: thesis: ( ( not [x,y] in LattRel B or ( x in field () & y in field () & [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),():] ) ) & ( not x in field () or not y in field () or not [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),():] or [x,y] in LattRel B ) )
A45: the carrier of () = <.a.) by FILTER_0:49;
thus ( [x,y] in LattRel B implies ( x in field () & y in field () & [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),():] ) ) :: thesis: ( not x in field () or not y in field () or not [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),():] or [x,y] in LattRel B )
proof
assume A46: [x,y] in LattRel B ; :: thesis: ( x in field () & y in field () & [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),():] )
then reconsider x9 = x, y9 = y as Element of B by ;
A47: x9 [= y9 by ;
thus ( x in field () & y in field () ) by ; :: thesis: [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),():]
A48: Top B in <.a.) by FILTER_0:11;
x9 "/\" (Top B) = x9 ;
then Top B [= x9 => y9 by ;
then x9 => y9 in <.a.) by A48;
then A49: x9 /\/ <.a.) [= y9 /\/ <.a.) by Th16;
A50: h . x9 = (x9 "\/" (x9 <=> a)) <=> x9 by A16;
A51: y9 "\/" (y9 <=> a) in Class (,y9) by Th60;
A52: (y9 "\/" (y9 <=> a)) <=> y9 = y9 "\/" a by A2;
A53: (x9 "\/" (x9 <=> a)) <=> x9 = x9 "\/" a by A2;
A54: h . y9 = (y9 "\/" (y9 <=> a)) <=> y9 by A16;
x9 "\/" (x9 <=> a) in Class (,x9) by Th60;
then reconsider hx = h . x, hy = h . y as Element of () by A45, A50, A54, A51, Lm4;
A55: Class (,x9) = g . x9 by A1;
x9 "\/" a [= y9 "\/" a by ;
then hx [= hy by ;
then A56: [(x9 /\/ <.a.)),hx] [= [(y9 /\/ <.a.)),hy] by ;
A57: y9 /\/ <.a.) = Class (,y9) by Def6;
A58: Class (,y9) = g . y9 by A1;
A59: f . y9 = [(g . y9),(h . y9)] by ;
A60: f . x9 = [(g . x9),(h . x9)] by ;
x9 /\/ <.a.) = Class (,x9) by Def6;
hence [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),():] by A55, A57, A58, A60, A59, A56; :: thesis: verum
end;
assume that
A61: x in field () and
A62: y in field () ; :: thesis: ( not [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),():] or [x,y] in LattRel B )
reconsider x9 = x, y9 = y as Element of B by ;
A63: h . x9 = (x9 "\/" (x9 <=> a)) <=> x9 by A16;
A64: f . y9 = [(g . y9),(h . y9)] by ;
A65: y9 /\/ <.a.) = Class (,y9) by Def6;
A66: Class (,x9) = g . x9 by A1;
A67: (y9 "\/" (y9 <=> a)) <=> y9 = y9 "\/" a by A2;
A68: (x9 "\/" (x9 <=> a)) <=> x9 = x9 "\/" a by A2;
A69: y9 "/\" x9 [= y9 by LATTICES:6;
A70: y9 "\/" (y9 <=> a) in Class (,y9) by Th60;
A71: h . y9 = (y9 "\/" (y9 <=> a)) <=> y9 by A16;
x9 "\/" (x9 <=> a) in Class (,x9) by Th60;
then reconsider hx = h . x, hy = h . y as Element of () by A45, A63, A71, A70, Lm4;
assume A72: [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),():] ; :: thesis: [x,y] in LattRel B
A73: f . x9 = [(g . x9),(h . x9)] by ;
A74: Class (,y9) = g . y9 by A1;
x9 /\/ <.a.) = Class (,x9) by Def6;
then A75: [(x9 /\/ <.a.)),hx] [= [(y9 /\/ <.a.)),hy] by A65, A66, A74, A73, A64, A72, Th31;
then x9 /\/ <.a.) [= y9 /\/ <.a.) by Th36;
then A76: x9 => y9 in <.a.) by Th16;
x9 => y9 = (x9 `) "\/" y9 by FILTER_0:42;
then a [= (x9 `) "\/" y9 by ;
then A77: x9 "/\" a [= x9 "/\" ((x9 `) "\/" y9) by LATTICES:9;
hx [= hy by ;
then x9 "\/" a [= y9 "\/" a by ;
then A78: x9 "/\" (x9 "\/" a) [= x9 "/\" (y9 "\/" a) by LATTICES:9;
A79: x9 "/\" (x9 `) = Bottom B by LATTICES:20;
x9 "/\" ((x9 `) "\/" y9) = (x9 "/\" (x9 `)) "\/" (x9 "/\" y9) by LATTICES:def 11;
then x9 "/\" a [= y9 by ;
then A80: (x9 "/\" y9) "\/" (x9 "/\" a) [= y9 by ;
x9 [= x9 "\/" a by LATTICES:5;
then x9 "/\" (x9 "\/" a) = x9 by LATTICES:4;
then x9 [= (x9 "/\" y9) "\/" (x9 "/\" a) by ;
then x9 [= y9 by ;
hence [x,y] in LattRel B ; :: thesis: verum