Metamath Proof Explorer


Theorem paddunssN

Description: Projective subspace sum includes the set union of its arguments. (Contributed by NM, 12-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses padd0.a A = Atoms K
padd0.p + ˙ = + 𝑃 K
Assertion paddunssN K B X A Y A X Y X + ˙ Y

Proof

Step Hyp Ref Expression
1 padd0.a A = Atoms K
2 padd0.p + ˙ = + 𝑃 K
3 ssun1 X Y X Y p A | q X r Y p K q join K r
4 eqid K = K
5 eqid join K = join K
6 4 5 1 2 paddval K B X A Y A X + ˙ Y = X Y p A | q X r Y p K q join K r
7 3 6 sseqtrrid K B X A Y A X Y X + ˙ Y