Metamath Proof Explorer


Theorem padd02

Description: Projective subspace sum with an empty set. (Contributed by NM, 11-Jan-2012)

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

Proof

Step Hyp Ref Expression
1 padd0.a A = Atoms K
2 padd0.p + ˙ = + 𝑃 K
3 simpl K B X A K B
4 0ss A
5 4 a1i K B X A A
6 simpr K B X A X A
7 3 5 6 3jca K B X A K B A X A
8 neirr ¬
9 8 intnanr ¬ X
10 1 2 paddval0 K B A X A ¬ X + ˙ X = X
11 7 9 10 sylancl K B X A + ˙ X = X
12 uncom X = X
13 un0 X = X
14 12 13 eqtri X = X
15 11 14 eqtrdi K B X A + ˙ X = X