Metamath Proof Explorer

Theorem paddfval

Description: Projective subspace sum operation. (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 paddfval ⊢K∈B→+˙=m∈𝒫A,n∈𝒫A⟼m∪n∪p∈A|∃q∈m∃r∈np≤˙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 elex ⊢K∈B→K∈V
6 fveq2 ⊢h=K→Atoms⁡h=Atoms⁡K
7 6 3 eqtr4di ⊢h=K→Atoms⁡h=A
8 7 pweqd ⊢h=K→𝒫Atoms⁡h=𝒫A
9 eqidd ⊢h=K→p=p
10 fveq2 ⊢h=K→≤h=≤K
11 10 1 eqtr4di ⊢h=K→≤h=≤˙
12 fveq2 ⊢h=K→join⁡h=join⁡K
13 12 2 eqtr4di ⊢h=K→join⁡h=∨˙
14 13 oveqd ⊢h=K→qjoin⁡hr=q∨˙r
15 9 11 14 breq123d ⊢h=K→p≤hqjoin⁡hr↔p≤˙q∨˙r
16 15 2rexbidv ⊢h=K→∃q∈m∃r∈np≤hqjoin⁡hr↔∃q∈m∃r∈np≤˙q∨˙r
17 7 16 rabeqbidv ⊢h=K→p∈Atoms⁡h|∃q∈m∃r∈np≤hqjoin⁡hr=p∈A|∃q∈m∃r∈np≤˙q∨˙r
18 17 uneq2d ⊢h=K→m∪n∪p∈Atoms⁡h|∃q∈m∃r∈np≤hqjoin⁡hr=m∪n∪p∈A|∃q∈m∃r∈np≤˙q∨˙r
19 8 8 18 mpoeq123dv ⊢h=K→m∈𝒫Atoms⁡h,n∈𝒫Atoms⁡h⟼m∪n∪p∈Atoms⁡h|∃q∈m∃r∈np≤hqjoin⁡hr=m∈𝒫A,n∈𝒫A⟼m∪n∪p∈A|∃q∈m∃r∈np≤˙q∨˙r
20 df-padd ⊢+𝑃=h∈V⟼m∈𝒫Atoms⁡h,n∈𝒫Atoms⁡h⟼m∪n∪p∈Atoms⁡h|∃q∈m∃r∈np≤hqjoin⁡hr
21 3 fvexi ⊢A∈V
22 21 pwex ⊢𝒫A∈V
23 22 22 mpoex ⊢m∈𝒫A,n∈𝒫A⟼m∪n∪p∈A|∃q∈m∃r∈np≤˙q∨˙r∈V
24 19 20 23 fvmpt ⊢K∈V→+𝑃⁡K=m∈𝒫A,n∈𝒫A⟼m∪n∪p∈A|∃q∈m∃r∈np≤˙q∨˙r
25 4 24 eqtrid ⊢K∈V→+˙=m∈𝒫A,n∈𝒫A⟼m∪n∪p∈A|∃q∈m∃r∈np≤˙q∨˙r
26 5 25 syl ⊢K∈B→+˙=m∈𝒫A,n∈𝒫A⟼m∪n∪p∈A|∃q∈m∃r∈np≤˙q∨˙r