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

Theorem paddclN 38582
Description: The projective sum of two subspaces is a subspace. Part of Lemma 16.2 of [MaedaMaeda] p. 68. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
paddidm.s 𝑆 = (PSubSp‘𝐾)
paddidm.p + = (+𝑃𝐾)
Assertion
Ref Expression
paddclN ((𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆) → (𝑋 + 𝑌) ∈ 𝑆)

Proof of Theorem paddclN
Dummy variables 𝑝 𝑞 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1 1136 . . 3 ((𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆) → 𝐾 ∈ HL)
2 eqid 2732 . . . . 5 (Atoms‘𝐾) = (Atoms‘𝐾)
3 paddidm.s . . . . 5 𝑆 = (PSubSp‘𝐾)
42, 3psubssat 38494 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝑆) → 𝑋 ⊆ (Atoms‘𝐾))
543adant3 1132 . . 3 ((𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆) → 𝑋 ⊆ (Atoms‘𝐾))
62, 3psubssat 38494 . . . 4 ((𝐾 ∈ HL ∧ 𝑌𝑆) → 𝑌 ⊆ (Atoms‘𝐾))
763adant2 1131 . . 3 ((𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆) → 𝑌 ⊆ (Atoms‘𝐾))
8 paddidm.p . . . 4 + = (+𝑃𝐾)
92, 8paddssat 38554 . . 3 ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾) ∧ 𝑌 ⊆ (Atoms‘𝐾)) → (𝑋 + 𝑌) ⊆ (Atoms‘𝐾))
101, 5, 7, 9syl3anc 1371 . 2 ((𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆) → (𝑋 + 𝑌) ⊆ (Atoms‘𝐾))
11 olc 866 . . . . 5 ((𝑝 ∈ (Atoms‘𝐾) ∧ ∃𝑞 ∈ (𝑋 + 𝑌)∃𝑟 ∈ (𝑋 + 𝑌)𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)) → ((𝑝 ∈ (𝑋 + 𝑌) ∨ 𝑝 ∈ (𝑋 + 𝑌)) ∨ (𝑝 ∈ (Atoms‘𝐾) ∧ ∃𝑞 ∈ (𝑋 + 𝑌)∃𝑟 ∈ (𝑋 + 𝑌)𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟))))
12 eqid 2732 . . . . . . . 8 (le‘𝐾) = (le‘𝐾)
13 eqid 2732 . . . . . . . 8 (join‘𝐾) = (join‘𝐾)
1412, 13, 2, 8elpadd 38539 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋 + 𝑌) ⊆ (Atoms‘𝐾) ∧ (𝑋 + 𝑌) ⊆ (Atoms‘𝐾)) → (𝑝 ∈ ((𝑋 + 𝑌) + (𝑋 + 𝑌)) ↔ ((𝑝 ∈ (𝑋 + 𝑌) ∨ 𝑝 ∈ (𝑋 + 𝑌)) ∨ (𝑝 ∈ (Atoms‘𝐾) ∧ ∃𝑞 ∈ (𝑋 + 𝑌)∃𝑟 ∈ (𝑋 + 𝑌)𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)))))
151, 10, 10, 14syl3anc 1371 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆) → (𝑝 ∈ ((𝑋 + 𝑌) + (𝑋 + 𝑌)) ↔ ((𝑝 ∈ (𝑋 + 𝑌) ∨ 𝑝 ∈ (𝑋 + 𝑌)) ∨ (𝑝 ∈ (Atoms‘𝐾) ∧ ∃𝑞 ∈ (𝑋 + 𝑌)∃𝑟 ∈ (𝑋 + 𝑌)𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)))))
162, 8padd4N 38580 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑋 ⊆ (Atoms‘𝐾) ∧ 𝑌 ⊆ (Atoms‘𝐾)) ∧ (𝑋 ⊆ (Atoms‘𝐾) ∧ 𝑌 ⊆ (Atoms‘𝐾))) → ((𝑋 + 𝑌) + (𝑋 + 𝑌)) = ((𝑋 + 𝑋) + (𝑌 + 𝑌)))
171, 5, 7, 5, 7, 16syl122anc 1379 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆) → ((𝑋 + 𝑌) + (𝑋 + 𝑌)) = ((𝑋 + 𝑋) + (𝑌 + 𝑌)))
183, 8paddidm 38581 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑋𝑆) → (𝑋 + 𝑋) = 𝑋)
19183adant3 1132 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆) → (𝑋 + 𝑋) = 𝑋)
203, 8paddidm 38581 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑌𝑆) → (𝑌 + 𝑌) = 𝑌)
21203adant2 1131 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆) → (𝑌 + 𝑌) = 𝑌)
2219, 21oveq12d 7412 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆) → ((𝑋 + 𝑋) + (𝑌 + 𝑌)) = (𝑋 + 𝑌))
2317, 22eqtrd 2772 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆) → ((𝑋 + 𝑌) + (𝑋 + 𝑌)) = (𝑋 + 𝑌))
2423eleq2d 2819 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆) → (𝑝 ∈ ((𝑋 + 𝑌) + (𝑋 + 𝑌)) ↔ 𝑝 ∈ (𝑋 + 𝑌)))
2515, 24bitr3d 280 . . . . 5 ((𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆) → (((𝑝 ∈ (𝑋 + 𝑌) ∨ 𝑝 ∈ (𝑋 + 𝑌)) ∨ (𝑝 ∈ (Atoms‘𝐾) ∧ ∃𝑞 ∈ (𝑋 + 𝑌)∃𝑟 ∈ (𝑋 + 𝑌)𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟))) ↔ 𝑝 ∈ (𝑋 + 𝑌)))
2611, 25imbitrid 243 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆) → ((𝑝 ∈ (Atoms‘𝐾) ∧ ∃𝑞 ∈ (𝑋 + 𝑌)∃𝑟 ∈ (𝑋 + 𝑌)𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)) → 𝑝 ∈ (𝑋 + 𝑌)))
2726expd 416 . . 3 ((𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆) → (𝑝 ∈ (Atoms‘𝐾) → (∃𝑞 ∈ (𝑋 + 𝑌)∃𝑟 ∈ (𝑋 + 𝑌)𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟) → 𝑝 ∈ (𝑋 + 𝑌))))
2827ralrimiv 3145 . 2 ((𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆) → ∀𝑝 ∈ (Atoms‘𝐾)(∃𝑞 ∈ (𝑋 + 𝑌)∃𝑟 ∈ (𝑋 + 𝑌)𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟) → 𝑝 ∈ (𝑋 + 𝑌)))
2912, 13, 2, 3ispsubsp2 38486 . . 3 (𝐾 ∈ HL → ((𝑋 + 𝑌) ∈ 𝑆 ↔ ((𝑋 + 𝑌) ⊆ (Atoms‘𝐾) ∧ ∀𝑝 ∈ (Atoms‘𝐾)(∃𝑞 ∈ (𝑋 + 𝑌)∃𝑟 ∈ (𝑋 + 𝑌)𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟) → 𝑝 ∈ (𝑋 + 𝑌)))))
30293ad2ant1 1133 . 2 ((𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆) → ((𝑋 + 𝑌) ∈ 𝑆 ↔ ((𝑋 + 𝑌) ⊆ (Atoms‘𝐾) ∧ ∀𝑝 ∈ (Atoms‘𝐾)(∃𝑞 ∈ (𝑋 + 𝑌)∃𝑟 ∈ (𝑋 + 𝑌)𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟) → 𝑝 ∈ (𝑋 + 𝑌)))))
3110, 28, 30mpbir2and 711 1 ((𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆) → (𝑋 + 𝑌) ∈ 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wral 3061  wrex 3070  wss 3945   class class class wbr 5142  cfv 6533  (class class class)co 7394  lecple 17188  joincjn 18248  Atomscatm 38002  HLchlt 38089  PSubSpcpsubsp 38236  +𝑃cpadd 38535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5357  ax-pr 5421  ax-un 7709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5568  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-rn 5681  df-res 5682  df-ima 5683  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7350  df-ov 7397  df-oprab 7398  df-mpo 7399  df-1st 7959  df-2nd 7960  df-proset 18232  df-poset 18250  df-plt 18267  df-lub 18283  df-glb 18284  df-join 18285  df-meet 18286  df-p0 18362  df-lat 18369  df-clat 18436  df-oposet 37915  df-ol 37917  df-oml 37918  df-covers 38005  df-ats 38006  df-atl 38037  df-cvlat 38061  df-hlat 38090  df-psubsp 38243  df-padd 38536
This theorem is referenced by:  pmodl42N  38591  pclun2N  38639
  Copyright terms: Public domain W3C validator