Theorem sspadd2

Description: A projective subspace sum is a superset of its second summand. ( ssun2 analog.) (Contributed by NM, 3-Jan-2012)

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

Proof

Step	Hyp	Ref	Expression
1		padd0.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		padd0.p	⊢ + = ( +𝑃 ‘ 𝐾 )
3		ssun2	⊢ 𝑋 ⊆ ( 𝑌 ∪ 𝑋 )
4		ssun1	⊢ ( 𝑌 ∪ 𝑋 ) ⊆ ( ( 𝑌 ∪ 𝑋 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑌 ∃ 𝑟 ∈ 𝑋 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) } )
5	3 4	sstri	⊢ 𝑋 ⊆ ( ( 𝑌 ∪ 𝑋 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑌 ∃ 𝑟 ∈ 𝑋 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) } )
6		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
7		eqid	⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
8	6 7 1 2	paddval	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑌 + 𝑋 ) = ( ( 𝑌 ∪ 𝑋 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑌 ∃ 𝑟 ∈ 𝑋 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) } ) )
9	8	3com23	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑌 + 𝑋 ) = ( ( 𝑌 ∪ 𝑋 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑌 ∃ 𝑟 ∈ 𝑋 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) } ) )
10	5 9	sseqtrrid	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → 𝑋 ⊆ ( 𝑌 + 𝑋 ) )