Metamath Proof Explorer


Theorem paddssw1

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 = Atoms K
paddssw.p + ˙ = + 𝑃 K
Assertion paddssw1 K B X A Y A Z A X Z Y Z X + ˙ Y Z + ˙ Z

Proof

Step Hyp Ref Expression
1 paddssw.a A = Atoms K
2 paddssw.p + ˙ = + 𝑃 K
3 simpl K B X A Y A Z A K B
4 simpr3 K B X A Y A Z A Z A
5 1 2 paddss12 K B Z A Z A X Z Y Z X + ˙ Y Z + ˙ Z
6 3 4 4 5 syl3anc K B X A Y A Z A X Z Y Z X + ˙ Y Z + ˙ Z