# Metamath Proof Explorer

Description: A projective subspace sum is a set of atoms. (Contributed by NM, 3-Jan-2012)

Ref Expression
Hypotheses padd0.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$

### Proof

Step Hyp Ref Expression
1 padd0.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
3 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
4 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
6 unss ${⊢}\left({X}\subseteq {A}\wedge {Y}\subseteq {A}\right)↔{X}\cup {Y}\subseteq {A}$
7 6 biimpi ${⊢}\left({X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\to {X}\cup {Y}\subseteq {A}$
8 ssrab2 ${⊢}\left\{{p}\in {A}|\exists {q}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {Y}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right\}\subseteq {A}$
9 7 8 jctir ${⊢}\left({X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\to \left({X}\cup {Y}\subseteq {A}\wedge \left\{{p}\in {A}|\exists {q}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {Y}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right\}\subseteq {A}\right)$
10 unss ${⊢}\left({X}\cup {Y}\subseteq {A}\wedge \left\{{p}\in {A}|\exists {q}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {Y}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right\}\subseteq {A}\right)↔\left({X}\cup {Y}\right)\cup \left\{{p}\in {A}|\exists {q}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {Y}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right\}\subseteq {A}$
11 9 10 sylib ${⊢}\left({X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\to \left({X}\cup {Y}\right)\cup \left\{{p}\in {A}|\exists {q}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {Y}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right\}\subseteq {A}$
12 11 3adant1 ${⊢}\left({K}\in {B}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\to \left({X}\cup {Y}\right)\cup \left\{{p}\in {A}|\exists {q}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {Y}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right\}\subseteq {A}$