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	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑋 + ∅ ) = 𝑋 )