let BL be Boolean Lattice; :: thesis: for B being Element of Fin the carrier of BL holds (FinJoin B) ` = FinMeet (B,(comp BL))

let B be Element of Fin the carrier of BL; :: thesis: (FinJoin B) ` = FinMeet (B,(comp BL))

set M = the L_meet of BL;

set J = the L_join of BL;

A1: for a, b being Element of BL holds (comp BL) . ( the L_join of BL . (a,b)) = the L_meet of BL . (((comp BL) . a),((comp BL) . b))

.= (Bottom BL) ` by LATTICE2:52

.= Top BL by Th30

.= the_unity_wrt the L_meet of BL by LATTICE2:57 ;

thus (FinJoin B) ` = ( the L_join of BL $$ (B,(id BL))) ` by LATTICE2:def 3

.= (comp BL) . ( the L_join of BL $$ (B,(id BL))) by Def12

.= the L_meet of BL $$ (B,((comp BL) * (id BL))) by A2, A1, SETWISEO:36

.= the L_meet of BL $$ (B,(comp BL)) by FUNCT_2:17

.= FinMeet (B,(comp BL)) by LATTICE2:def 4 ; :: thesis: verum

let B be Element of Fin the carrier of BL; :: thesis: (FinJoin B) ` = FinMeet (B,(comp BL))

set M = the L_meet of BL;

set J = the L_join of BL;

A1: for a, b being Element of BL holds (comp BL) . ( the L_join of BL . (a,b)) = the L_meet of BL . (((comp BL) . a),((comp BL) . b))

proof

A2: (comp BL) . (the_unity_wrt the L_join of BL) =
(the_unity_wrt the L_join of BL) `
by Def12
let a, b be Element of BL; :: thesis: (comp BL) . ( the L_join of BL . (a,b)) = the L_meet of BL . (((comp BL) . a),((comp BL) . b))

thus (comp BL) . ( the L_join of BL . (a,b)) = (a "\/" b) ` by Def12

.= (a `) "/\" (b `) by LATTICES:24

.= the L_meet of BL . (((comp BL) . a),(b `)) by Def12

.= the L_meet of BL . (((comp BL) . a),((comp BL) . b)) by Def12 ; :: thesis: verum

end;thus (comp BL) . ( the L_join of BL . (a,b)) = (a "\/" b) ` by Def12

.= (a `) "/\" (b `) by LATTICES:24

.= the L_meet of BL . (((comp BL) . a),(b `)) by Def12

.= the L_meet of BL . (((comp BL) . a),((comp BL) . b)) by Def12 ; :: thesis: verum

.= (Bottom BL) ` by LATTICE2:52

.= Top BL by Th30

.= the_unity_wrt the L_meet of BL by LATTICE2:57 ;

thus (FinJoin B) ` = ( the L_join of BL $$ (B,(id BL))) ` by LATTICE2:def 3

.= (comp BL) . ( the L_join of BL $$ (B,(id BL))) by Def12

.= the L_meet of BL $$ (B,((comp BL) * (id BL))) by A2, A1, SETWISEO:36

.= the L_meet of BL $$ (B,(comp BL)) by FUNCT_2:17

.= FinMeet (B,(comp BL)) by LATTICE2:def 4 ; :: thesis: verum