Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  paddssat Structured version   Visualization version   GIF version

 Description: A projective subspace sum is a set of atoms. (Contributed by NM, 3-Jan-2012.)
Hypotheses
Ref Expression
Assertion
Ref Expression
paddssat ((𝐾𝐵𝑋𝐴𝑌𝐴) → (𝑋 + 𝑌) ⊆ 𝐴)

Dummy variables 𝑞 𝑝 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2825 . . 3 (le‘𝐾) = (le‘𝐾)
2 eqid 2825 . . 3 (join‘𝐾) = (join‘𝐾)
3 padd0.a . . 3 𝐴 = (Atoms‘𝐾)
4 padd0.p . . 3 + = (+𝑃𝐾)
51, 2, 3, 4paddval 35872 . 2 ((𝐾𝐵𝑋𝐴𝑌𝐴) → (𝑋 + 𝑌) = ((𝑋𝑌) ∪ {𝑝𝐴 ∣ ∃𝑞𝑋𝑟𝑌 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)}))
6 unss 4016 . . . . . 6 ((𝑋𝐴𝑌𝐴) ↔ (𝑋𝑌) ⊆ 𝐴)
76biimpi 208 . . . . 5 ((𝑋𝐴𝑌𝐴) → (𝑋𝑌) ⊆ 𝐴)
8 ssrab2 3914 . . . . 5 {𝑝𝐴 ∣ ∃𝑞𝑋𝑟𝑌 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)} ⊆ 𝐴
97, 8jctir 516 . . . 4 ((𝑋𝐴𝑌𝐴) → ((𝑋𝑌) ⊆ 𝐴 ∧ {𝑝𝐴 ∣ ∃𝑞𝑋𝑟𝑌 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)} ⊆ 𝐴))
10 unss 4016 . . . 4 (((𝑋𝑌) ⊆ 𝐴 ∧ {𝑝𝐴 ∣ ∃𝑞𝑋𝑟𝑌 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)} ⊆ 𝐴) ↔ ((𝑋𝑌) ∪ {𝑝𝐴 ∣ ∃𝑞𝑋𝑟𝑌 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)}) ⊆ 𝐴)
119, 10sylib 210 . . 3 ((𝑋𝐴𝑌𝐴) → ((𝑋𝑌) ∪ {𝑝𝐴 ∣ ∃𝑞𝑋𝑟𝑌 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)}) ⊆ 𝐴)
12113adant1 1164 . 2 ((𝐾𝐵𝑋𝐴𝑌𝐴) → ((𝑋𝑌) ∪ {𝑝𝐴 ∣ ∃𝑞𝑋𝑟𝑌 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)}) ⊆ 𝐴)
135, 12eqsstrd 3864 1 ((𝐾𝐵𝑋𝐴𝑌𝐴) → (𝑋 + 𝑌) ⊆ 𝐴)