Theorem paddssw2

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

Proof

Step	Hyp	Ref	Expression
1		paddssw.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		paddssw.p	⊢ + = ( +𝑃 ‘ 𝐾 )
3	1 2	sspadd1	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → 𝑋 ⊆ ( 𝑋 + 𝑌 ) )
4	3	3adant3r3	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝑋 ⊆ ( 𝑋 + 𝑌 ) )
5		sstr	⊢ ( ( 𝑋 ⊆ ( 𝑋 + 𝑌 ) ∧ ( 𝑋 + 𝑌 ) ⊆ 𝑍 ) → 𝑋 ⊆ 𝑍 )
6	4 5	sylan	⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) ∧ ( 𝑋 + 𝑌 ) ⊆ 𝑍 ) → 𝑋 ⊆ 𝑍 )
7	6	ex	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 + 𝑌 ) ⊆ 𝑍 → 𝑋 ⊆ 𝑍 ) )
8		simpl	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝐾 ∈ 𝐵 )
9		simpr2	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝑌 ⊆ 𝐴 )
10		simpr1	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝑋 ⊆ 𝐴 )
11	1 2	sspadd2	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → 𝑌 ⊆ ( 𝑋 + 𝑌 ) )
12	8 9 10 11	syl3anc	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝑌 ⊆ ( 𝑋 + 𝑌 ) )
13		sstr	⊢ ( ( 𝑌 ⊆ ( 𝑋 + 𝑌 ) ∧ ( 𝑋 + 𝑌 ) ⊆ 𝑍 ) → 𝑌 ⊆ 𝑍 )
14	12 13	sylan	⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) ∧ ( 𝑋 + 𝑌 ) ⊆ 𝑍 ) → 𝑌 ⊆ 𝑍 )
15	14	ex	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 + 𝑌 ) ⊆ 𝑍 → 𝑌 ⊆ 𝑍 ) )
16	7 15	jcad	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 + 𝑌 ) ⊆ 𝑍 → ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) ) )