ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  shftfval GIF version

Theorem shftfval 10814
Description: The value of the sequence shifter operation is a function on . 𝐴 is ordinarily an integer. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
Hypothesis
Ref Expression
shftfval.1 𝐹 ∈ V
Assertion
Ref Expression
shftfval (𝐴 ∈ ℂ → (𝐹 shift 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥𝐴)𝐹𝑦)})
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐹,𝑦

Proof of Theorem shftfval
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplr 528 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥𝐴)𝐹𝑦) → 𝑥 ∈ ℂ)
2 simpll 527 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥𝐴)𝐹𝑦) → 𝐴 ∈ ℂ)
31, 2subcld 8258 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥𝐴)𝐹𝑦) → (𝑥𝐴) ∈ ℂ)
4 vex 2740 . . . . . . . . . . 11 𝑦 ∈ V
5 breldmg 4829 . . . . . . . . . . 11 (((𝑥𝐴) ∈ ℂ ∧ 𝑦 ∈ V ∧ (𝑥𝐴)𝐹𝑦) → (𝑥𝐴) ∈ dom 𝐹)
64, 5mp3an2 1325 . . . . . . . . . 10 (((𝑥𝐴) ∈ ℂ ∧ (𝑥𝐴)𝐹𝑦) → (𝑥𝐴) ∈ dom 𝐹)
73, 6sylancom 420 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥𝐴)𝐹𝑦) → (𝑥𝐴) ∈ dom 𝐹)
8 npcan 8156 . . . . . . . . . . . 12 ((𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑥𝐴) + 𝐴) = 𝑥)
98eqcomd 2183 . . . . . . . . . . 11 ((𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ) → 𝑥 = ((𝑥𝐴) + 𝐴))
109ancoms 268 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → 𝑥 = ((𝑥𝐴) + 𝐴))
1110adantr 276 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥𝐴)𝐹𝑦) → 𝑥 = ((𝑥𝐴) + 𝐴))
12 oveq1 5876 . . . . . . . . . . 11 (𝑤 = (𝑥𝐴) → (𝑤 + 𝐴) = ((𝑥𝐴) + 𝐴))
1312eqeq2d 2189 . . . . . . . . . 10 (𝑤 = (𝑥𝐴) → (𝑥 = (𝑤 + 𝐴) ↔ 𝑥 = ((𝑥𝐴) + 𝐴)))
1413rspcev 2841 . . . . . . . . 9 (((𝑥𝐴) ∈ dom 𝐹𝑥 = ((𝑥𝐴) + 𝐴)) → ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴))
157, 11, 14syl2anc 411 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥𝐴)𝐹𝑦) → ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴))
16 vex 2740 . . . . . . . . 9 𝑥 ∈ V
17 eqeq1 2184 . . . . . . . . . 10 (𝑧 = 𝑥 → (𝑧 = (𝑤 + 𝐴) ↔ 𝑥 = (𝑤 + 𝐴)))
1817rexbidv 2478 . . . . . . . . 9 (𝑧 = 𝑥 → (∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴) ↔ ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴)))
1916, 18elab 2881 . . . . . . . 8 (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ↔ ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴))
2015, 19sylibr 134 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥𝐴)𝐹𝑦) → 𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)})
21 brelrng 4854 . . . . . . . . 9 (((𝑥𝐴) ∈ ℂ ∧ 𝑦 ∈ V ∧ (𝑥𝐴)𝐹𝑦) → 𝑦 ∈ ran 𝐹)
224, 21mp3an2 1325 . . . . . . . 8 (((𝑥𝐴) ∈ ℂ ∧ (𝑥𝐴)𝐹𝑦) → 𝑦 ∈ ran 𝐹)
233, 22sylancom 420 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥𝐴)𝐹𝑦) → 𝑦 ∈ ran 𝐹)
2420, 23jca 306 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥𝐴)𝐹𝑦) → (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹))
2524expl 378 . . . . 5 (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ∧ (𝑥𝐴)𝐹𝑦) → (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹)))
2625ssopab2dv 4275 . . . 4 (𝐴 ∈ ℂ → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥𝐴)𝐹𝑦)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹)})
27 df-xp 4629 . . . 4 ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹)}
2826, 27sseqtrrdi 3204 . . 3 (𝐴 ∈ ℂ → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥𝐴)𝐹𝑦)} ⊆ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹))
29 shftfval.1 . . . . . 6 𝐹 ∈ V
3029dmex 4889 . . . . 5 dom 𝐹 ∈ V
3130abrexex 6112 . . . 4 {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∈ V
3229rnex 4890 . . . 4 ran 𝐹 ∈ V
3331, 32xpex 4738 . . 3 ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) ∈ V
34 ssexg 4139 . . 3 (({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥𝐴)𝐹𝑦)} ⊆ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) ∧ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) ∈ V) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥𝐴)𝐹𝑦)} ∈ V)
3528, 33, 34sylancl 413 . 2 (𝐴 ∈ ℂ → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥𝐴)𝐹𝑦)} ∈ V)
36 breq 4002 . . . . . 6 (𝑧 = 𝐹 → ((𝑥𝑤)𝑧𝑦 ↔ (𝑥𝑤)𝐹𝑦))
3736anbi2d 464 . . . . 5 (𝑧 = 𝐹 → ((𝑥 ∈ ℂ ∧ (𝑥𝑤)𝑧𝑦) ↔ (𝑥 ∈ ℂ ∧ (𝑥𝑤)𝐹𝑦)))
3837opabbidv 4066 . . . 4 (𝑧 = 𝐹 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥𝑤)𝑧𝑦)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥𝑤)𝐹𝑦)})
39 oveq2 5877 . . . . . . 7 (𝑤 = 𝐴 → (𝑥𝑤) = (𝑥𝐴))
4039breq1d 4010 . . . . . 6 (𝑤 = 𝐴 → ((𝑥𝑤)𝐹𝑦 ↔ (𝑥𝐴)𝐹𝑦))
4140anbi2d 464 . . . . 5 (𝑤 = 𝐴 → ((𝑥 ∈ ℂ ∧ (𝑥𝑤)𝐹𝑦) ↔ (𝑥 ∈ ℂ ∧ (𝑥𝐴)𝐹𝑦)))
4241opabbidv 4066 . . . 4 (𝑤 = 𝐴 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥𝑤)𝐹𝑦)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥𝐴)𝐹𝑦)})
43 df-shft 10808 . . . 4 shift = (𝑧 ∈ V, 𝑤 ∈ ℂ ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥𝑤)𝑧𝑦)})
4438, 42, 43ovmpog 6003 . . 3 ((𝐹 ∈ V ∧ 𝐴 ∈ ℂ ∧ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥𝐴)𝐹𝑦)} ∈ V) → (𝐹 shift 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥𝐴)𝐹𝑦)})
4529, 44mp3an1 1324 . 2 ((𝐴 ∈ ℂ ∧ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥𝐴)𝐹𝑦)} ∈ V) → (𝐹 shift 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥𝐴)𝐹𝑦)})
4635, 45mpdan 421 1 (𝐴 ∈ ℂ → (𝐹 shift 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥𝐴)𝐹𝑦)})
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104   = wceq 1353  wcel 2148  {cab 2163  wrex 2456  Vcvv 2737  wss 3129   class class class wbr 4000  {copab 4060   × cxp 4621  dom cdm 4623  ran crn 4624  (class class class)co 5869  cc 7800   + caddc 7805  cmin 8118   shift cshi 10807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4115  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-resscn 7894  ax-1cn 7895  ax-icn 7897  ax-addcl 7898  ax-addrcl 7899  ax-mulcl 7900  ax-addcom 7902  ax-addass 7904  ax-distr 7906  ax-i2m1 7907  ax-0id 7910  ax-rnegex 7911  ax-cnre 7913
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-id 4290  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-riota 5825  df-ov 5872  df-oprab 5873  df-mpo 5874  df-sub 8120  df-shft 10808
This theorem is referenced by:  shftdm  10815  shftfib  10816  shftfn  10817  2shfti  10824  shftidt2  10825
  Copyright terms: Public domain W3C validator