Metamath Proof Explorer

Theorem sspadd2

Description: A projective subspace sum is a superset of its second summand. ( ssun2 analog.) (Contributed by NM, 3-Jan-2012)

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

Proof

Step Hyp Ref Expression
1 padd0.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
2 padd0.p
3 ssun2 ${⊢}{X}\subseteq {Y}\cup {X}$
4 ssun1 ${⊢}{Y}\cup {X}\subseteq \left({Y}\cup {X}\right)\cup \left\{{p}\in {A}|\exists {q}\in {Y}\phantom{\rule{.4em}{0ex}}\exists {r}\in {X}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right\}$
5 3 4 sstri ${⊢}{X}\subseteq \left({Y}\cup {X}\right)\cup \left\{{p}\in {A}|\exists {q}\in {Y}\phantom{\rule{.4em}{0ex}}\exists {r}\in {X}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right\}$
6 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
7 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
8 6 7 1 2 paddval
9 8 3com23
10 5 9 sseqtrrid