# Metamath Proof Explorer

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 ( ( 𝐾𝐵𝑋𝐴𝑌𝐴 ) → ( 𝑋 + 𝑌 ) ⊆ 𝐴 )