Theorem paddssw1

Description: Subset law for projective subspace sum valid for all subsets of atoms. (Contributed by NM, 14-Mar-2012)

	Ref	Expression
Hypotheses	paddssw.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	paddssw.p	⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion	paddssw1	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) → ( 𝑋 + 𝑌 ) ⊆ ( 𝑍 + 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		paddssw.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		paddssw.p	⊢ + = ( +𝑃 ‘ 𝐾 )
3		simpl	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝐾 ∈ 𝐵 )
4		simpr3	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝑍 ⊆ 𝐴 )
5	1 2	paddss12	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑍 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) → ( 𝑋 + 𝑌 ) ⊆ ( 𝑍 + 𝑍 ) ) )
6	3 4 4 5	syl3anc	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) → ( 𝑋 + 𝑌 ) ⊆ ( 𝑍 + 𝑍 ) ) )