Theorem padd02

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

	Ref	Expression
Hypotheses	padd0.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	padd0.p	⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion	padd02	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( ∅ + 𝑋 ) = 𝑋 )

Proof

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