Theorem paddval0

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

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

Proof

Step	Hyp	Ref	Expression
1		padd0.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		padd0.p	⊢ + = ( +𝑃 ‘ 𝐾 )
3	1 2	elpadd0	⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ¬ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( 𝑞 ∈ ( 𝑋 + 𝑌 ) ↔ ( 𝑞 ∈ 𝑋 ∨ 𝑞 ∈ 𝑌 ) ) )
4		elun	⊢ ( 𝑞 ∈ ( 𝑋 ∪ 𝑌 ) ↔ ( 𝑞 ∈ 𝑋 ∨ 𝑞 ∈ 𝑌 ) )
5	3 4	bitr4di	⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ¬ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( 𝑞 ∈ ( 𝑋 + 𝑌 ) ↔ 𝑞 ∈ ( 𝑋 ∪ 𝑌 ) ) )
6	5	eqrdv	⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ¬ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( 𝑋 + 𝑌 ) = ( 𝑋 ∪ 𝑌 ) )