Metamath Proof Explorer


Theorem paddssw2

Description: Subset law for projective subspace sum valid for all subsets of atoms. (Contributed by NM, 14-Mar-2012)

Ref Expression
Hypotheses paddssw.a A=AtomsK
paddssw.p +˙=+𝑃K
Assertion paddssw2 KBXAYAZAX+˙YZXZYZ

Proof

Step Hyp Ref Expression
1 paddssw.a A=AtomsK
2 paddssw.p +˙=+𝑃K
3 1 2 sspadd1 KBXAYAXX+˙Y
4 3 3adant3r3 KBXAYAZAXX+˙Y
5 sstr XX+˙YX+˙YZXZ
6 4 5 sylan KBXAYAZAX+˙YZXZ
7 6 ex KBXAYAZAX+˙YZXZ
8 simpl KBXAYAZAKB
9 simpr2 KBXAYAZAYA
10 simpr1 KBXAYAZAXA
11 1 2 sspadd2 KBYAXAYX+˙Y
12 8 9 10 11 syl3anc KBXAYAZAYX+˙Y
13 sstr YX+˙YX+˙YZYZ
14 12 13 sylan KBXAYAZAX+˙YZYZ
15 14 ex KBXAYAZAX+˙YZYZ
16 7 15 jcad KBXAYAZAX+˙YZXZYZ