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

Theorem elpaddn0 37551
Description: Member of projective subspace sum of nonempty sets. (Contributed by NM, 3-Jan-2012.)
Hypotheses
Ref Expression
paddfval.l = (le‘𝐾)
paddfval.j = (join‘𝐾)
paddfval.a 𝐴 = (Atoms‘𝐾)
paddfval.p + = (+𝑃𝐾)
Assertion
Ref Expression
elpaddn0 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑆 ∈ (𝑋 + 𝑌) ↔ (𝑆𝐴 ∧ ∃𝑞𝑋𝑟𝑌 𝑆 (𝑞 𝑟))))
Distinct variable groups:   𝑟,𝑞,𝐾   𝑋,𝑞   𝑌,𝑞,𝑟   𝑆,𝑞,𝑟   𝐴,𝑞,𝑟   ,𝑞,𝑟   ,𝑞,𝑟   𝑋,𝑟
Allowed substitution hints:   + (𝑟,𝑞)

Proof of Theorem elpaddn0
StepHypRef Expression
1 paddfval.l . . . 4 = (le‘𝐾)
2 paddfval.j . . . 4 = (join‘𝐾)
3 paddfval.a . . . 4 𝐴 = (Atoms‘𝐾)
4 paddfval.p . . . 4 + = (+𝑃𝐾)
51, 2, 3, 4elpadd 37550 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) → (𝑆 ∈ (𝑋 + 𝑌) ↔ ((𝑆𝑋𝑆𝑌) ∨ (𝑆𝐴 ∧ ∃𝑞𝑋𝑟𝑌 𝑆 (𝑞 𝑟)))))
65adantr 484 . 2 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑆 ∈ (𝑋 + 𝑌) ↔ ((𝑆𝑋𝑆𝑌) ∨ (𝑆𝐴 ∧ ∃𝑞𝑋𝑟𝑌 𝑆 (𝑞 𝑟)))))
7 simpl2 1194 . . . . . 6 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → 𝑋𝐴)
87sseld 3900 . . . . 5 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑆𝑋𝑆𝐴))
9 simpll1 1214 . . . . . . . . . . . . 13 ((((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑆𝑋) ∧ 𝑟𝑌) → 𝐾 ∈ Lat)
10 ssel2 3895 . . . . . . . . . . . . . . . 16 ((𝑋𝐴𝑆𝑋) → 𝑆𝐴)
11103ad2antl2 1188 . . . . . . . . . . . . . . 15 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑆𝑋) → 𝑆𝐴)
1211adantr 484 . . . . . . . . . . . . . 14 ((((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑆𝑋) ∧ 𝑟𝑌) → 𝑆𝐴)
13 eqid 2737 . . . . . . . . . . . . . . 15 (Base‘𝐾) = (Base‘𝐾)
1413, 3atbase 37040 . . . . . . . . . . . . . 14 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
1512, 14syl 17 . . . . . . . . . . . . 13 ((((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑆𝑋) ∧ 𝑟𝑌) → 𝑆 ∈ (Base‘𝐾))
16 simpl3 1195 . . . . . . . . . . . . . . 15 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑆𝑋) → 𝑌𝐴)
1716sselda 3901 . . . . . . . . . . . . . 14 ((((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑆𝑋) ∧ 𝑟𝑌) → 𝑟𝐴)
1813, 3atbase 37040 . . . . . . . . . . . . . 14 (𝑟𝐴𝑟 ∈ (Base‘𝐾))
1917, 18syl 17 . . . . . . . . . . . . 13 ((((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑆𝑋) ∧ 𝑟𝑌) → 𝑟 ∈ (Base‘𝐾))
2013, 1, 2latlej1 17954 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ 𝑟 ∈ (Base‘𝐾)) → 𝑆 (𝑆 𝑟))
219, 15, 19, 20syl3anc 1373 . . . . . . . . . . . 12 ((((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑆𝑋) ∧ 𝑟𝑌) → 𝑆 (𝑆 𝑟))
2221reximdva0 4266 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑆𝑋) ∧ 𝑌 ≠ ∅) → ∃𝑟𝑌 𝑆 (𝑆 𝑟))
2322exp31 423 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) → (𝑆𝑋 → (𝑌 ≠ ∅ → ∃𝑟𝑌 𝑆 (𝑆 𝑟))))
2423com23 86 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) → (𝑌 ≠ ∅ → (𝑆𝑋 → ∃𝑟𝑌 𝑆 (𝑆 𝑟))))
2524imp 410 . . . . . . . 8 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑌 ≠ ∅) → (𝑆𝑋 → ∃𝑟𝑌 𝑆 (𝑆 𝑟)))
2625ancld 554 . . . . . . 7 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑌 ≠ ∅) → (𝑆𝑋 → (𝑆𝑋 ∧ ∃𝑟𝑌 𝑆 (𝑆 𝑟))))
27 oveq1 7220 . . . . . . . . . 10 (𝑞 = 𝑆 → (𝑞 𝑟) = (𝑆 𝑟))
2827breq2d 5065 . . . . . . . . 9 (𝑞 = 𝑆 → (𝑆 (𝑞 𝑟) ↔ 𝑆 (𝑆 𝑟)))
2928rexbidv 3216 . . . . . . . 8 (𝑞 = 𝑆 → (∃𝑟𝑌 𝑆 (𝑞 𝑟) ↔ ∃𝑟𝑌 𝑆 (𝑆 𝑟)))
3029rspcev 3537 . . . . . . 7 ((𝑆𝑋 ∧ ∃𝑟𝑌 𝑆 (𝑆 𝑟)) → ∃𝑞𝑋𝑟𝑌 𝑆 (𝑞 𝑟))
3126, 30syl6 35 . . . . . 6 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑌 ≠ ∅) → (𝑆𝑋 → ∃𝑞𝑋𝑟𝑌 𝑆 (𝑞 𝑟)))
3231adantrl 716 . . . . 5 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑆𝑋 → ∃𝑞𝑋𝑟𝑌 𝑆 (𝑞 𝑟)))
338, 32jcad 516 . . . 4 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑆𝑋 → (𝑆𝐴 ∧ ∃𝑞𝑋𝑟𝑌 𝑆 (𝑞 𝑟))))
34 simpl3 1195 . . . . . 6 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → 𝑌𝐴)
3534sseld 3900 . . . . 5 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑆𝑌𝑆𝐴))
36 simpll1 1214 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑞𝑋) ∧ 𝑆𝑌) → 𝐾 ∈ Lat)
37 ssel2 3895 . . . . . . . . . . . . . . . . . 18 ((𝑋𝐴𝑞𝑋) → 𝑞𝐴)
38373ad2antl2 1188 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑞𝑋) → 𝑞𝐴)
3938adantr 484 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑞𝑋) ∧ 𝑆𝑌) → 𝑞𝐴)
4013, 3atbase 37040 . . . . . . . . . . . . . . . 16 (𝑞𝐴𝑞 ∈ (Base‘𝐾))
4139, 40syl 17 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑞𝑋) ∧ 𝑆𝑌) → 𝑞 ∈ (Base‘𝐾))
42 simpl3 1195 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑞𝑋) → 𝑌𝐴)
4342sselda 3901 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑞𝑋) ∧ 𝑆𝑌) → 𝑆𝐴)
4443, 14syl 17 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑞𝑋) ∧ 𝑆𝑌) → 𝑆 ∈ (Base‘𝐾))
4513, 1, 2latlej2 17955 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ 𝑞 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → 𝑆 (𝑞 𝑆))
4636, 41, 44, 45syl3anc 1373 . . . . . . . . . . . . . 14 ((((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑞𝑋) ∧ 𝑆𝑌) → 𝑆 (𝑞 𝑆))
4746ex 416 . . . . . . . . . . . . 13 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑞𝑋) → (𝑆𝑌𝑆 (𝑞 𝑆)))
4847ancld 554 . . . . . . . . . . . 12 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑞𝑋) → (𝑆𝑌 → (𝑆𝑌𝑆 (𝑞 𝑆))))
49 oveq2 7221 . . . . . . . . . . . . . 14 (𝑟 = 𝑆 → (𝑞 𝑟) = (𝑞 𝑆))
5049breq2d 5065 . . . . . . . . . . . . 13 (𝑟 = 𝑆 → (𝑆 (𝑞 𝑟) ↔ 𝑆 (𝑞 𝑆)))
5150rspcev 3537 . . . . . . . . . . . 12 ((𝑆𝑌𝑆 (𝑞 𝑆)) → ∃𝑟𝑌 𝑆 (𝑞 𝑟))
5248, 51syl6 35 . . . . . . . . . . 11 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑞𝑋) → (𝑆𝑌 → ∃𝑟𝑌 𝑆 (𝑞 𝑟)))
5352impancom 455 . . . . . . . . . 10 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑆𝑌) → (𝑞𝑋 → ∃𝑟𝑌 𝑆 (𝑞 𝑟)))
5453ancld 554 . . . . . . . . 9 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑆𝑌) → (𝑞𝑋 → (𝑞𝑋 ∧ ∃𝑟𝑌 𝑆 (𝑞 𝑟))))
5554eximdv 1925 . . . . . . . 8 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑆𝑌) → (∃𝑞 𝑞𝑋 → ∃𝑞(𝑞𝑋 ∧ ∃𝑟𝑌 𝑆 (𝑞 𝑟))))
56 n0 4261 . . . . . . . 8 (𝑋 ≠ ∅ ↔ ∃𝑞 𝑞𝑋)
57 df-rex 3067 . . . . . . . 8 (∃𝑞𝑋𝑟𝑌 𝑆 (𝑞 𝑟) ↔ ∃𝑞(𝑞𝑋 ∧ ∃𝑟𝑌 𝑆 (𝑞 𝑟)))
5855, 56, 573imtr4g 299 . . . . . . 7 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑆𝑌) → (𝑋 ≠ ∅ → ∃𝑞𝑋𝑟𝑌 𝑆 (𝑞 𝑟)))
5958impancom 455 . . . . . 6 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑋 ≠ ∅) → (𝑆𝑌 → ∃𝑞𝑋𝑟𝑌 𝑆 (𝑞 𝑟)))
6059adantrr 717 . . . . 5 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑆𝑌 → ∃𝑞𝑋𝑟𝑌 𝑆 (𝑞 𝑟)))
6135, 60jcad 516 . . . 4 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑆𝑌 → (𝑆𝐴 ∧ ∃𝑞𝑋𝑟𝑌 𝑆 (𝑞 𝑟))))
6233, 61jaod 859 . . 3 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → ((𝑆𝑋𝑆𝑌) → (𝑆𝐴 ∧ ∃𝑞𝑋𝑟𝑌 𝑆 (𝑞 𝑟))))
63 pm4.72 950 . . 3 (((𝑆𝑋𝑆𝑌) → (𝑆𝐴 ∧ ∃𝑞𝑋𝑟𝑌 𝑆 (𝑞 𝑟))) ↔ ((𝑆𝐴 ∧ ∃𝑞𝑋𝑟𝑌 𝑆 (𝑞 𝑟)) ↔ ((𝑆𝑋𝑆𝑌) ∨ (𝑆𝐴 ∧ ∃𝑞𝑋𝑟𝑌 𝑆 (𝑞 𝑟)))))
6462, 63sylib 221 . 2 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → ((𝑆𝐴 ∧ ∃𝑞𝑋𝑟𝑌 𝑆 (𝑞 𝑟)) ↔ ((𝑆𝑋𝑆𝑌) ∨ (𝑆𝐴 ∧ ∃𝑞𝑋𝑟𝑌 𝑆 (𝑞 𝑟)))))
656, 64bitr4d 285 1 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑆 ∈ (𝑋 + 𝑌) ↔ (𝑆𝐴 ∧ ∃𝑞𝑋𝑟𝑌 𝑆 (𝑞 𝑟))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 847  w3a 1089   = wceq 1543  wex 1787  wcel 2110  wne 2940  wrex 3062  wss 3866  c0 4237   class class class wbr 5053  cfv 6380  (class class class)co 7213  Basecbs 16760  lecple 16809  joincjn 17818  Latclat 17937  Atomscatm 37014  +𝑃cpadd 37546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-1st 7761  df-2nd 7762  df-lub 17852  df-join 17854  df-lat 17938  df-ats 37018  df-padd 37547
This theorem is referenced by:  paddvaln0N  37552  elpaddri  37553  elpaddat  37555  paddasslem15  37585  paddasslem16  37586  pmodlem2  37598  pmapjat1  37604
  Copyright terms: Public domain W3C validator