Description: Projective subspace sum includes the set union of its arguments. (Contributed by NM, 12-Jan-2012) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | padd0.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | |
padd0.p | ⊢ + = ( +𝑃 ‘ 𝐾 ) | ||
Assertion | paddunssN | ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 ∪ 𝑌 ) ⊆ ( 𝑋 + 𝑌 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | padd0.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | |
2 | padd0.p | ⊢ + = ( +𝑃 ‘ 𝐾 ) | |
3 | ssun1 | ⊢ ( 𝑋 ∪ 𝑌 ) ⊆ ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) } ) | |
4 | eqid | ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) | |
5 | eqid | ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 ) | |
6 | 4 5 1 2 | paddval | ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) = ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) } ) ) |
7 | 3 6 | sseqtrrid | ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 ∪ 𝑌 ) ⊆ ( 𝑋 + 𝑌 ) ) |