Theorem paddss

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

	Ref	Expression
Hypotheses	paddss.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	paddss.s	⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
	paddss.p	⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion	paddss	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → ( ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) ↔ ( 𝑋 + 𝑌 ) ⊆ 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		paddss.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		paddss.s	⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
3		paddss.p	⊢ + = ( +𝑃 ‘ 𝐾 )
4		simpl	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → 𝐾 ∈ 𝐵 )
5		simpr1	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → 𝑋 ⊆ 𝐴 )
6		simpr2	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → 𝑌 ⊆ 𝐴 )
7	1 2	psubssat	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑍 ∈ 𝑆 ) → 𝑍 ⊆ 𝐴 )
8	7	3ad2antr3	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → 𝑍 ⊆ 𝐴 )
9	1 3	paddssw1	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) → ( 𝑋 + 𝑌 ) ⊆ ( 𝑍 + 𝑍 ) ) )
10	4 5 6 8 9	syl13anc	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → ( ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) → ( 𝑋 + 𝑌 ) ⊆ ( 𝑍 + 𝑍 ) ) )
11	2 3	paddidm	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑍 ∈ 𝑆 ) → ( 𝑍 + 𝑍 ) = 𝑍 )
12	11	3ad2antr3	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → ( 𝑍 + 𝑍 ) = 𝑍 )
13	12	sseq2d	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → ( ( 𝑋 + 𝑌 ) ⊆ ( 𝑍 + 𝑍 ) ↔ ( 𝑋 + 𝑌 ) ⊆ 𝑍 ) )
14	10 13	sylibd	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → ( ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) → ( 𝑋 + 𝑌 ) ⊆ 𝑍 ) )
15	1 3	paddssw2	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 + 𝑌 ) ⊆ 𝑍 → ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) ) )
16	4 5 6 8 15	syl13anc	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → ( ( 𝑋 + 𝑌 ) ⊆ 𝑍 → ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) ) )
17	14 16	impbid	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → ( ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) ↔ ( 𝑋 + 𝑌 ) ⊆ 𝑍 ) )