This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem paddssat

Description: A projective subspace sum is a set of atoms. (Contributed by NM, 3-Jan-2012)

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

Proof

Step	Hyp	Ref	Expression
1		padd0.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		padd0.p	⊢ + = ( +_𝑃 ‘ 𝐾 )
3		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
4		eqid	⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
5	3 4 1 2	paddval	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) = ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) } ) )
6		unss	⊢ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ↔ ( 𝑋 ∪ 𝑌 ) ⊆ 𝐴 )
7	6	biimpi	⊢ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 ∪ 𝑌 ) ⊆ 𝐴 )
8		ssrab2	⊢ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) } ⊆ 𝐴
9	7 8	jctir	⊢ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( ( 𝑋 ∪ 𝑌 ) ⊆ 𝐴 ∧ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) } ⊆ 𝐴 ) )
10		unss	⊢ ( ( ( 𝑋 ∪ 𝑌 ) ⊆ 𝐴 ∧ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) } ⊆ 𝐴 ) ↔ ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) } ) ⊆ 𝐴 )
11	9 10	sylib	⊢ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) } ) ⊆ 𝐴 )
12	11	3adant1	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) } ) ⊆ 𝐴 )
13	5 12	eqsstrd	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) ⊆ 𝐴 )