Metamath Proof Explorer


Theorem padd01

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

Ref Expression
Hypotheses padd0.a 𝐴 = ( Atoms ‘ 𝐾 )
padd0.p + = ( +𝑃𝐾 )
Assertion padd01 ( ( 𝐾𝐵𝑋𝐴 ) → ( 𝑋 + ∅ ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 padd0.a 𝐴 = ( Atoms ‘ 𝐾 )
2 padd0.p + = ( +𝑃𝐾 )
3 simpl ( ( 𝐾𝐵𝑋𝐴 ) → 𝐾𝐵 )
4 simpr ( ( 𝐾𝐵𝑋𝐴 ) → 𝑋𝐴 )
5 0ss ∅ ⊆ 𝐴
6 5 a1i ( ( 𝐾𝐵𝑋𝐴 ) → ∅ ⊆ 𝐴 )
7 3 4 6 3jca ( ( 𝐾𝐵𝑋𝐴 ) → ( 𝐾𝐵𝑋𝐴 ∧ ∅ ⊆ 𝐴 ) )
8 neirr ¬ ∅ ≠ ∅
9 8 intnan ¬ ( 𝑋 ≠ ∅ ∧ ∅ ≠ ∅ )
10 1 2 paddval0 ( ( ( 𝐾𝐵𝑋𝐴 ∧ ∅ ⊆ 𝐴 ) ∧ ¬ ( 𝑋 ≠ ∅ ∧ ∅ ≠ ∅ ) ) → ( 𝑋 + ∅ ) = ( 𝑋 ∪ ∅ ) )
11 7 9 10 sylancl ( ( 𝐾𝐵𝑋𝐴 ) → ( 𝑋 + ∅ ) = ( 𝑋 ∪ ∅ ) )
12 un0 ( 𝑋 ∪ ∅ ) = 𝑋
13 11 12 eqtrdi ( ( 𝐾𝐵𝑋𝐴 ) → ( 𝑋 + ∅ ) = 𝑋 )