let D be non empty set ; :: thesis: for p, q, r being PartialPredicate of D holds PP_and (p,(PP_or (q,r))) = PP_or ((PP_and (p,q)),(PP_and (p,r)))
let p, q, r be PartialPredicate of D; :: thesis: PP_and (p,(PP_or (q,r))) = PP_or ((PP_and (p,q)),(PP_and (p,r)))
set qr = PP_or (q,r);
set a = PP_and (p,(PP_or (q,r)));
set pq = PP_and (p,q);
set pr = PP_and (p,r);
set b = PP_or ((PP_and (p,q)),(PP_and (p,r)));
A1: dom (PP_or (q,r)) = { d where d is Element of D : ( ( d in dom q & q . d = TRUE ) or ( d in dom r & r . d = TRUE ) or ( d in dom q & q . d = FALSE & d in dom r & r . d = FALSE ) ) } by Def4;
A2: dom (PP_and (p,(PP_or (q,r)))) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = TRUE ) ) } by Th16;
A3: dom (PP_and (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) ) } by Th16;
A4: dom (PP_and (p,r)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom r & r . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom r & r . d = TRUE ) ) } by Th16;
A5: dom (PP_or ((PP_and (p,q)),(PP_and (p,r)))) = { d where d is Element of D : ( ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = TRUE ) or ( d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = TRUE ) or ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = FALSE & d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = FALSE ) ) } by Def4;
thus dom (PP_and (p,(PP_or (q,r)))) = dom (PP_or ((PP_and (p,q)),(PP_and (p,r)))) :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom (PP_and (p,(PP_or (q,r)))) or (PP_and (p,(PP_or (q,r)))) . b1 = (PP_or ((PP_and (p,q)),(PP_and (p,r)))) . b1 )
proof
thus dom (PP_and (p,(PP_or (q,r)))) c= dom (PP_or ((PP_and (p,q)),(PP_and (p,r)))) :: according to XBOOLE_0:def 10 :: thesis: dom (PP_or ((PP_and (p,q)),(PP_and (p,r)))) c= dom (PP_and (p,(PP_or (q,r))))
proof
let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in dom (PP_and (p,(PP_or (q,r)))) or d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r)))) )
assume d in dom (PP_and (p,(PP_or (q,r)))) ; :: thesis: d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r))))
per cases then ( ( d in dom p & p . d = FALSE ) or ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = TRUE ) ) by Th17;
suppose ( d in dom p & p . d = FALSE ) ; :: thesis: d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r))))
then ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = FALSE & d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = FALSE ) by A3, A4, Th19;
hence d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r)))) by A5; :: thesis: verum
end;
suppose ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = FALSE ) ; :: thesis: d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r))))
then ( d in dom q & q . d = FALSE & d in dom r & r . d = FALSE ) by Th13;
then ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = FALSE & d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = FALSE ) by A3, A4, Th19;
hence d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r)))) by A5; :: thesis: verum
end;
suppose that A6: ( d in dom p & p . d = TRUE ) and
A7: ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = TRUE ) ; :: thesis: d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r))))
( ( d in dom q & q . d = TRUE ) or ( d in dom r & r . d = TRUE ) ) by A7, Th10;
then ( ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = TRUE ) or ( d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = TRUE ) ) by A3, A4, A6, Th18;
hence d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r)))) by A5; :: thesis: verum
end;
end;
end;
let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r)))) or d in dom (PP_and (p,(PP_or (q,r)))) )
assume d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r)))) ; :: thesis: d in dom (PP_and (p,(PP_or (q,r))))
per cases then ( ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = TRUE ) or ( d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = TRUE ) or ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = FALSE & d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = FALSE ) ) by Th8;
suppose A8: ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = TRUE ) ; :: thesis: d in dom (PP_and (p,(PP_or (q,r))))
then A9: ( d in dom p & p . d = TRUE ) by Th23;
( d in dom q & q . d = TRUE ) by A8, Th23;
then ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = TRUE ) by A1, Def4;
hence d in dom (PP_and (p,(PP_or (q,r)))) by A2, A9; :: thesis: verum
end;
suppose A10: ( d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = TRUE ) ; :: thesis: d in dom (PP_and (p,(PP_or (q,r))))
then A11: ( d in dom p & p . d = TRUE ) by Th23;
( d in dom r & r . d = TRUE ) by A10, Th23;
then ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = TRUE ) by A1, Def4;
hence d in dom (PP_and (p,(PP_or (q,r)))) by A2, A11; :: thesis: verum
end;
suppose ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = FALSE & d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = FALSE ) ; :: thesis: d in dom (PP_and (p,(PP_or (q,r))))
then ( ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = FALSE ) ) & ( ( d in dom p & p . d = FALSE ) or ( d in dom r & r . d = FALSE ) ) ) by Th25;
then ( ( d in dom p & p . d = FALSE ) or ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = FALSE ) ) by A1, Def4;
hence d in dom (PP_and (p,(PP_or (q,r)))) by A2; :: thesis: verum
end;
end;
end;
let d be object ; :: thesis: ( not d in dom (PP_and (p,(PP_or (q,r)))) or (PP_and (p,(PP_or (q,r)))) . d = (PP_or ((PP_and (p,q)),(PP_and (p,r)))) . d )
assume d in dom (PP_and (p,(PP_or (q,r)))) ; :: thesis: (PP_and (p,(PP_or (q,r)))) . d = (PP_or ((PP_and (p,q)),(PP_and (p,r)))) . d
per cases then ( ( d in dom p & p . d = FALSE ) or ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = TRUE ) ) by Th17;
suppose A12: ( d in dom p & p . d = FALSE ) ; :: thesis: (PP_and (p,(PP_or (q,r)))) . d = (PP_or ((PP_and (p,q)),(PP_and (p,r)))) . d
then ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = FALSE & d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = FALSE ) by A3, A4, Th19;
hence (PP_or ((PP_and (p,q)),(PP_and (p,r)))) . d = FALSE by Def4
.= (PP_and (p,(PP_or (q,r)))) . d by A12, Th19 ;
:: thesis: verum
end;
suppose A13: ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = FALSE ) ; :: thesis: (PP_and (p,(PP_or (q,r)))) . d = (PP_or ((PP_and (p,q)),(PP_and (p,r)))) . d
then ( d in dom q & q . d = FALSE & d in dom r & r . d = FALSE ) by Th13;
then ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = FALSE & d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = FALSE ) by A3, A4, Th19;
hence (PP_or ((PP_and (p,q)),(PP_and (p,r)))) . d = FALSE by Def4
.= (PP_and (p,(PP_or (q,r)))) . d by A13, Th19 ;
:: thesis: verum
end;
suppose that A14: ( d in dom p & p . d = TRUE ) and
A15: ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = TRUE ) ; :: thesis: (PP_and (p,(PP_or (q,r)))) . d = (PP_or ((PP_and (p,q)),(PP_and (p,r)))) . d
( ( d in dom q & q . d = TRUE ) or ( d in dom r & r . d = TRUE ) ) by A15, Th10;
then ( ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = TRUE ) or ( d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = TRUE ) ) by A3, A4, A14, Th18;
hence (PP_or ((PP_and (p,q)),(PP_and (p,r)))) . d = TRUE by Def4
.= (PP_and (p,(PP_or (q,r)))) . d by A14, A15, Th18 ;
:: thesis: verum
end;
end;