Theorem paddss12

Description: Subset law for projective subspace sum. ( unss12 analog.) (Contributed by NM, 7-Mar-2012)

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

Proof

Step	Hyp	Ref	Expression
1		padd0.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		padd0.p	⊢ + = ( +𝑃 ‘ 𝐾 )
3		simpl1	⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) ) → 𝐾 ∈ 𝐵 )
4		simpl2	⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) ) → 𝑌 ⊆ 𝐴 )
5		sstr	⊢ ( ( 𝑍 ⊆ 𝑊 ∧ 𝑊 ⊆ 𝐴 ) → 𝑍 ⊆ 𝐴 )
6	5	ancoms	⊢ ( ( 𝑊 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝑊 ) → 𝑍 ⊆ 𝐴 )
7	6	ad2ant2l	⊢ ( ( ( 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) ) → 𝑍 ⊆ 𝐴 )
8	7	3adantl1	⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) ) → 𝑍 ⊆ 𝐴 )
9	3 4 8	3jca	⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) ) → ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) )
10		simprl	⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) ) → 𝑋 ⊆ 𝑌 )
11	1 2	paddss1	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( 𝑋 ⊆ 𝑌 → ( 𝑋 + 𝑍 ) ⊆ ( 𝑌 + 𝑍 ) ) )
12	9 10 11	sylc	⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) ) → ( 𝑋 + 𝑍 ) ⊆ ( 𝑌 + 𝑍 ) )
13	1 2	paddss2	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑊 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑍 ⊆ 𝑊 → ( 𝑌 + 𝑍 ) ⊆ ( 𝑌 + 𝑊 ) ) )
14	13	3com23	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) → ( 𝑍 ⊆ 𝑊 → ( 𝑌 + 𝑍 ) ⊆ ( 𝑌 + 𝑊 ) ) )
15	14	imp	⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ 𝑍 ⊆ 𝑊 ) → ( 𝑌 + 𝑍 ) ⊆ ( 𝑌 + 𝑊 ) )
16	15	adantrl	⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) ) → ( 𝑌 + 𝑍 ) ⊆ ( 𝑌 + 𝑊 ) )
17	12 16	sstrd	⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) ) → ( 𝑋 + 𝑍 ) ⊆ ( 𝑌 + 𝑊 ) )
18	17	ex	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) → ( ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) → ( 𝑋 + 𝑍 ) ⊆ ( 𝑌 + 𝑊 ) ) )