let DL be distributive upper-bounded Lattice; :: thesis: for B being Element of Fin the carrier of DL
for p being Element of DL
for f being UnOp of the carrier of DL holds the L_join of DL . (( the L_meet of DL $$ (B,f)),p) = the L_meet of DL $$ (B,( the L_join of DL [:] (f,p)))
let B be Element of Fin the carrier of DL; :: thesis: for p being Element of DL
for f being UnOp of the carrier of DL holds the L_join of DL . (( the L_meet of DL $$ (B,f)),p) = the L_meet of DL $$ (B,( the L_join of DL [:] (f,p)))
let p be Element of DL; :: thesis: for f being UnOp of the carrier of DL holds the L_join of DL . (( the L_meet of DL $$ (B,f)),p) = the L_meet of DL $$ (B,( the L_join of DL [:] (f,p)))
let f be UnOp of the carrier of DL; :: thesis: the L_join of DL . (( the L_meet of DL $$ (B,f)),p) = the L_meet of DL $$ (B,( the L_join of DL [:] (f,p)))
set J = the L_join of DL;
set M = the L_meet of DL;
now :: thesis: the L_join of DL . (( the L_meet of DL $$ (B,f)),p) = the L_meet of DL $$ (B,( the L_join of DL [:] (f,p)))
per cases ( B <> {} or B = {} ) ;
suppose B <> {} ; :: thesis: the L_join of DL . (( the L_meet of DL $$ (B,f)),p) = the L_meet of DL $$ (B,( the L_join of DL [:] (f,p)))
hence the L_join of DL . (( the L_meet of DL $$ (B,f)),p) = the L_meet of DL $$ (B,( the L_join of DL [:] (f,p))) by LATTICE2:21, SETWISEO:28; :: thesis: verum
end;
suppose A1: B = {} ; :: thesis: the L_join of DL . (( the L_meet of DL $$ (B,f)),p) = the L_meet of DL $$ (B,( the L_join of DL [:] (f,p)))
A2: now :: thesis: for f being UnOp of the carrier of DL holds the L_meet of DL $$ (B,f) = Top DL
let f be UnOp of the carrier of DL; :: thesis: the L_meet of DL $$ (B,f) = Top DL
thus the L_meet of DL $$ (B,f) = FinMeet (({}. the carrier of DL),f) by A1, LATTICE2:def 4
.= Top DL by Lm2 ; :: thesis: verum
end;
hence the L_join of DL . (( the L_meet of DL $$ (B,f)),p) = (Top DL) "\/" p
.= Top DL
.= the L_meet of DL $$ (B,( the L_join of DL [:] (f,p))) by A2 ;
:: thesis: verum
end;
end;
end;
hence the L_join of DL . (( the L_meet of DL $$ (B,f)),p) = the L_meet of DL $$ (B,( the L_join of DL [:] (f,p))) ; :: thesis: verum