Metamath Proof Explorer

Theorem paddval

Description: Projective subspace sum operation value. (Contributed by NM, 29-Dec-2011)

Ref Expression
Hypotheses paddfval.l ⊢≤˙=≤K
paddfval.j ⊢∨˙=join⁡K
paddfval.a ⊢A=Atoms⁡K
paddfval.p ⊢+˙=+𝑃⁡K
Assertion paddval ⊢K∈B∧X⊆A∧Y⊆A→X+˙Y=X∪Y∪p∈A|∃q∈X∃r∈Yp≤˙q∨˙r

Proof

Step Hyp Ref Expression
1 paddfval.l ⊢≤˙=≤K
2 paddfval.j ⊢∨˙=join⁡K
3 paddfval.a ⊢A=Atoms⁡K
4 paddfval.p ⊢+˙=+𝑃⁡K
5 biid ⊢K∈B↔K∈B
6 3 fvexi ⊢A∈V
7 6 elpw2 ⊢X∈𝒫A↔X⊆A
8 6 elpw2 ⊢Y∈𝒫A↔Y⊆A
9 1 2 3 4 paddfval ⊢K∈B→+˙=m∈𝒫A,n∈𝒫A⟼m∪n∪p∈A|∃q∈m∃r∈np≤˙q∨˙r
10 9 oveqd ⊢K∈B→X+˙Y=Xm∈𝒫A,n∈𝒫A⟼m∪n∪p∈A|∃q∈m∃r∈np≤˙q∨˙rY
11 10 3ad2ant1 ⊢K∈B∧X∈𝒫A∧Y∈𝒫A→X+˙Y=Xm∈𝒫A,n∈𝒫A⟼m∪n∪p∈A|∃q∈m∃r∈np≤˙q∨˙rY
12 simpl ⊢X∈𝒫A∧Y∈𝒫A→X∈𝒫A
13 simpr ⊢X∈𝒫A∧Y∈𝒫A→Y∈𝒫A
14 unexg ⊢X∈𝒫A∧Y∈𝒫A→X∪Y∈V
15 6 rabex ⊢p∈A|∃q∈X∃r∈Yp≤˙q∨˙r∈V
16 unexg ⊢X∪Y∈V∧p∈A|∃q∈X∃r∈Yp≤˙q∨˙r∈V→X∪Y∪p∈A|∃q∈X∃r∈Yp≤˙q∨˙r∈V
17 14 15 16 sylancl ⊢X∈𝒫A∧Y∈𝒫A→X∪Y∪p∈A|∃q∈X∃r∈Yp≤˙q∨˙r∈V
18 12 13 17 3jca ⊢X∈𝒫A∧Y∈𝒫A→X∈𝒫A∧Y∈𝒫A∧X∪Y∪p∈A|∃q∈X∃r∈Yp≤˙q∨˙r∈V
19 18 3adant1 ⊢K∈B∧X∈𝒫A∧Y∈𝒫A→X∈𝒫A∧Y∈𝒫A∧X∪Y∪p∈A|∃q∈X∃r∈Yp≤˙q∨˙r∈V
20 uneq1 ⊢m=X→m∪n=X∪n
21 rexeq ⊢m=X→∃q∈m∃r∈np≤˙q∨˙r↔∃q∈X∃r∈np≤˙q∨˙r
22 21 rabbidv ⊢m=X→p∈A|∃q∈m∃r∈np≤˙q∨˙r=p∈A|∃q∈X∃r∈np≤˙q∨˙r
23 20 22 uneq12d ⊢m=X→m∪n∪p∈A|∃q∈m∃r∈np≤˙q∨˙r=X∪n∪p∈A|∃q∈X∃r∈np≤˙q∨˙r
24 uneq2 ⊢n=Y→X∪n=X∪Y
25 rexeq ⊢n=Y→∃r∈np≤˙q∨˙r↔∃r∈Yp≤˙q∨˙r
26 25 rexbidv ⊢n=Y→∃q∈X∃r∈np≤˙q∨˙r↔∃q∈X∃r∈Yp≤˙q∨˙r
27 26 rabbidv ⊢n=Y→p∈A|∃q∈X∃r∈np≤˙q∨˙r=p∈A|∃q∈X∃r∈Yp≤˙q∨˙r
28 24 27 uneq12d ⊢n=Y→X∪n∪p∈A|∃q∈X∃r∈np≤˙q∨˙r=X∪Y∪p∈A|∃q∈X∃r∈Yp≤˙q∨˙r
29 eqid ⊢m∈𝒫A,n∈𝒫A⟼m∪n∪p∈A|∃q∈m∃r∈np≤˙q∨˙r=m∈𝒫A,n∈𝒫A⟼m∪n∪p∈A|∃q∈m∃r∈np≤˙q∨˙r
30 23 28 29 ovmpog ⊢X∈𝒫A∧Y∈𝒫A∧X∪Y∪p∈A|∃q∈X∃r∈Yp≤˙q∨˙r∈V→Xm∈𝒫A,n∈𝒫A⟼m∪n∪p∈A|∃q∈m∃r∈np≤˙q∨˙rY=X∪Y∪p∈A|∃q∈X∃r∈Yp≤˙q∨˙r
31 19 30 syl ⊢K∈B∧X∈𝒫A∧Y∈𝒫A→Xm∈𝒫A,n∈𝒫A⟼m∪n∪p∈A|∃q∈m∃r∈np≤˙q∨˙rY=X∪Y∪p∈A|∃q∈X∃r∈Yp≤˙q∨˙r
32 11 31 eqtrd ⊢K∈B∧X∈𝒫A∧Y∈𝒫A→X+˙Y=X∪Y∪p∈A|∃q∈X∃r∈Yp≤˙q∨˙r
33 5 7 8 32 syl3anbr ⊢K∈B∧X⊆A∧Y⊆A→X+˙Y=X∪Y∪p∈A|∃q∈X∃r∈Yp≤˙q∨˙r